From 053b314478e4802c55885f4fe8e89a570c890eef Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Tue, 3 Oct 2023 15:00:48 -0400
Subject: [PATCH] Another definition of limit

---
 src/simplicial-hott/13-limits.rzk.md | 90 +++++++++++++++-------------
 1 file changed, 49 insertions(+), 41 deletions(-)

diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md
index 400826a0..163c49b4 100644
--- a/src/simplicial-hott/13-limits.rzk.md
+++ b/src/simplicial-hott/13-limits.rzk.md
@@ -21,6 +21,37 @@ over `#!rzk f`.
   := Σ (b : B), hom (A → B) (constant A B b) f
 ```
 
+Given a function `#!rzk f : A → B` and `#!rzk b:B` we define the type of cocones
+under `#!rzk f`.
+
+```rzk
+#def cocone
+  ( A B : U )
+  ( f : A → B )
+  : U
+  := Σ (b : B), hom ( A → B) f (constant A B b)
+```
+We define a colimit for `#!rzk f : A → B` as an initial cocone under `#!rzk f`.
+
+```rzk
+#def colimit
+  ( A B : U )
+  ( f : A → B )
+  : U
+  := Σ ( 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`.
+
+```rzk
+#def limit
+  ( A B : U )
+  ( f : A → B )
+  : 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.
+Define cone as a family.
 ```rzk
 #def cone2
   (A B : U)
@@ -28,7 +59,7 @@ over `#!rzk f`.
   := \ f → \ b → (hom (A → B) (constant A B b) f)
 ```
 ```rzk
-#def constant-nat-trans-components
+#def constant-nat-trans
   (A B : U)
   ( x y : B )
   ( k : hom B x y)
@@ -36,62 +67,39 @@ over `#!rzk f`.
   := \ 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 )
-  : (cone2 A B f x) → (hom B b x) →  (cone2 A B f b)
-  := \ α k → vertical-comp-nat-trans
+  ( 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 )
+              ( \ a → B)
+              ( \ a → is-segal-B)
               ( constant A B b)
               ( constant A B x)
-              ( \ a → \ t → constant-nat-trans A B b x k a t)
+              (f)
+              ( constant-nat-trans A B b x k )
               ( α)
 ```
-
-Given a function `#!rzk f : A → B` and `#!rzk b:B` we define the type of cocones
-under `#!rzk f`.
-
-```rzk
-#def cocone
-  ( A B : U )
-  ( f : A → B )
-  : U
-  := Σ (b : B), hom ( A → B) f (constant A B b)
-```
-
-```rzk
-#def cocone2
-  (A B : U)
-  : (f : A → B) → (b : B) → U
-  := \ f → \ b → (hom ( A → B) f (constant A B b))
-```
-
-We define a colimit for `#!rzk f : A → B` as an initial cocone under `#!rzk f`.
+Another definition of limit.
 
 ```rzk
-#def colimit
-  ( A B : U )
-  ( f : A → B )
+#def limit2
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  ( is-segal-B : is-segal B)
   : U
-  := Σ ( x : cocone A B f ) , is-initial (cocone A B f) x
+  := Σ (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 )
 ```
 
-We define a limit of `#!rzk f : A → B` as a terminal 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
-```
 
 ## Uniqueness of initial and final objects.