Uniqueness of adjunction data

src/hott/05-sigma.rzk.md

@@ -536,7 +536,20 @@ This is the dependent version of the currying equivalence.
   ( B : A → U)
   ( C : (x : A) → B x → U)
   : Equiv
-      ( (x : A) → Σ (y : B x) , C x y)
-      ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x))
+    ( (x : A) → Σ (y : B x) , C x y)
+    ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x))
   := (choice A B C , is-equiv-choice A B C)
+
+#def inv-equiv-choice
+  ( A : U)
+  ( B : A → U)
+  ( C : (x : A) → B x → U)
+  : Equiv
+    ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x))
+    ( (x : A) → Σ (y : B x) , C x y)
+  :=
+  inv-equiv
+  ( (x : A) → Σ (y : B x) , C x y)
+  ( Σ ( f : (x : A) → B x) , (x : A) → C x (f x))
+  ( equiv-choice A B C)
 ```

src/simplicial-hott/05-segal-types.rzk.md

@@ -1182,6 +1182,20 @@ We conclude that Segal composition is associative.
     ( left-associative-is-segal A is-segal-A w x y z f g h)
     ( right-associative-is-segal A is-segal-A w x y z f g h)
 
+#def rev-associative-is-segal uses (extext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( w x y z : A)
+  ( f : hom A w x)
+  ( g : hom A x y)
+  ( h : hom A y z)
+  : ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h)) =
+    ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
+  :=
+    rev (hom A w z)
+    ( comp-is-segal A is-segal-A w y z (comp-is-segal A is-segal-A w x y f g) h)
+    ( comp-is-segal A is-segal-A w x z f (comp-is-segal A is-segal-A x y z g h))
+    ( associative-is-segal A is-segal-A w x y z f g h)
 
 #def postcomp-is-segal
   ( A : U)

src/simplicial-hott/06-2cat-of-segal-types.rzk.md

@@ -101,6 +101,30 @@ Preservation of composition requires the Segal hypothesis.
       ( ap-hom2 A B F x y z f g
         ( comp-is-segal A is-segal-A x y z f g)
         ( witness-comp-is-segal A is-segal-A x y z f g))
+
+#def rev-functors-pres-comp
+  ( A B : U)
+  ( is-segal-A : is-segal A)
+  ( is-segal-B : is-segal B)
+  ( F : A → B)
+  ( x y z : A)
+  ( f : hom A x y)
+  ( g : hom A y z)
+  :
+    ( ap-hom A B F x z (comp-is-segal A is-segal-A x y z f g))
+    =
+    ( comp-is-segal B is-segal-B
+      ( F x) (F y) (F z)
+      ( ap-hom A B F x y f)
+      ( ap-hom A B F y z g))
+  :=
+    rev (hom B (F x) (F z))
+    ( comp-is-segal B is-segal-B
+      ( F x) (F y) (F z)
+      ( ap-hom A B F x y f)
+      ( ap-hom A B F y z g))
+    ( ap-hom A B F x z (comp-is-segal A is-segal-A x y z f g))
+    ( functors-pres-comp A B is-segal-A is-segal-B F x y z f g)
 ```
 
 ## Natural transformations

src/simplicial-hott/08-covariant.rzk.md

@@ -1336,6 +1336,25 @@ equivalence. This follows from the fact that the total types (summed over
       v
 ```
 
+We compute covariant transport of a substitution.
+
+```rzk
+#def compute-covariant-transport-of-substitution
+  ( A B : U)
+  ( C : A → U)
+  ( is-covariant-C : is-covariant A C)
+  ( g : B → A)
+  ( x y : B)
+  ( f : hom B x y)
+  ( u : C (g x))
+  : covariant-transport B x y f (\ b → C (g b))
+    ( is-covariant-substitution-is-covariant A B C is-covariant-C g) u
+    =
+    covariant-transport A (g x) (g y) (ap-hom B A g x y f) C
+    ( is-covariant-C) u
+  := refl
+```
+
 ## Covariant functoriality
 
 The covariant transport operation defines a covariantly functorial action of
@@ -2198,7 +2217,7 @@ The fibers of a covariant fibration over a Segal type are discrete types.
       ( v))
 ```
 
-In a segal type, covariant hom families are covariant,hence representable homs
+In a Segal type, covariant hom families are covariant, hence representable homs
 are discrete.
 
 ```rzk title="RS17, Corollary 8.19"

src/simplicial-hott/10-rezk-types.rzk.md

@@ -742,6 +742,38 @@ map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence.
         is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y)
 ```
 
+The inverse to `#!rzk iso-eq` for a Rezk type.
+
+```rzk
+#def eq-iso-is-rezk
+  ( A : U)
+  ( is-rezk-A : is-rezk A)
+  ( x y : A)
+  : Iso A (first is-rezk-A) x y → x = y
+  :=
+    section-is-equiv (x = y) (Iso A (first is-rezk-A) x y)
+    ( iso-eq A (first is-rezk-A) x y)
+    ( ( second is-rezk-A) x y)
+
+#def iso-eq-iso-is-rezk
+  ( A : U)
+  ( is-rezk-A : is-rezk A)
+  ( x y : A)
+  ( (e, is-iso-e) : Iso A (first is-rezk-A) x y)
+  : first (iso-eq A (first is-rezk-A) x y (eq-iso-is-rezk A is-rezk-A x y (e, is-iso-e))) = e
+  :=
+    first-path-Σ
+    ( hom A x y)
+    ( is-iso-arrow A (first is-rezk-A) x y)
+    ( iso-eq A (first is-rezk-A) x y
+      ( eq-iso-is-rezk A is-rezk-A x y (e, is-iso-e)))
+    ( (e, is-iso-e))
+    ( ( second
+      ( has-section-is-equiv (x = y) (Iso A (first is-rezk-A) x y)
+        ( iso-eq A (first is-rezk-A) x y)
+        ( ( second is-rezk-A) x y))) (e, is-iso-e))
+```
+
 The following results show how `#!rzk iso-eq` mediates between the
 type-theoretic operations on paths and the category-theoretic operations on
 arrows.