Transport-split and preunivalent type families

src/foundation-core/contractible-maps.lagda.md

@@ -129,8 +129,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of path-split maps see
   [`foundation.path-split-maps`](foundation.path-split-maps.md).

src/foundation-core/equivalences.lagda.md

@@ -749,8 +749,8 @@ syntax step-equivalence-reasoning e Z f = e ≃ Z by f
 
 ## See also
 
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).

src/foundation-core/path-split-maps.lagda.md

@@ -24,9 +24,9 @@ open import foundation-core.sections
 ## Idea
 
 A map `f : A → B` is said to be **path split** if it has a
-[section](foundation-core.sections.md) and its action on
-[identity types](foundation-core.identity-types.md) `Id x y → Id (f x) (f y)`
-has a section for each `x y : A`. By the
+[section](foundation-core.sections.md) and its
+[action on identifications](foundation.action-on-identifications-functions.md)
+`x ＝ y → f x ＝ f y` has a section for each `x y : A`. By the
 [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md),
 it follows that a map is path-split if and only if it is an
 [equivalence](foundation-core.equivalences.md).
@@ -80,8 +80,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).

src/foundation-core/sets.lagda.md

@@ -147,4 +147,21 @@ abstract
     {l1 l2 : Level} (A : UU l1) {B : UU l2} (e : A ≃ B) →
     is-set A → is-set B
   is-set-equiv' = is-trunc-equiv' zero-𝕋
+
+abstract
+  is-set-equiv-is-set :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+    is-set A → is-set B → is-set (A ≃ B)
+  is-set-equiv-is-set = is-trunc-equiv-is-trunc zero-𝕋
+
+module _
+  {l1 l2 : Level} (A : Set l1) (B : Set l2)
+  where
+
+  type-equiv-Set : UU (l1 ⊔ l2)
+  type-equiv-Set = type-Set A ≃ type-Set B
+
+  equiv-Set : Set (l1 ⊔ l2)
+  pr1 equiv-Set = type-equiv-Set
+  pr2 equiv-Set = is-set-equiv-is-set (is-set-type-Set A) (is-set-type-Set B)
 ```

src/foundation-core/transport-along-identifications.lagda.md

@@ -110,7 +110,7 @@ module _
 ```agda
 tr-Id-left :
   {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : b ＝ a) →
-  tr (_＝ a) q p ＝ ((inv q) ∙ p)
+  tr (_＝ a) q p ＝ (inv q ∙ p)
 tr-Id-left refl p = refl
 ```
 

src/foundation.lagda.md

@@ -270,6 +270,7 @@ open import foundation.precomposition-type-families public
 open import foundation.preidempotent-maps public
 open import foundation.preimages-of-subtypes public
 open import foundation.preunivalence public
+open import foundation.preunivalent-type-families public
 open import foundation.principle-of-omniscience public
 open import foundation.product-decompositions public
 open import foundation.product-decompositions-subuniverse public
@@ -352,6 +353,7 @@ open import foundation.transport-along-equivalences public
 open import foundation.transport-along-higher-identifications public
 open import foundation.transport-along-homotopies public
 open import foundation.transport-along-identifications public
+open import foundation.transport-split-type-families public
 open import foundation.transposition-span-diagrams public
 open import foundation.trivial-relaxed-sigma-decompositions public
 open import foundation.trivial-sigma-decompositions public

src/foundation/contractible-maps.lagda.md

@@ -133,8 +133,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of path-split maps see
   [`foundation.path-split-maps`](foundation.path-split-maps.md).

src/foundation/embeddings.lagda.md

@@ -322,9 +322,9 @@ module _
 
   abstract
     is-emb-section-ap :
-      ((x y : A) → section (ap f {x = x} {y = y})) → is-emb f
-    is-emb-section-ap section-ap-f x y =
-      fundamental-theorem-id-section x (λ y → ap f {y = y}) (section-ap-f x) y
+      ((x y : A) → section (ap f {x} {y})) → is-emb f
+    is-emb-section-ap section-ap-f x =
+      fundamental-theorem-id-section x (λ y → ap f) (section-ap-f x)
 ```
 
 ### If there is an equivalence `(f x = f y) ≃ (x = y)` that sends `refl` to `refl`, then f is an embedding

src/foundation/equivalences-maybe.lagda.md

@@ -380,6 +380,11 @@ equiv-equiv-Maybe :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (Maybe X ≃ Maybe Y) → (X ≃ Y)
 pr1 (equiv-equiv-Maybe e) = map-equiv-equiv-Maybe e
 pr2 (equiv-equiv-Maybe e) = is-equiv-map-equiv-equiv-Maybe e
