Merge pull request #86 from rzk-lang/limits-colimits-2

Limits-colimits-2

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

@@ -31,7 +31,6 @@ under `#!rzk f`.
   : 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
@@ -51,6 +50,114 @@ 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 of limits, we eventually want to prove both definitions coincide.
+Define cone as a family.
+
+```rzk
+#def cone2
+  (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 )
+              ( α)
+```
+Another definition of limit.
+
+```rzk
+#def limit2
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( 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 )
+```
+
+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)
+  : 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 )
+```
+The following alternative definition does not require a Segalness condition. When
+`#!rzk is-segal B` then definitions 1 and 3 coincide.
+
+```rzk
+#def limit3
+  ( A B : U)
+  ( f : A → B)
+  : U
+  := Σ ( b : B),(x : B) → Equiv (hom B b x ) (cone2 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)
+```
 
 ## Uniqueness of initial and final objects.