Another definition of colimit

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

@@ -50,8 +50,9 @@ We define a limit of `#!rzk f : A → B` as a terminal cone over `#!rzk f`.
   : U
   :=  Σ ( x : cone A B f ) , is-final (cone A B f) x
 ```
-We give a second definition, we eventually want to prove that they coincide.
+We give a second definition of limits, we eventually want to prove both definitions coincide.
 Define cone as a family.
+
 ```rzk
 #def cone2
   (A B : U)
@@ -100,6 +101,49 @@ Another definition of limit.
       → is-equiv (cone2 A B f x) (cone2 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
+  (A 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 )
+  ( 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 )
+```
+Another definition of colimit.
+
+```rzk
+#def colimit2
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  ( is-segal-B : is-segal 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 )
+```
+
 
 ## Uniqueness of initial and final objects.