colimits are unique up to isomorphism

src/simplicial-hott/13-limits.rzk.md

@@ -8,15 +8,22 @@ This is a literate `rzk` file:
 #lang rzk-1
 ```
 
+Some definitions make use of function extentionality.
+
+```rzk
+#assume funext : FunExt
+#assume naiveextext : NaiveExtExt
+```
+
 ## Definition limits and colimits
 
 Given a function `#!rzk f : A → B` and `#!rzk b:B` we define the type of cones
 over `#!rzk f`.
 
 ```rzk
 #def cone
-  ( A B : U )
-  ( f : A → B )
+  ( A B : U)
+  ( f : A → B)
   : U
   := Σ (b : B), hom (A → B) (constant A B b) f
 ```
@@ -26,8 +33,8 @@ under `#!rzk f`.
 
 ```rzk
 #def cocone
-  ( A B : U )
-  ( f : A → B )
+  ( A B : U)
+  ( f : A → B)
   : U
   := Σ (b : B), hom ( A → B) f (constant A B b)
 ```
@@ -39,55 +46,53 @@ We define a colimit for `#!rzk f : A → B` as an initial cocone under `#!rzk f`
   ( A B : U )
   ( f : A → B )
   : U
-  := Σ ( x : cocone A B f ) , is-initial (cocone A B f) x
+  := Σ ( x : cocone A B f) , is-initial ( cocone A B f) x
 ```
 
-We define a limit of `#!rzk f : A → B` as a terminal cone over `#!rzk f`.
+We define a limit of `#!rzk f : A → B` as a final cone over `#!rzk f`.
 
 ```rzk
 #def limit
   ( A B : U )
   ( f : A → B )
   : U
-  :=  Σ ( x : cone A B f ) , is-final (cone A B f) x
+  :=  Σ ( x : cone A B f) , is-final ( cone A B f) x
 ```
 
 We give a second definition of limits, we eventually want to prove both
 definitions coincide. Define cone as a family.
 
 ```rzk
-#def cone2
+#def family-cone
   (A B : U)
   : (A → B) → (B) → U
   := \ f → \ b → (hom (A → B) (constant A B b) f)
-```
 
-```rzk
 #def constant-nat-trans
   (A B : U)
   ( x y : B )
   ( k : hom B x y)
   : hom (A → B) (constant A B x) (constant A B y)
   := \ t a → ( constant A ( hom B x y ) k ) a t
-```
 
-```rzk
 #def cone-precomposition
   ( A B : U)
   ( is-segal-B : is-segal B)
   ( f : A → B )
   ( b x : B )
   ( k : hom B b x)
-  : (cone2 A B f x) →  (cone2 A B f b)
-  := \ α → vertical-comp-nat-trans
-              ( A)
-              ( \ a → B)
-              ( \ a → is-segal-B)
-              ( constant A B b)
-              ( constant A B x)
-              (f)
-              ( constant-nat-trans A B b x k )
-              ( α)
+  : ( family-cone A B f x) →  ( family-cone A B f b)
+  :=
+  \ α
+  → vertical-comp-nat-trans
+    ( A)
+    ( \ _ → B)
+    ( \ _ → is-segal-B)
+    ( constant A B b)
+    ( constant A B x)
+    ( f)
+    ( constant-nat-trans A B b x k)
+    ( α)
 ```
 
 Another definition of limit.
@@ -99,38 +104,41 @@ Another definition of limit.
   ( f : A → B)
   : U
   := Σ (b : B),
-     Σ ( c : cone2 A B f b ),
-     ( x : B) → ( k : hom B b x)
-      → is-equiv (cone2 A B f x) (cone2 A B f b) (cone-precomposition A B is-segal-B f b x k )
+  Σ ( c : family-cone A B f b)
+    , ( x : B) → ( k : hom B b x)
+      → is-equiv
+        ( family-cone A B f x)
+        ( family-cone A B f b)
+        ( cone-precomposition A B is-segal-B f b x k)
 ```
 
 We give a second definition of colimits, we eventually want to prove both
 definitions coincide. Define cocone as a family.
 
 ```rzk
-#def cocone2
+#def family-cocone
   (A B : U)
-  : (A → B) → (B) → U
+  : ( A → B) → ( B) → U
   := \ f → \ b → (hom (A → B) f (constant A B b))
-```
 
-```rzk
 #def cocone-postcomposition
   ( A B : U)
   ( is-segal-B : is-segal B)
-  ( f : A → B )
-  ( x b : B )
+  ( f : A → B)
+  ( x b : B)
   ( k : hom B x b)