+
+compute-equiv-equiv-Maybe-id-equiv :
+  {l1 : Level} {X : UU l1} →
+  equiv-equiv-Maybe id-equiv ＝ id-equiv {A = X}
+compute-equiv-equiv-Maybe-id-equiv = eq-htpy-equiv refl-htpy
 ```
 
 ### For any set `X`, the type of automorphisms on `X` is equivalent to the type of automorphisms on `Maybe X` that fix the exception

src/foundation/equivalences.lagda.md

@@ -805,8 +805,8 @@ module _
 
 ## See also
 
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).

src/foundation/fundamental-theorem-of-identity-types.lagda.md

@@ -8,11 +8,13 @@ module foundation.fundamental-theorem-of-identity-types where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.retracts-of-types
 open import foundation.universe-levels
 
 open import foundation-core.contractible-types
 open import foundation-core.equivalences
 open import foundation-core.families-of-equivalences
+open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
@@ -87,7 +89,7 @@ module _
 
   abstract
     fundamental-theorem-id-J' :
-      (is-fiberwise-equiv (ind-Id a (λ x p → B x) b)) → is-torsorial B
+      is-fiberwise-equiv (ind-Id a (λ x p → B x) b) → is-torsorial B
     fundamental-theorem-id-J' H =
       is-contr-is-equiv'
         ( Σ A (Id a))
@@ -105,18 +107,29 @@ module _
 
   abstract
     fundamental-theorem-id-retraction :
-      (i : (x : A) → B x → a ＝ x) → (R : (x : A) → retraction (i x)) →
+      (i : (x : A) → B x → a ＝ x) →
+      ((x : A) → retraction (i x)) →
       is-fiberwise-equiv i
     fundamental-theorem-id-retraction i R =
       is-fiberwise-equiv-is-equiv-tot
         ( is-equiv-is-contr (tot i)
-          ( is-contr-retract-of (Σ _ (λ y → a ＝ y))
-            ( pair (tot i)
-              ( pair (tot λ x → pr1 (R x))
-                ( ( inv-htpy (preserves-comp-tot i (λ x → pr1 (R x)))) ∙h
-                  ( ( tot-htpy λ x → pr2 (R x)) ∙h (tot-id B)))))
+          ( is-contr-retract-of
+            ( Σ _ (λ y → a ＝ y))
+            ( ( tot i) ,
+              ( tot (λ x → pr1 (R x))) ,
+              ( ( inv-htpy (preserves-comp-tot i (pr1 ∘ R))) ∙h
+                ( tot-htpy (pr2 ∘ R)) ∙h
+                ( tot-id B)))
             ( is-torsorial-path a))
           ( is-torsorial-path a))
+
+    fundamental-theorem-id-retract :
+      (R : (x : A) → (B x) retract-of (a ＝ x)) →
+      is-fiberwise-equiv (inclusion-retract ∘ R)
+    fundamental-theorem-id-retract R =
+      fundamental-theorem-id-retraction
+        ( inclusion-retract ∘ R)
+        ( retraction-retract ∘ R)
 ```
 
 ### The fundamental theorem of identity types, using sections
@@ -128,19 +141,18 @@ module _
 
   abstract
     fundamental-theorem-id-section :
-      (f : (x : A) → a ＝ x → B x) → ((x : A) → section (f x)) →
+      (f : (x : A) → a ＝ x → B x) →
+      ((x : A) → section (f x)) →
       is-fiberwise-equiv f
     fundamental-theorem-id-section f section-f x =
-      is-equiv-section-is-equiv (f x) (section-f x) (is-fiberwise-equiv-i x)
-      where
-      i : (x : A) → B x → a ＝ x
-      i = λ x → pr1 (section-f x)
-      retraction-i : (x : A) → retraction (i x)
-      pr1 (retraction-i x) = f x
-      pr2 (retraction-i x) = pr2 (section-f x)
-      is-fiberwise-equiv-i : is-fiberwise-equiv i
-      is-fiberwise-equiv-i =
-        fundamental-theorem-id-retraction a i retraction-i
+      is-equiv-section-is-equiv
+        ( f x)
+        ( section-f x)
+        ( fundamental-theorem-id-retraction
+          ( a)
+          ( λ x → map-section (f x) (section-f x))
+          ( λ x → (f x , is-section-map-section (f x) (section-f x)))
+          ( x))
 ```
 
 ## See also

src/foundation/identity-systems.lagda.md

@@ -15,6 +15,7 @@ open import foundation.universe-levels
 open import foundation-core.contractible-types
 open import foundation-core.families-of-equivalences
 open import foundation-core.identity-types
+open import foundation-core.propositions
 open import foundation-core.sections
 open import foundation-core.torsorial-type-families
 open import foundation-core.transport-along-identifications
@@ -59,11 +60,11 @@ module _
 
 ```agda
 module _
-    {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (a : A) (b : B a)
-    where
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (a : A) (b : B a)
+  where
 
-    is-identity-system : UUω
-    is-identity-system = {l : Level} → is-identity-system-Level l B a b
+  is-identity-system : UUω
+  is-identity-system = {l : Level} → is-identity-system-Level l B a b
 ```
 
 ## Properties

src/foundation/path-split-maps.lagda.md

@@ -74,8 +74,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).

src/foundation/preunivalence.lagda.md

@@ -107,4 +107,5 @@ preunivalence = preunivalence-axiom-univalence-axiom univalence
 - Preunivalence is sufficient to prove that `Id : A → (A → 𝒰)` is an embedding.
   This fact is proven in
   [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md)
+- [Preunivalent type families](foundation.preunivalent-type-families.md)
 - [Preunivalent categories](category-theory.preunivalent-categories.md)