From 928908e5203a855c71350cdcdf6c6de704658e9a Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Tue, 3 Oct 2023 15:26:54 -0400
Subject: [PATCH] Another definition of colimit

---
 src/simplicial-hott/13-limits.rzk.md | 46 +++++++++++++++++++++++++++-
 1 file changed, 45 insertions(+), 1 deletion(-)

diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md
index 163c49b4..708a532f 100644
--- a/src/simplicial-hott/13-limits.rzk.md
+++ b/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.