Merge branch 'main' into weak-ext-ext

mkdocs.yml

@@ -31,6 +31,7 @@ nav:
       - Covariantly Functorial Type Families: simplicial-hott/08-covariant.rzk.md
       - The Yoneda Lemma: simplicial-hott/09-yoneda.rzk.md
       - Rezk Types: simplicial-hott/10-rezk-types.rzk.md
+      - Adjunctions: simplicial-hott/11-adjunctions.rzk.md
       - Cocartesian Families: simplicial-hott/12-cocartesian.rzk.md
 
 markdown_extensions:

src/hott/03-equivalences.rzk.md

@@ -448,32 +448,48 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to
 Using function extensionality, a fiberwise equivalence defines an equivalence of
 dependent function types.
 
+```rzk
+#def is-equiv-function-is-equiv-family uses (funext)
+  ( X : U)
+  ( A B : X → U)
+  ( f : (x : X) → (A x) → (B x))
+  ( famisequiv : (x : X) → is-equiv (A x) (B x) (f x))
+  : is-equiv ((x : X) → A x) ((x : X) → B x) ( \ a x → f x (a x))
+  :=
+    ( ( ( \ b x → first (first (famisequiv x)) (b x)) ,
+        ( \ a →
+           eq-htpy
+            X A
+           ( \ x →
+              first
+                ( first (famisequiv x))
+                ( f x (a x)))
+            ( a)
+            ( \ x → second (first (famisequiv x)) (a x)))) ,
+      ( ( \ b x → first (second (famisequiv x)) (b x)) ,
+        ( \ b →
+            eq-htpy
+            X B
+            ( \ x →
+               f x (first (second (famisequiv x)) (b x)))
+            ( b)
+            ( \ x → second (second (famisequiv x)) (b x)))))
+```
+
 ```rzk
 #def equiv-function-equiv-family uses (funext)
   ( X : U)
   ( A B : X → U)
   ( famequiv : (x : X) → Equiv (A x) (B x))
   : Equiv ((x : X) → A x) ((x : X) → B x)
   :=
-    ( ( \ a x → first (famequiv x) (a x)) ,
-      ( ( ( \ b x → first (first (second (famequiv x))) (b x)) ,
-          ( \ a →
-            eq-htpy
-              X A
-              ( \ x →
-                first
-                  ( first (second (famequiv x)))
-                  ( first (famequiv x) (a x)))
-              ( a)
-              ( \ x → second (first (second (famequiv x))) (a x)))) ,
-        ( ( \ b x → first (second (second (famequiv x))) (b x)) ,
-          ( \ b →
-            eq-htpy
-              X B
-              ( \ x →
-                first (famequiv x) (first (second (second (famequiv x))) (b x)))
-              ( b)
-              ( \ x → second (second (second (famequiv x))) (b x))))))
+    ( ( \ a x → (first (famequiv x)) (a x)) ,
+      ( is-equiv-function-is-equiv-family
+        ( X)
+        ( A)
+        ( B)
+        ( \ x ax → first (famequiv x) (ax))
+        ( \ x → second (famequiv x))))
 ```
 
 ## Embeddings

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

@@ -101,6 +101,18 @@ unique lift with specified domain.
   := ( Σ (C : (A → U)) , is-covariant A C)
 ```
 
+The notion of a covariant family is stable under substitution into the base.
+
+```rzk title="RS17, Remark 8.3"
+#def is-covariant-substitution-is-covariant
+  ( A B : U)
+  ( C : A → U)
+  ( is-covariant-C : is-covariant A C)
+  ( g : B → A)
+  : is-covariant B (\ b → C (g b))
+  := \ x y f u → is-covariant-C (g x) (g y) (ap-hom B A g x y f) u
+```
+
 The notion of having a unique lift with a fixed domain may also be expressed by
 contractibility of the type of extensions along the domain inclusion into the
 1-simplex.
@@ -496,7 +508,7 @@ Finally, we see that covariant hom families in a Segal type are covariant.
   (A : U)
   (is-segal-A : is-segal A)
   (a : A)
-  : is-covariant A (\ x → hom A a x)
+  : is-covariant A (hom A a)
   := is-segal-representable-dhom-from-contractible A is-segal-A a
 ```
 
@@ -830,9 +842,9 @@ is covariant as shown above. Transport of an `e : C x` along an arrow
 
 ```
 
-We show that for each `v : C y`, the  map `covariant-uniqueness` is an equivalence.
-This follows from the fact that the total spaces (summed over `v : C y`)
-of both sides are contractible.
+We show that for each `v : C y`, the map `covariant-uniqueness` is an
+equivalence. This follows from the fact that the total spaces (summed over
+`v : C y`) of both sides are contractible.
 
 ```rzk title="RS17, Lemma 8.15"
 #def is-equiv-total-map-covariant-uniqueness-curried
@@ -1125,6 +1137,18 @@ has a unique lift with specified codomain.
   := ( Σ (C : A → U) , is-contravariant A C)
 ```
 
+The notion of a contravariant family is stable under substitution into the base.
+
+```rzk title="RS17, Remark 8.3, dual form"
+#def is-contravariant-substitution-is-contravariant
+  ( A B : U)
+  ( C : A → U)
+  ( is-contravariant-C : is-contravariant A C)
+  ( g : B → A)
+  : is-contravariant B (\ b → C (g b))
+  := \ x y f v → is-contravariant-C (g x) (g y) (ap-hom B A g x y f) v
+```
+
 The notion of having a unique lift with a fixed codomain may also be expressed
 by contractibility of the type of extensions along the codomain inclusion into
 the 1-simplex.

src/simplicial-hott/09-yoneda.rzk.md

@@ -209,6 +209,25 @@ This is proven combining the previous steps.
         ( evid-yon A is-segal-A a C is-covariant-C)))
 ```
 
+For later use, we observe that the same proof shows that the inverse map is an
+equivalence.
+
+```rzk
+#def inv-yoneda-lemma uses (funext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a : A)
+  ( C : A → U)
+  ( is-covariant-C : is-covariant A C)
+  : is-equiv (C a) ((z : A) → hom A a z → C z)
+      ( yon A is-segal-A a C is-covariant-C)
+  :=
+    ( ( ( evid A a C) ,
+        ( evid-yon A is-segal-A a C is-covariant-C)) ,
+      ( ( evid A a C) ,
+        ( yon-evid A is-segal-A a C is-covariant-C)))
+```
+
 ## Naturality
 
 The equivalence of the Yoneda lemma is natural in both $a : A$ and $C : A → U$.
@@ -557,6 +576,25 @@ equivalence.
         ( contra-evid-yon A is-segal-A a C is-contravariant-C)))
 ```
 
+For later use, we observe that the same proof shows that the inverse map is an
+equivalence.
+
+```rzk
+#def inv-contra-yoneda-lemma uses (funext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a : A)
+  ( C : A → U)
+  ( is-contravariant-C : is-contravariant A C)
+  : is-equiv (C a) ((z : A) → hom A z a → C z)
+      ( contra-yon A is-segal-A a C is-contravariant-C)
+  :=
+    ( ( ( contra-evid A a C) ,
+        ( contra-evid-yon A is-segal-A a C is-contravariant-C)) ,
+      ( ( contra-evid A a C) ,
+        ( contra-yon-evid A is-segal-A a C is-contravariant-C)))
+```
+
 ## Contravariant Naturality
 
 The equivalence of the Yoneda lemma is natural in both $a : A$ and $C : A → U$.