-  : (cocone2 A B f x) → (cocone2 A B f b)
-  := \ α → vertical-comp-nat-trans
-              ( A)
-              ( \ a → B)
-              ( \ a → is-segal-B)
-              (f)
-              ( constant A B x)
-              ( constant A B b)
-              ( α)
-              ( constant-nat-trans A B x b k )
+  : ( family-cocone A B f x) → ( family-cocone A B f b)
+  :=
+  \ α
+  → vertical-comp-nat-trans
+    ( A)
+    ( \ _ → B)
+    ( \ _ → is-segal-B)
+    ( f)
+    ( constant A B x)
+    ( constant A B b)
+    ( α)
+    ( constant-nat-trans A B x b k )
 ```
 
 Another definition of colimit.
@@ -142,9 +150,12 @@ Another definition of colimit.
   ( f : A → B)
   : U
   := Σ (b : B),
-     Σ ( c : cocone2 A B f b ),
-     ( x : B) → ( k : hom B x b)
-      → is-equiv (cocone2 A B f x) (cocone2 A B f b) (cocone-postcomposition A B is-segal-B f x b k )
+  Σ ( c : family-cocone A B f b)
+    , ( x : B) → ( k : hom B x b)
+    → is-equiv
+      ( family-cocone A B f x)
+      ( family-cocone A B f b)
+      ( cocone-postcomposition A B is-segal-B f x b k)
 ```
 
 The following alternative definition does not require a Segalness condition.
@@ -155,15 +166,13 @@ When `#!rzk is-segal B` then definitions 1 and 3 coincide.
   ( A B : U)
   ( f : A → B)
   : U
-  := Σ ( b : B),(x : B) → Equiv (hom B b x ) (cone2 A B f x)
-```
+  := Σ ( b : B),( x : B) → Equiv ( hom B b x) ( family-cone A B f x)
 
-```rzk
 #def colimit3
   ( A B : U)
   ( f : A → B)
   : U
-  := Σ ( b : B),(x : B) → Equiv (hom B x b ) (cocone2 A B f x)
+  := Σ ( b : B), ( x : B) → Equiv ( hom B x b) ( family-cocone A B f x)
 ```
 
 ## Uniqueness of initial and final objects.
@@ -207,7 +216,6 @@ In a Segal type, final objects are isomorphic.
   ( a b : A)
   ( is-final-a : is-final A a)
   ( is-final-b : is-final A b)
-  ( iso : Iso A is-segal-A a b)
   : Iso A is-segal-A a b
   :=
     ( first (is-final-b a) ,
@@ -229,4 +237,68 @@ In a Segal type, final objects are isomorphic.
             ( id-hom A b))))
 ```
 
-## Uniqueness up to isomophism of (co)limits
+## Uniqueness up to isomophism of (co)limits.
+
+The type of cocones of a function with codomain a Segal type is a Segal type.
+
+```rzk title="BM22, Remark 4 (i)"
+#def is-covariant-family-cone-is-segal
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  : is-covariant B ( \ b → family-cocone A B f b)
+  :=
+    is-covariant-substitution-is-covariant
+    ( A → B)
+    ( B)
+    ( hom ( A → B) f)
+    ( is-covariant-representable-is-segal
+        ( A → B)
+        ( is-segal-function-type
+          ( funext)
+          ( A)
+          ( \ _ → B)
+          ( \ _ → is-segal-B))
+        ( f))
+    ( \ b → constant A B b)
+
+#def is-segal-cocone-is-segal uses (funext)
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  : is-segal ( cocone A B f)
+  :=
+    is-segal-total-type-covariant-family-is-segal-base
+    ( naiveextext)
+    ( B)
+    ( family-cocone A B f)
+    ( is-covariant-family-cone-is-segal
+      ( A)
+      ( B)
+      ( is-segal-B)
+      ( f))
+    ( is-segal-B)
+```
+
+Colimits are unique up to isomorphism.
+
+```rzk title="BM, Corollary 1 (i)"
+#def iso-colimit-is-segal uses ( naiveextext funext)
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  ( x y : colimit A B f)
+  : Iso
+    ( cocone A B f)
+    ( is-segal-cocone-is-segal A B is-segal-B f)
+    ( first x)
+    ( first y)
+  :=
+    iso-initial
+    ( cocone A B f)
+    ( is-segal-cocone-is-segal A B is-segal-B f)
+    ( first x)
+    ( first y)
+    ( second x)
+    ( second y)
+```