From c68b463867691b2d7739366cd50e31ef88374529 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Mon, 29 Apr 2024 14:43:53 +0200 Subject: [PATCH 01/37] experiment --- src/simplicial-hott/08-covariant.rzk.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index f50094e5..d73698e0 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -1056,6 +1056,30 @@ types as follows. ( representable-dhom-from-cofibration-composition A a x y f u) ``` +## Dependent Composition + +```rzk +#def dependent-composition + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( k : dhom A x y f C u v) + ( m : dhom A y z g C v w) + : Σ ( n : (dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w)) + , ( dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) + C u v w k m n) + := (U + , U) +``` + ## Covariant lifts, transport, and uniqueness In a covariant family C over a base type A , a term u : C x may be transported From 9e06319e8a7e8ed0ee8df73b51c493ce75600b86 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Mon, 29 Apr 2024 15:25:22 +0200 Subject: [PATCH 02/37] nonsense --- src/simplicial-hott/08-covariant.rzk.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index d73698e0..e12f8ea6 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -1076,7 +1076,9 @@ types as follows. , ( dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g) C u v w k m n) - := (U + := (comp-is-segal (total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) U , U) ``` From d9a8ee098d704fb15cfaafe558b2fb4c23bdb327 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Mon, 29 Apr 2024 15:36:47 +0200 Subject: [PATCH 03/37] hello mr google how do I compose maps --- src/simplicial-hott/08-covariant.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index e12f8ea6..ba5b0eea 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -1078,7 +1078,7 @@ types as follows. C u v w k m n) := (comp-is-segal (total-type A C) ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) U + A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) k m ---something wrong here , U) ``` From 0b2de2f6400dc216b9f2c16a253297f9597e6e5c Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Mon, 29 Apr 2024 16:19:25 +0200 Subject: [PATCH 04/37] hello google how do I compose maps --- src/simplicial-hott/08-covariant.rzk.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index ba5b0eea..78cbf837 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -1056,7 +1056,7 @@ types as follows. ( representable-dhom-from-cofibration-composition A a x y f u) ``` -## Dependent Composition +## Dependent composition ```rzk #def dependent-composition @@ -1078,8 +1078,12 @@ types as follows. C u v w k m n) := (comp-is-segal (total-type A C) ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) k m ---something wrong here - , U) + A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) + ( \ t → (f t , k t)) (\ t → (g t , m t)) ---I truly have no idea + , witness-comp-is-segal (total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) + ( \ t → (f t , k t)) (\ t → (g t , m t))) ``` ## Covariant lifts, transport, and uniqueness From 1688283cf5d334dd34c53312d530f11a9fc09700 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Mon, 29 Apr 2024 17:24:21 +0200 Subject: [PATCH 05/37] If an infinite number of monkeys type randomly on infinite typewriters, does one of them produce composition over a Segal type? --- src/simplicial-hott/08-covariant.rzk.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 78cbf837..a55e5e8d 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -1073,17 +1073,15 @@ types as follows. ( k : dhom A x y f C u v) ( m : dhom A y z g C v w) : Σ ( n : (dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w)) - , ( dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + , ( dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g) C u v w k m n) - := (comp-is-segal (total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) - ( \ t → (f t , k t)) (\ t → (g t , m t)) ---I truly have no idea - , witness-comp-is-segal (total-type A C) + := (projection-total-type (comp-is-segal (total-type A C) ( is-segal-total-type-covariant-family-is-segal-base A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) ( \ t → (f t , k t)) (\ t → (g t , m t))) + ---I truly have no idea + , U) ``` ## Covariant lifts, transport, and uniqueness From e50e3b1e8dbda98e06cbeb49e1d79b94871344d1 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 1 May 2024 17:23:42 +0200 Subject: [PATCH 06/37] ? --- src/simplicial-hott/08-covariant.rzk.md | 106 ++++++++++++++---------- 1 file changed, 60 insertions(+), 46 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index a55e5e8d..97c80ded 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -467,6 +467,66 @@ Segal, then so is `Σ A, C`. ( is-naive-left-fibration-is-covariant A C is-covariant-C)) ``` +## Dependent composition + +```rzk +#def dcomp uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( k : dhom A x y f C u v) + ( m : dhom A y z g C v w) + : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w + := comp-is-segal (total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( x , u) (y , v) (z , w) + ( \ t → (f t , k t)) (\ t → (g t , m t)) + --I now need to project to the second variable but I can't. + + --second (first (first( + --( is-segal-total-type-covariant-family-is-segal-base + --A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) + --( \ t → (f t , k t)) (\ t → (g t , m t))))) + + --Σ ( n : (dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w)) + --, ( dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + --( witness-comp-is-segal A is-segal-A x y z f g) + --C u v w k m n) + + --projection-total-type????? + --( comp-is-segal (total-type A C) + --( is-segal-total-type-covariant-family-is-segal-base + --A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) + --( \ t → (f t , k t)) (\ t → (g t , m t))) +``` + +## Covariant lifts, transport, and uniqueness + +In a covariant family C over a base type A , a term u : C x may be transported +along an arrow f : hom A x y to give a term in C y. + +```rzk title="RS17, covariant transport from beginning of Section 8.2" +#def covariant-transport + ( A : U) + ( x y : A) + ( f : hom A x y) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + : C y + := + first (center-contraction (dhom-from A x y f C u) (is-covariant-C x y f u)) +``` + + ## Representable covariant families If `A` is a Segal type and `a : A` is any term, then `hom A a` defines a @@ -1056,52 +1116,6 @@ types as follows. ( representable-dhom-from-cofibration-composition A a x y f u) ``` -## Dependent composition - -```rzk -#def dependent-composition - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( k : dhom A x y f C u v) - ( m : dhom A y z g C v w) - : Σ ( n : (dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w)) - , ( dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) - ( witness-comp-is-segal A is-segal-A x y z f g) - C u v w k m n) - := (projection-total-type (comp-is-segal (total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) - ( \ t → (f t , k t)) (\ t → (g t , m t))) - ---I truly have no idea - , U) -``` - -## Covariant lifts, transport, and uniqueness - -In a covariant family C over a base type A , a term u : C x may be transported -along an arrow f : hom A x y to give a term in C y. - -```rzk title="RS17, covariant transport from beginning of Section 8.2" -#def covariant-transport - ( A : U) - ( x y : A) - ( f : hom A x y) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - : C y - := - first (center-contraction (dhom-from A x y f C u) (is-covariant-C x y f u)) -``` - For example, if `A` is a Segal type and `a : A`, the family `C x := hom A a x` is covariant as shown above. Transport of an `e : C x` along an arrow `f : hom A x y` just yields composition of `f` with `e`. From 13c6f0b16151298c17885e2c69941fd13ef32de0 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 8 May 2024 16:48:48 +0200 Subject: [PATCH 07/37] fdjahFIJ --- src/simplicial-hott/08-covariant.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 97c80ded..8eb2bf61 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -484,11 +484,11 @@ Segal, then so is `Σ A, C`. ( k : dhom A x y f C u v) ( m : dhom A y z g C v w) : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w - := comp-is-segal (total-type A C) + := \ t → second ((comp-is-segal (total-type A C) ( is-segal-total-type-covariant-family-is-segal-base A C is-covariant-C is-segal-A) ( x , u) (y , v) (z , w) - ( \ t → (f t , k t)) (\ t → (g t , m t)) + ( \ r → (f r , k r)) (\ s → (g s , m s))) t) --I now need to project to the second variable but I can't. --second (first (first( From 9bd60f51cb1d9d1fbcc31c10784c3d8e0ddcb498 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 8 May 2024 21:44:19 +0200 Subject: [PATCH 08/37] dcomp --- src/simplicial-hott/08-covariant.rzk.md | 37 ++++++++----------------- 1 file changed, 12 insertions(+), 25 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 8eb2bf61..24311e19 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -469,7 +469,7 @@ Segal, then so is `Σ A, C`. ## Dependent composition -```rzk +```rzk title="RS17, Remark 8.11" #def dcomp uses (extext) ( A : U) ( is-segal-A : is-segal A) @@ -481,31 +481,18 @@ Segal, then so is `Σ A, C`. ( u : C x) ( v : C y) ( w : C z) - ( k : dhom A x y f C u v) - ( m : dhom A y z g C v w) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w - := \ t → second ((comp-is-segal (total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - ( x , u) (y , v) (z , w) - ( \ r → (f r , k r)) (\ s → (g s , m s))) t) - --I now need to project to the second variable but I can't. - - --second (first (first( - --( is-segal-total-type-covariant-family-is-segal-base - --A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) - --( \ t → (f t , k t)) (\ t → (g t , m t))))) - - --Σ ( n : (dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w)) - --, ( dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) - --( witness-comp-is-segal A is-segal-A x y z f g) - --C u v w k m n) - - --projection-total-type????? - --( comp-is-segal (total-type A C) - --( is-segal-total-type-covariant-family-is-segal-base - --A C is-covariant-C is-segal-A) (x , u) (y , v) (z , w) - --( \ t → (f t , k t)) (\ t → (g t , m t))) + := + \ r → + second + ( comp-is-segal + ( total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( x , u) (y , v) (z , w) + ( \ r → (f r , ff r)) (\ s → (g s , gg s)) r) ``` ## Covariant lifts, transport, and uniqueness From a12e80452e33ca9d16578d28c350a9d3a4b94fd9 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis <116834840+thchatzidiamantis@users.noreply.github.com> Date: Wed, 8 May 2024 22:05:26 +0200 Subject: [PATCH 09/37] Update 08-covariant.rzk.md --- src/simplicial-hott/08-covariant.rzk.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 24311e19..4cb191a9 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -485,14 +485,14 @@ Segal, then so is `Σ A, C`. ( gg : dhom A y z g C v w) : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w := - \ r → + \ t → second ( comp-is-segal ( total-type A C) ( is-segal-total-type-covariant-family-is-segal-base A C is-covariant-C is-segal-A) ( x , u) (y , v) (z , w) - ( \ r → (f r , ff r)) (\ s → (g s , gg s)) r) + ( \ r → (f r , ff r)) (\ s → (g s , gg s)) t) ``` ## Covariant lifts, transport, and uniqueness From 4eb0fb8ceb01b6bd77add5cee9031ae7179e00bf Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Sun, 26 May 2024 15:30:35 +0200 Subject: [PATCH 10/37] stuff --- src/simplicial-hott/08-covariant.rzk.md | 152 ++++++++++++++++++++++-- 1 file changed, 141 insertions(+), 11 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 24311e19..f29ed1ec 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -469,8 +469,79 @@ Segal, then so is `Σ A, C`. ## Dependent composition + +```rzk +-- #def dhom-dhom-to-dhom2 +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( h : hom A x z) +-- ( α : hom2 A x y z f g h) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- ( hh : dhom A x z h C u w) +-- : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) +-- , ( hom2 (total-type A C) (x , u) (y , v) (z , w) +-- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) +``` + +```rzk +#def dhom2-to-dhom + ( A : U) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( h : hom A x z) + ( α : hom2 A x y z f g h) + ( C : A → U) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + ( hh : dhom A x z h C u w) + : dhom2 A x y z f g h α C u v w ff gg hh + → dhom A x z h C u w + := + \ k → + ( \ t → k (t , t)) +``` + +```rzk +#def dhom2-to-hom2-total-type + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : ( Σ ( h : hom A x z) + , Σ ( α : hom2 A x y z f g h) + , ( Σ ( hh : dhom A x z h C u w) + , dhom2 A x y z f g h α C u v w ff gg hh)) + → ( Σ ( k : hom (total-type A C) (x , u) (z , w)) + , ( hom2 (total-type A C) (x , u) (y , v) (z , w) + ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) + := + \ (h , (α , (hh , k))) → + ( \ t → (h t , hh t) , \ t → (α t , k t)) +``` + ```rzk title="RS17, Remark 8.11" -#def dcomp uses (extext) +#def hom2-total-type-to-dhom2 ( A : U) ( is-segal-A : is-segal A) ( x y z : A) @@ -483,16 +554,75 @@ Segal, then so is `Σ A, C`. ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w - := - \ r → - second - ( comp-is-segal - ( total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - ( x , u) (y , v) (z , w) - ( \ r → (f r , ff r)) (\ s → (g s , gg s)) r) + : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) + , ( hom2 (total-type A C) (x , u) (y , v) (z , w) + ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) + → Σ ( h : hom A x z) + , Σ ( α : hom2 A x y z f g h) + , ( Σ ( hh : dhom A x z h C u w) + , dhom2 A x y z f g h α C u v w ff gg hh) + := + \ (k , kk) → + ( \ t → first (k t) + , ( \ t → first (kk t) + , ( \ t → second (kk (t , t)) , \ t → second (kk t)))) +-- #def test uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( h : hom A x z) +-- ( α : hom2 A x y z f g h) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : is-contr (Σ (hh : dhom A x z h C u w) +-- , dhom2 A x y z f g h α C u v w ff gg hh) +-- := + + + +-- #def total-hom-to-dhom +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y : A) +-- ( C : A → U) +-- ( f : hom A x y) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( k : hom (total-type A C) (x , u) (y , v)) +-- : dhom A x y f C u v +-- := \ t → second (k t) + --[t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y] + +-- #def dcomp uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w +-- := +-- second +-- comp-is-segal +-- ( total-type A C) +-- ( is-segal-total-type-covariant-family-is-segal-base +-- A C is-covariant-C is-segal-A) +-- ( x , u) (y , v) (z , w) +-- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) ``` ## Covariant lifts, transport, and uniqueness From 8d96c09c09bc253aea2ecbe6b14dfddc58afcca6 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Sun, 26 May 2024 18:13:13 +0200 Subject: [PATCH 11/37] problem --- src/simplicial-hott/08-covariant.rzk.md | 57 ++++++++++++++++++++++++- 1 file changed, 56 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 54f5d15f..02cef205 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -513,6 +513,19 @@ Segal, then so is `Σ A, C`. ( \ t → k (t , t)) ``` +```rzk +#def dhom-to-hom-total-type + ( A : U) + ( x y : A) + ( f : hom A x y) + ( C : A → U) + ( u : C x) + ( v : C y) + ( ff : dhom A x y f C u v) + : hom (total-type A C) (x , u) (y , v) + := \ t → (f t , ff t) +``` + ```rzk #def dhom2-to-hom2-total-type ( A : U) @@ -539,7 +552,7 @@ Segal, then so is `Σ A, C`. ( \ t → (h t , hh t) , \ t → (α t , k t)) ``` -```rzk title="RS17, Remark 8.11" +```rzk #def hom2-total-type-to-dhom2 ( A : U) ( is-segal-A : is-segal A) @@ -565,6 +578,48 @@ Segal, then so is `Σ A, C`. ( \ t → first (k t) , ( \ t → first (kk t) , ( \ t → second (kk (t , t)) , \ t → second (kk t)))) +``` + +```rzk title="RS17, Remark 8.11" +#def dcomp uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w + := + dhom2-to-dhom A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg + -- I need something of type dhom A x z h C u w here + -- It crashed when I added the same thing as below, but with a first instead of a second in front + ( second (second (second (hom2-total-type-to-dhom2 + A is-segal-A x y z f g C is-covariant-C u v w ff gg + ( comp-is-segal + ( total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( x , u) (y , v) (z , w) + ( dhom-to-hom-total-type A x y f C u v ff) + ( dhom-to-hom-total-type A y z g C v w gg) + , witness-comp-is-segal + ( total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( x , u) (y , v) (z , w) + ( dhom-to-hom-total-type A x y f C u v ff) + ( dhom-to-hom-total-type A y z g C v w gg)))))) + +``` + +```rzk -- #def test uses (extext) -- ( A : U) -- ( is-segal-A : is-segal A) From b2de3fa4850ee4aa617fda17fe93680b0703ad05 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Sun, 26 May 2024 18:14:59 +0200 Subject: [PATCH 12/37] problem --- src/simplicial-hott/08-covariant.rzk.md | 1 - 1 file changed, 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 02cef205..0cabdcf8 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -598,7 +598,6 @@ Segal, then so is `Σ A, C`. := dhom2-to-dhom A x y z f g (comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg - -- I need something of type dhom A x z h C u w here -- It crashed when I added the same thing as below, but with a first instead of a second in front ( second (second (second (hom2-total-type-to-dhom2 A is-segal-A x y z f g C is-covariant-C u v w ff gg From 4917e1b71886bfad4520fbe07c87be951b6b7458 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Sun, 26 May 2024 18:37:11 +0200 Subject: [PATCH 13/37] nothing works --- src/simplicial-hott/08-covariant.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 0cabdcf8..b31a4dda 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -581,6 +581,7 @@ Segal, then so is `Σ A, C`. ``` ```rzk title="RS17, Remark 8.11" +--This probably doesn't work, same "being over comp f g" problems as the previous approach. #def dcomp uses (extext) ( A : U) ( is-segal-A : is-segal A) @@ -615,7 +616,6 @@ Segal, then so is `Σ A, C`. ( x , u) (y , v) (z , w) ( dhom-to-hom-total-type A x y f C u v ff) ( dhom-to-hom-total-type A y z g C v w gg)))))) - ``` ```rzk From 51ea1e9a78b0ee9af7d98875875256f9f5dc5353 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 28 May 2024 12:29:58 +0200 Subject: [PATCH 14/37] approach 3 --- src/simplicial-hott/08-covariant.rzk.md | 83 +++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index b31a4dda..6961a536 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -526,6 +526,89 @@ Segal, then so is `Σ A, C`. := \ t → (f t , ff t) ``` +```rzk +#def comp-total-type uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : hom (total-type A C) (x , u) (z , w) + := comp-is-segal + ( total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( x , u) (y , v) (z , w) + ( dhom-to-hom-total-type A x y f C u v ff) + ( dhom-to-hom-total-type A y z g C v w gg) +``` + +```rzk +#def proj-comp-total-type uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : hom A x z + := + \ t → first + ( comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg t) +``` + +```rzk +#def eq-comp-total-type uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) + =_{hom A x z} + ( comp-is-segal A is-segal-A x y z f g) + := U +``` + +```rzk +#def dhom-to-hom-total-type-to-comp + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w + := + U +``` + ```rzk #def dhom2-to-hom2-total-type ( A : U) From 3b771ec795132edf14c53655c1612e07bdc3eb72 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 28 May 2024 12:31:26 +0200 Subject: [PATCH 15/37] approach 3 --- src/simplicial-hott/08-covariant.rzk.md | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 6961a536..090b47c3 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -590,25 +590,6 @@ Segal, then so is `Σ A, C`. := U ``` -```rzk -#def dhom-to-hom-total-type-to-comp - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w - := - U -``` - ```rzk #def dhom2-to-hom2-total-type ( A : U) From 49aad7504339270f4def2fe9ed3af714f7214752 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 28 May 2024 15:07:32 +0200 Subject: [PATCH 16/37] new crash! --- src/simplicial-hott/08-covariant.rzk.md | 42 +++++++++++++++++++++++-- 1 file changed, 40 insertions(+), 2 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 090b47c3..5647998c 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -570,6 +570,42 @@ Segal, then so is `Σ A, C`. ( comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg t) ``` +```rzk +#def is-comp-proj-comp-total-type uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : hom2 A x y z f g + ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) + := + witness-comp-is-segal + ( total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( x , u) (y , v) (z , w) + ( dhom-to-hom-total-type A x y f C u v ff) + ( dhom-to-hom-total-type A y z g C v w gg) + + -- \ t → first + -- ( witness-comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg) t ) + -- This crashed. +``` + ```rzk #def eq-comp-total-type uses (extext) ( A : U) @@ -584,10 +620,12 @@ Segal, then so is `Σ A, C`. ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - : ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) + : ( comp-is-segal A is-segal-A x y z f g) =_{hom A x z} - ( comp-is-segal A is-segal-A x y z f g) + ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) := U +-- Strategy: Show in the previous statement that this is indeed a composition +-- and then just use uniqueness-comp-is-segal ``` ```rzk From 30115a2e698355a7ff93a3ed197f87141b50deb9 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 28 May 2024 15:12:54 +0200 Subject: [PATCH 17/37] Labeled the crashes --- src/simplicial-hott/08-covariant.rzk.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 5647998c..09715d06 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -701,7 +701,7 @@ Segal, then so is `Σ A, C`. := dhom2-to-dhom A x y z f g (comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg - -- It crashed when I added the same thing as below, but with a first instead of a second in front + -- This crashed when I added the same thing as below, but with a first instead of a second in front ( second (second (second (hom2-total-type-to-dhom2 A is-segal-A x y z f g C is-covariant-C u v w ff gg ( comp-is-segal @@ -771,13 +771,14 @@ Segal, then so is `Σ A, C`. -- ( gg : dhom A y z g C v w) -- : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w -- := --- second --- comp-is-segal +-- \ t → second +-- ( comp-is-segal -- ( total-type A C) -- ( is-segal-total-type-covariant-family-is-segal-base -- A C is-covariant-C is-segal-A) -- ( x , u) (y , v) (z , w) --- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) +-- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) t) +-- This crashed. ``` ## Covariant lifts, transport, and uniqueness From d6039a0f501b63c29393487cbb6aaeec40e2e3c1 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 29 May 2024 13:54:46 +0200 Subject: [PATCH 18/37] more problems --- src/simplicial-hott/08-covariant.rzk.md | 36 ++++++++++++------------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 09715d06..b03a83a6 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -584,25 +584,23 @@ Segal, then so is `Σ A, C`. ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - : hom2 A x y z f g - ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) - := - witness-comp-is-segal - ( total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - ( x , u) (y , v) (z , w) - ( dhom-to-hom-total-type A x y f C u v ff) - ( dhom-to-hom-total-type A y z g C v w gg) - - -- \ t → first - -- ( witness-comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg) t ) + : Σ ( h : hom A x z) , hom2 A x y z f g h + --( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) + := + -- ( \ t → first (comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg) t) + -- , \ t → first (witness-comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg))) -- This crashed. ``` From c4930c1a29bcf76018774812627275d6267f22bf Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 29 May 2024 18:53:11 +0200 Subject: [PATCH 19/37] crash again --- src/simplicial-hott/08-covariant.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index b03a83a6..95380350 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -600,7 +600,7 @@ Segal, then so is `Σ A, C`. -- A C is-covariant-C is-segal-A) -- ( x , u) (y , v) (z , w) -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg))) + -- ( dhom-to-hom-total-type A y z g C v w gg) t)) -- This crashed. ``` From 0bd1544cf9fc4683662bcf5571f6acdf1a61cc9d Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 5 Jun 2024 09:17:56 +0200 Subject: [PATCH 20/37] something works --- src/simplicial-hott/08-covariant.rzk.md | 296 ++++++++++++++++-------- 1 file changed, 201 insertions(+), 95 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 95380350..b206573d 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -470,60 +470,88 @@ Segal, then so is `Σ A, C`. ## Dependent composition ```rzk --- #def dhom-dhom-to-dhom2 --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( h : hom A x z) --- ( α : hom2 A x y z f g h) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- ( hh : dhom A x z h C u w) --- : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) --- , ( hom2 (total-type A C) (x , u) (y , v) (z , w) --- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) +#def dhom-to-hom-total-type + ( A : U) + ( x y : A) + ( f : hom A x y) + ( C : A → U) + ( u : C x) + ( v : C y) + ( ff : dhom A x y f C u v) + : hom (total-type A C) (x , u) (y , v) + := \ t → (f t , ff t) ``` ```rzk -#def dhom2-to-dhom +#def dhom-to-hom ( A : U) + ( x y : A) + ( f : hom A x y) + ( C : A → U) + ( u : C x) + ( v : C y) + ( ff : dhom A x y f C u v) + : hom A x y + := f +``` + +```rzk +#def dhom-to-hom-total-type-on-pairs + ( A : U) + ( is-segal-A : is-segal A) ( x y z : A) ( f : hom A x y) ( g : hom A y z) - ( h : hom A x z) - ( α : hom2 A x y z f g h) ( C : A → U) + ( is-covariant-C : is-covariant A C) ( u : C x) ( v : C y) ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - ( hh : dhom A x z h C u w) - : dhom2 A x y z f g h α C u v w ff gg hh - → dhom A x z h C u w + : product (hom (total-type A C) (x , u) (y , v)) + ( hom (total-type A C) (y , v) (z , w)) := - \ k → - ( \ t → k (t , t)) + ( ( dhom-to-hom-total-type A x y f C u v ff) + , ( dhom-to-hom-total-type A y z g C v w gg)) ``` ```rzk -#def dhom-to-hom-total-type +#def hom-total-type-to-dhom ( A : U) + ( is-segal-A : is-segal A) ( x y : A) ( f : hom A x y) ( C : A → U) + ( is-covariant-C : is-covariant A C) ( u : C x) ( v : C y) - ( ff : dhom A x y f C u v) - : hom (total-type A C) (x , u) (y , v) - := \ t → (f t , ff t) + : ( Σ ( k : hom (total-type A C) (x , u) (y , v)) + , ( ( \ t → first (k t)) =_{hom A x y} f)) + → dhom A x y f C u v + := \ (k , p) → + \ t → (transport (hom A x y) + ( \ g → dhom A x y g C u v) + ( \ t → first (k t)) f p (\ t → second (k t)) t) +``` + +```rzk +#def dhom-to-hom-total-type-over + ( A : U) + ( is-segal-A : is-segal A) + ( x y : A) + ( f : hom A x y) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( u : C x) + ( v : C y) + : dhom A x y f C u v + → ( Σ ( k : hom (total-type A C) (x , u) (y , v)) + , ( ( \ t → first (k t)) =_{hom A x y} f)) + := + \ ff → + ( dhom-to-hom-total-type A x y f C u v ff + , refl) ``` ```rzk @@ -541,7 +569,8 @@ Segal, then so is `Σ A, C`. ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) : hom (total-type A C) (x , u) (z , w) - := comp-is-segal + := + comp-is-segal ( total-type A C) ( is-segal-total-type-covariant-family-is-segal-base A C is-covariant-C is-segal-A) @@ -551,27 +580,51 @@ Segal, then so is `Σ A, C`. ``` ```rzk -#def proj-comp-total-type uses (extext) +-- #def dhom-dhom-to-dhom2 +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( h : hom A x z) +-- ( α : hom2 A x y z f g h) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- ( hh : dhom A x z h C u w) +-- : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) +-- , ( hom2 (total-type A C) (x , u) (y , v) (z , w) +-- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) +``` + +```rzk +#def dhom2-to-dhom ( A : U) - ( is-segal-A : is-segal A) ( x y z : A) ( f : hom A x y) ( g : hom A y z) + ( h : hom A x z) + ( α : hom2 A x y z f g h) ( C : A → U) - ( is-covariant-C : is-covariant A C) ( u : C x) ( v : C y) ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - : hom A x z + ( hh : dhom A x z h C u w) + : dhom2 A x y z f g h α C u v w ff gg hh + → dhom A x z h C u w := - \ t → first - ( comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg t) + \ k → + ( \ t → k (t , t)) ``` ```rzk -#def is-comp-proj-comp-total-type uses (extext) +#def proj-comp-total-type uses (extext) ( A : U) ( is-segal-A : is-segal A) ( x y z : A) @@ -584,9 +637,29 @@ Segal, then so is `Σ A, C`. ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - : Σ ( h : hom A x z) , hom2 A x y z f g h - --( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) + : hom A x z := + \ t → first + ( comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg t) +``` + +```rzk +-- #def is-comp-proj-comp-total-type uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : Σ ( h : hom A x z) , hom2 A x y z f g h + -- hom2 A x y z f g ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) + -- := -- ( \ t → first (comp-is-segal -- ( total-type A C) -- ( is-segal-total-type-covariant-family-is-segal-base @@ -605,23 +678,56 @@ Segal, then so is `Σ A, C`. ``` ```rzk -#def eq-comp-total-type uses (extext) - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : ( comp-is-segal A is-segal-A x y z f g) - =_{hom A x z} - ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) - := U +-- #def is-comp-proj-comp-total-type uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : Σ ( h : hom A x z) , hom2 A x y z f g h +-- := U + -- ( \ t → first (comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg) t) + -- , \ t → first (witness-comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg) t) + +``` + +```rzk +-- #def eq-comp-total-type uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : ( comp-is-segal A is-segal-A x y z f g) +-- =_{hom A x z} +-- ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) +-- := U -- Strategy: Show in the previous statement that this is indeed a composition -- and then just use uniqueness-comp-is-segal ``` @@ -680,43 +786,43 @@ Segal, then so is `Σ A, C`. , ( \ t → second (kk (t , t)) , \ t → second (kk t)))) ``` -```rzk title="RS17, Remark 8.11" ---This probably doesn't work, same "being over comp f g" problems as the previous approach. -#def dcomp uses (extext) - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w - := - dhom2-to-dhom A x y z f g (comp-is-segal A is-segal-A x y z f g) - ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg - -- This crashed when I added the same thing as below, but with a first instead of a second in front - ( second (second (second (hom2-total-type-to-dhom2 - A is-segal-A x y z f g C is-covariant-C u v w ff gg - ( comp-is-segal - ( total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - ( x , u) (y , v) (z , w) - ( dhom-to-hom-total-type A x y f C u v ff) - ( dhom-to-hom-total-type A y z g C v w gg) - , witness-comp-is-segal - ( total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - ( x , u) (y , v) (z , w) - ( dhom-to-hom-total-type A x y f C u v ff) - ( dhom-to-hom-total-type A y z g C v w gg)))))) -``` +-- ```rzk title="RS17, Remark 8.11" +-- --This probably doesn't work, same "being over comp f g" problems as the previous approach. +-- #def dcomp uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w +-- := +-- dhom2-to-dhom A x y z f g (comp-is-segal A is-segal-A x y z f g) +-- ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg +-- -- This crashed when I added the same thing as below, but with a first instead of a second in front +-- ( second (second (second (hom2-total-type-to-dhom2 +-- A is-segal-A x y z f g C is-covariant-C u v w ff gg +-- ( comp-is-segal +-- ( total-type A C) +-- ( is-segal-total-type-covariant-family-is-segal-base +-- A C is-covariant-C is-segal-A) +-- ( x , u) (y , v) (z , w) +-- ( dhom-to-hom-total-type A x y f C u v ff) +-- ( dhom-to-hom-total-type A y z g C v w gg) +-- , witness-comp-is-segal +-- ( total-type A C) +-- ( is-segal-total-type-covariant-family-is-segal-base +-- A C is-covariant-C is-segal-A) +-- ( x , u) (y , v) (z , w) +-- ( dhom-to-hom-total-type A x y f C u v ff) +-- ( dhom-to-hom-total-type A y z g C v w gg)))))) +-- ``` ```rzk -- #def test uses (extext) From 2d67a0ba98668a7f6073f09fa92ed19056d79c3c Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Thu, 6 Jun 2024 22:38:14 +0200 Subject: [PATCH 21/37] new crashes dropped --- src/simplicial-hott/08-covariant.rzk.md | 281 +++++++++++++++--------- 1 file changed, 179 insertions(+), 102 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index b206573d..ed0ab1cf 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -509,7 +509,8 @@ Segal, then so is `Σ A, C`. ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - : product (hom (total-type A C) (x , u) (y , v)) + : product + ( hom (total-type A C) (x , u) (y , v)) ( hom (total-type A C) (y , v) (z , w)) := ( ( dhom-to-hom-total-type A x y f C u v ff) @@ -530,9 +531,11 @@ Segal, then so is `Σ A, C`. , ( ( \ t → first (k t)) =_{hom A x y} f)) → dhom A x y f C u v := \ (k , p) → - \ t → (transport (hom A x y) - ( \ g → dhom A x y g C u v) - ( \ t → first (k t)) f p (\ t → second (k t)) t) + \ t → + ( transport + ( hom A x y) + ( \ g → dhom A x y g C u v) + ( \ t → first (k t)) f p (\ t → second (k t)) t) ``` ```rzk @@ -555,72 +558,50 @@ Segal, then so is `Σ A, C`. ``` ```rzk -#def comp-total-type uses (extext) +#def is-over-dhom-to-hom-total-type ( A : U) ( is-segal-A : is-segal A) - ( x y z : A) + ( x y : A) ( f : hom A x y) - ( g : hom A y z) ( C : A → U) ( is-covariant-C : is-covariant A C) ( u : C x) ( v : C y) - ( w : C z) ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : hom (total-type A C) (x , u) (z , w) - := - comp-is-segal - ( total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - ( x , u) (y , v) (z , w) - ( dhom-to-hom-total-type A x y f C u v ff) - ( dhom-to-hom-total-type A y z g C v w gg) -``` - -```rzk --- #def dhom-dhom-to-dhom2 --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( h : hom A x z) --- ( α : hom2 A x y z f g h) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- ( hh : dhom A x z h C u w) --- : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) --- , ( hom2 (total-type A C) (x , u) (y , v) (z , w) --- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) + : ( \ t → first (dhom-to-hom-total-type A x y f C u v ff t)) =_{hom A x y} f + := refl ``` ```rzk -#def dhom2-to-dhom +#def comp-total-type uses (extext) ( A : U) + ( is-segal-A : is-segal A) ( x y z : A) ( f : hom A x y) ( g : hom A y z) - ( h : hom A x z) - ( α : hom2 A x y z f g h) ( C : A → U) + ( is-covariant-C : is-covariant A C) ( u : C x) ( v : C y) ( w : C z) ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) - ( hh : dhom A x z h C u w) - : dhom2 A x y z f g h α C u v w ff gg hh - → dhom A x z h C u w + : hom (total-type A C) (x , u) (z , w) := - \ k → - ( \ t → k (t , t)) + -- \ t → (witness-comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg) (t , t)) + comp-is-segal + ( total-type A C) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( x , u) (y , v) (z , w) + ( dhom-to-hom-total-type A x y f C u v ff) + ( dhom-to-hom-total-type A y z g C v w gg) ``` ```rzk @@ -657,24 +638,74 @@ Segal, then so is `Σ A, C`. -- ( w : C z) -- ( ff : dhom A x y f C u v) -- ( gg : dhom A y z g C v w) --- : Σ ( h : hom A x z) , hom2 A x y z f g h - -- hom2 A x y z f g ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) - -- := - -- ( \ t → first (comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg) t) - -- , \ t → first (witness-comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg) t)) - -- This crashed. +-- : ( ( t₁ , t₂) : Δ²) → A +-- [ t₂ ≡ 0₂ ↦ f t₁ +-- , t₁ ≡ 1₂ ↦ g t₂ +-- , t₂ ≡ t₁ ↦ (proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) t₂ +-- ] +-- hom2 A x y z f g +-- ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) +-- := +-- \ (t₁ , t₂) → +-- ( first (witness-comp-is-segal +-- ( total-type A C) +-- ( is-segal-total-type-covariant-family-is-segal-base +-- A C is-covariant-C is-segal-A) +-- ( x , u) (y , v) (z , w) +-- ( dhom-to-hom-total-type A x y f C u v ff) +-- ( dhom-to-hom-total-type A y z g C v w gg) (t₁ , t₂))) +``` + +```rzk +-- #def is-comp-proj-comp-total-type uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : hom2 A x y z f g +-- ( \ t → first +-- ( comp-is-segal +-- ( total-type A C) +-- ( is-segal-total-type-covariant-family-is-segal-base +-- A C is-covariant-C is-segal-A) +-- ( x , u) (y , v) (z , w) +-- ( \ r → (f r , ff r)) +-- ( \ s → (g s , gg s)) t)) +-- := +-- \ (t₁ , t₂) → +-- ( first (witness-comp-is-segal +-- ( total-type A C) +-- ( is-segal-total-type-covariant-family-is-segal-base +-- A C is-covariant-C is-segal-A) +-- ( x , u) (y , v) (z , w) +-- ( \ r → (f r , ff r)) +-- ( \ s → (g s , gg s)) (t₁ , t₂))) + +-- The thing above but unfolded, also crashes +``` + +```rzk +#def test-comp + ( A : U) + ( is-segal-A : is-segal A) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + : ( ( t₁ , t₂) : Δ²) → A + [ t₂ ≡ 0₂ ↦ f t₁ + , t₁ ≡ 1₂ ↦ g t₂ + , t₂ ≡ t₁ ↦ (comp-is-segal A is-segal-A x y z f g) t₂ + ] + := + witness-comp-is-segal A is-segal-A x y z f g ``` ```rzk @@ -707,7 +738,6 @@ Segal, then so is `Σ A, C`. -- ( x , u) (y , v) (z , w) -- ( dhom-to-hom-total-type A x y f C u v ff) -- ( dhom-to-hom-total-type A y z g C v w gg) t) - ``` ```rzk @@ -732,6 +762,51 @@ Segal, then so is `Σ A, C`. -- and then just use uniqueness-comp-is-segal ``` +```rzk +-- #def dhom-dhom-to-dhom2 +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( h : hom A x z) +-- ( α : hom2 A x y z f g h) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- ( hh : dhom A x z h C u w) +-- : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) +-- , ( hom2 (total-type A C) (x , u) (y , v) (z , w) +-- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) +``` + +```rzk +#def dhom2-to-dhom + ( A : U) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( h : hom A x z) + ( α : hom2 A x y z f g h) + ( C : A → U) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + ( hh : dhom A x z h C u w) + : dhom2 A x y z f g h α C u v w ff gg hh + → dhom A x z h C u w + := + \ k → + \ t → + k (t , t) +``` + ```rzk #def dhom2-to-hom2-total-type ( A : U) @@ -747,15 +822,16 @@ Segal, then so is `Σ A, C`. ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) : ( Σ ( h : hom A x z) - , Σ ( α : hom2 A x y z f g h) - , ( Σ ( hh : dhom A x z h C u w) - , dhom2 A x y z f g h α C u v w ff gg hh)) + , Σ ( α : hom2 A x y z f g h) + , ( Σ ( hh : dhom A x z h C u w) + , dhom2 A x y z f g h α C u v w ff gg hh)) → ( Σ ( k : hom (total-type A C) (x , u) (z , w)) - , ( hom2 (total-type A C) (x , u) (y , v) (z , w) - ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) + , ( hom2 (total-type A C) (x , u) (y , v) (z , w) + ( dhom-to-hom-total-type A x y f C u v ff) + ( dhom-to-hom-total-type A y z g C v w gg) k)) := \ (h , (α , (hh , k))) → - ( \ t → (h t , hh t) , \ t → (α t , k t)) + ( dhom-to-hom-total-type A x z h C u w hh , \ t → (α t , k t)) ``` ```rzk @@ -773,21 +849,22 @@ Segal, then so is `Σ A, C`. ( ff : dhom A x y f C u v) ( gg : dhom A y z g C v w) : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) - , ( hom2 (total-type A C) (x , u) (y , v) (z , w) - ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) - → Σ ( h : hom A x z) - , Σ ( α : hom2 A x y z f g h) - , ( Σ ( hh : dhom A x z h C u w) - , dhom2 A x y z f g h α C u v w ff gg hh) + , ( hom2 (total-type A C) (x , u) (y , v) (z , w) + ( dhom-to-hom-total-type A x y f C u v ff) + ( dhom-to-hom-total-type A y z g C v w gg) k)) + → Σ ( h : hom A x z) + , Σ ( α : hom2 A x y z f g h) + , ( Σ ( hh : dhom A x z h C u w) + , dhom2 A x y z f g h α C u v w ff gg hh) := \ (k , kk) → - ( \ t → first (k t) - , ( \ t → first (kk t) - , ( \ t → second (kk (t , t)) , \ t → second (kk t)))) + ( \ t → first (k t) + , ( \ t → first (kk t) + , ( \ t → second (kk (t , t)) , \ t → second (kk t)))) ``` --- ```rzk title="RS17, Remark 8.11" --- --This probably doesn't work, same "being over comp f g" problems as the previous approach. +```rzk title="RS17, Remark 8.11" +--This probably doesn't work, same "being over comp f g" problems as the previous approach. -- #def dcomp uses (extext) -- ( A : U) -- ( is-segal-A : is-segal A) @@ -805,24 +882,24 @@ Segal, then so is `Σ A, C`. -- := -- dhom2-to-dhom A x y z f g (comp-is-segal A is-segal-A x y z f g) -- ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg --- -- This crashed when I added the same thing as below, but with a first instead of a second in front --- ( second (second (second (hom2-total-type-to-dhom2 --- A is-segal-A x y z f g C is-covariant-C u v w ff gg --- ( comp-is-segal --- ( total-type A C) --- ( is-segal-total-type-covariant-family-is-segal-base --- A C is-covariant-C is-segal-A) --- ( x , u) (y , v) (z , w) --- ( dhom-to-hom-total-type A x y f C u v ff) --- ( dhom-to-hom-total-type A y z g C v w gg) --- , witness-comp-is-segal --- ( total-type A C) --- ( is-segal-total-type-covariant-family-is-segal-base --- A C is-covariant-C is-segal-A) --- ( x , u) (y , v) (z , w) --- ( dhom-to-hom-total-type A x y f C u v ff) --- ( dhom-to-hom-total-type A y z g C v w gg)))))) --- ``` + -- This crashed when I added the same thing as below, but with a first instead of a second in front + -- ( second (second (second (hom2-total-type-to-dhom2 + -- A is-segal-A x y z f g C is-covariant-C u v w ff gg + -- ( comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg) + -- , witness-comp-is-segal + -- ( total-type A C) + -- ( is-segal-total-type-covariant-family-is-segal-base + -- A C is-covariant-C is-segal-A) + -- ( x , u) (y , v) (z , w) + -- ( dhom-to-hom-total-type A x y f C u v ff) + -- ( dhom-to-hom-total-type A y z g C v w gg)))))) +``` ```rzk -- #def test uses (extext) From f4b7a8981330050c0847893930ae85e0e0266ec9 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Sun, 16 Jun 2024 15:37:07 +0200 Subject: [PATCH 22/37] modified 06-contractible --- .vscode/settings.json | 3 +- src/hott/06-contractible.rzk.md | 179 +++++++++++++++++++++++- src/simplicial-hott/08-covariant.rzk.md | 40 +++++- 3 files changed, 210 insertions(+), 12 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index ffa59b7e..25d32da2 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -62,5 +62,6 @@ "editor.detectIndentation": false, "editor.insertSpaces": true }, - "rzk.format.enable": true + "rzk.format.enable": true, + "agdaMode.connection.agdaLanguageServer": true } diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index 7b94d7c9..7664eb6c 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -59,6 +59,9 @@ This is a literate `rzk` file: #end contractible-data ``` + + + ## Unit type The prototypical contractible type is the unit type, which is built-in to rzk. @@ -224,10 +227,6 @@ A retract of contractible types is contractible. #end is-contr-is-retract-of-is-contr ``` -```rzk - -``` - ## Functions between contractible types ```rzk title="Any function between contractible types is an equivalence" @@ -553,3 +552,175 @@ together the two identifications to the out and back path. ( path-eq-path-through-center-is-contr A is-contr-A x y p)) ( path-eq-path-through-center-is-contr A is-contr-A x y q) ``` + +## Total type over a contractible type + +We prove that a ∑-type with contractible base is equivalent to the dependent +type evaluated at the point of contraction. + +```rzk +#def sigma-is-contr-base-1 + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + : + ( C (center-contraction A is-contr-A)) + → ( Σ ( x : A) , C x) + := + \ v → ((center-contraction A is-contr-A) , v) +``` + +```rzk +#def sigma-is-contr-base-2 + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + : + ( Σ ( x : A) , C x) + → ( C (center-contraction A is-contr-A)) + := + \ (x , u) → + transport + A + C + x + ( center-contraction A is-contr-A) + ( rev + A + ( center-contraction A is-contr-A) + x + ( homotopy-contraction A is-contr-A x)) + u +``` + +```rzk +#def has-retraction-sigma-is-contr-base + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + : has-retraction + ( Σ ( x : A) , C x) + ( C (center-contraction A is-contr-A)) + ( sigma-is-contr-base-2 A is-contr-A C) + := + ( ( sigma-is-contr-base-1 A is-contr-A C) + , \ (x , u) → + ( rev (Σ (x : A) , C x) + ( x , u) + ( sigma-is-contr-base-1 A is-contr-A C + ( sigma-is-contr-base-2 A is-contr-A C (x , u))) + ( transport-lift A C + ( x) + ( center-contraction A is-contr-A) + ( rev + ( A) + ( center-contraction A is-contr-A) + ( x) + ( homotopy-contraction A is-contr-A x)) + u))) +``` + +```rzk +#def test2 + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + ( u : C (center-contraction A is-contr-A)) + : transport A C + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( first-path-Σ A C (center-contraction A is-contr-A , u) + ( center-contraction A is-contr-A , u) + ( refl)) + ( u) =_{ C (center-contraction A is-contr-A) } + ( u) + := + second-path-Σ A C + ( ( center-contraction A is-contr-A) , u) + ( ( center-contraction A is-contr-A) , u) + refl +``` + +```rzk +#def test3 + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + ( u : C (center-contraction A is-contr-A)) + : ( sigma-is-contr-base-2 A is-contr-A C + ( sigma-is-contr-base-1 A is-contr-A C u)) + =_{ C (center-contraction A is-contr-A) } + ( transport A C + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( first-path-Σ A C (center-contraction A is-contr-A , u) + ( center-contraction A is-contr-A , u) + ( refl)) + ( u)) + := + transport2 + ( A) + ( C) + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( rev + A + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( homotopy-contraction A is-contr-A (center-contraction A is-contr-A))) + ( refl) + ( all-paths-equal-is-contr + ( A) + ( is-contr-A) + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( rev + A + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( homotopy-contraction A is-contr-A (center-contraction A is-contr-A))) + ( refl)) + u +``` + +```rzk +#def has-section-sigma-is-contr-base + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + : has-section + ( Σ ( x : A) , C x) + ( C (center-contraction A is-contr-A)) + ( sigma-is-contr-base-2 A is-contr-A C) + := + ( ( sigma-is-contr-base-1 A is-contr-A C) + , \ u → + ( concat + ( C (center-contraction A is-contr-A)) + ( sigma-is-contr-base-2 A is-contr-A C + ( sigma-is-contr-base-1 A is-contr-A C u)) + ( transport A C + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( first-path-Σ A C (center-contraction A is-contr-A , u) + ( center-contraction A is-contr-A , u) + ( refl)) + ( u)) + ( u) + ( test3 A is-contr-A C u) + ( test2 A is-contr-A C u))) +``` + +```rzk +#def equiv-sigma-is-contr-base + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + : Equiv + ( Σ ( x : A) , C x) + ( C (center-contraction A is-contr-A)) + := + ( ( sigma-is-contr-base-2 A is-contr-A C) + , ( ( ( has-retraction-sigma-is-contr-base A is-contr-A C) + , ( has-section-sigma-is-contr-base A is-contr-A C)))) +``` diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index ed0ab1cf..3eb662b7 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -467,6 +467,7 @@ Segal, then so is `Σ A, C`. ( is-naive-left-fibration-is-covariant A C is-covariant-C)) ``` + ## Dependent composition ```rzk @@ -638,12 +639,38 @@ Segal, then so is `Σ A, C`. -- ( w : C z) -- ( ff : dhom A x y f C u v) -- ( gg : dhom A y z g C v w) --- : ( ( t₁ , t₂) : Δ²) → A --- [ t₂ ≡ 0₂ ↦ f t₁ --- , t₁ ≡ 1₂ ↦ g t₂ --- , t₂ ≡ t₁ ↦ (proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) t₂ --- ] --- hom2 A x y z f g +-- : +-- hom2 (total-type A C) (x , u) (y , v) (z , w) +-- ( dhom-to-hom-total-type A x y f C u v ff) +-- ( dhom-to-hom-total-type A y z g C v w gg) +-- ( comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) +-- := +-- witness-comp-is-segal +-- ( total-type A C) +-- ( is-segal-total-type-covariant-family-is-segal-base +-- A C is-covariant-C is-segal-A) +-- ( x , u) (y , v) (z , w) +-- ( dhom-to-hom-total-type A x y f C u v ff) +-- ( dhom-to-hom-total-type A y z g C v w gg) +``` + +```rzk +-- #set-option "max-whnf-depth" = "20" +-- #def is-comp-proj-comp-total-type uses (extext) +-- ( A : U) +-- ( is-segal-A : is-segal A) +-- ( x y z : A) +-- ( f : hom A x y) +-- ( g : hom A y z) +-- ( C : A → U) +-- ( is-covariant-C : is-covariant A C) +-- ( u : C x) +-- ( v : C y) +-- ( w : C z) +-- ( ff : dhom A x y f C u v) +-- ( gg : dhom A y z g C v w) +-- : +-- hom2 A x y z f g -- ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) -- := -- \ (t₁ , t₂) → @@ -980,7 +1007,6 @@ along an arrow f : hom A x y to give a term in C y. first (center-contraction (dhom-from A x y f C u) (is-covariant-C x y f u)) ``` - ## Representable covariant families If `A` is a Segal type and `a : A` is any term, then `hom A a` defines a From b8888fd9839f6ea5e5eb816b2cab40aebcf655b7 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Sun, 16 Jun 2024 15:40:38 +0200 Subject: [PATCH 23/37] looks better --- src/hott/06-contractible.rzk.md | 33 +++++++++++++++------------------ 1 file changed, 15 insertions(+), 18 deletions(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index 7664eb6c..b1867f4c 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -59,9 +59,6 @@ This is a literate `rzk` file: #end contractible-data ``` - - - ## Unit type The prototypical contractible type is the unit type, which is built-in to rzk. @@ -581,16 +578,16 @@ type evaluated at the point of contraction. := \ (x , u) → transport - A - C - x + ( A) + ( C) + ( x) ( center-contraction A is-contr-A) ( rev - A + ( A) ( center-contraction A is-contr-A) - x + ( x) ( homotopy-contraction A is-contr-A x)) - u + ( u) ``` ```rzk @@ -664,7 +661,7 @@ type evaluated at the point of contraction. ( center-contraction A is-contr-A) ( center-contraction A is-contr-A) ( rev - A + ( A) ( center-contraction A is-contr-A) ( center-contraction A is-contr-A) ( homotopy-contraction A is-contr-A (center-contraction A is-contr-A))) @@ -675,12 +672,12 @@ type evaluated at the point of contraction. ( center-contraction A is-contr-A) ( center-contraction A is-contr-A) ( rev - A - ( center-contraction A is-contr-A) - ( center-contraction A is-contr-A) - ( homotopy-contraction A is-contr-A (center-contraction A is-contr-A))) - ( refl)) - u + ( A) + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( homotopy-contraction A is-contr-A (center-contraction A is-contr-A))) + ( refl)) + ( u) ``` ```rzk @@ -703,8 +700,8 @@ type evaluated at the point of contraction. ( center-contraction A is-contr-A) ( center-contraction A is-contr-A) ( first-path-Σ A C (center-contraction A is-contr-A , u) - ( center-contraction A is-contr-A , u) - ( refl)) + ( center-contraction A is-contr-A , u) + ( refl)) ( u)) ( u) ( test3 A is-contr-A C u) From 56bb0d92092706ccce7c47690ab67f9bc59ce434 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Sun, 16 Jun 2024 16:23:16 +0200 Subject: [PATCH 24/37] contractible over sum type --- src/hott/06-contractible.rzk.md | 134 ++++++++++++-------------------- 1 file changed, 50 insertions(+), 84 deletions(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index b1867f4c..d26be1af 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -552,23 +552,23 @@ together the two identifications to the out and back path. ## Total type over a contractible type -We prove that a ∑-type with contractible base is equivalent to the dependent +We show that a ∑-type with contractible base is equivalent to the dependent type evaluated at the point of contraction. ```rzk -#def sigma-is-contr-base-1 +#def second-center-to-total-type-is-contr-base ( A : U) ( is-contr-A : is-contr A) ( C : A → U) : ( C (center-contraction A is-contr-A)) - → ( Σ ( x : A) , C x) + → ( Σ ( x : A) , C x) := \ v → ((center-contraction A is-contr-A) , v) ``` ```rzk -#def sigma-is-contr-base-2 +#def total-type-to-second-center-is-contr-base ( A : U) ( is-contr-A : is-contr A) ( C : A → U) @@ -591,21 +591,21 @@ type evaluated at the point of contraction. ``` ```rzk -#def has-retraction-sigma-is-contr-base +#def has-retraction-total-type-to-second-center-is-contr-base ( A : U) ( is-contr-A : is-contr A) ( C : A → U) : has-retraction ( Σ ( x : A) , C x) ( C (center-contraction A is-contr-A)) - ( sigma-is-contr-base-2 A is-contr-A C) + ( total-type-to-second-center-is-contr-base A is-contr-A C) := - ( ( sigma-is-contr-base-1 A is-contr-A C) + ( ( second-center-to-total-type-is-contr-base A is-contr-A C) , \ (x , u) → ( rev (Σ (x : A) , C x) ( x , u) - ( sigma-is-contr-base-1 A is-contr-A C - ( sigma-is-contr-base-2 A is-contr-A C (x , u))) + ( second-center-to-total-type-is-contr-base A is-contr-A C + ( total-type-to-second-center-is-contr-base A is-contr-A C (x , u))) ( transport-lift A C ( x) ( center-contraction A is-contr-A) @@ -614,88 +614,25 @@ type evaluated at the point of contraction. ( center-contraction A is-contr-A) ( x) ( homotopy-contraction A is-contr-A x)) - u))) + ( u)))) ``` ```rzk -#def test2 - ( A : U) - ( is-contr-A : is-contr A) - ( C : A → U) - ( u : C (center-contraction A is-contr-A)) - : transport A C - ( center-contraction A is-contr-A) - ( center-contraction A is-contr-A) - ( first-path-Σ A C (center-contraction A is-contr-A , u) - ( center-contraction A is-contr-A , u) - ( refl)) - ( u) =_{ C (center-contraction A is-contr-A) } - ( u) - := - second-path-Σ A C - ( ( center-contraction A is-contr-A) , u) - ( ( center-contraction A is-contr-A) , u) - refl -``` - -```rzk -#def test3 - ( A : U) - ( is-contr-A : is-contr A) - ( C : A → U) - ( u : C (center-contraction A is-contr-A)) - : ( sigma-is-contr-base-2 A is-contr-A C - ( sigma-is-contr-base-1 A is-contr-A C u)) - =_{ C (center-contraction A is-contr-A) } - ( transport A C - ( center-contraction A is-contr-A) - ( center-contraction A is-contr-A) - ( first-path-Σ A C (center-contraction A is-contr-A , u) - ( center-contraction A is-contr-A , u) - ( refl)) - ( u)) - := - transport2 - ( A) - ( C) - ( center-contraction A is-contr-A) - ( center-contraction A is-contr-A) - ( rev - ( A) - ( center-contraction A is-contr-A) - ( center-contraction A is-contr-A) - ( homotopy-contraction A is-contr-A (center-contraction A is-contr-A))) - ( refl) - ( all-paths-equal-is-contr - ( A) - ( is-contr-A) - ( center-contraction A is-contr-A) - ( center-contraction A is-contr-A) - ( rev - ( A) - ( center-contraction A is-contr-A) - ( center-contraction A is-contr-A) - ( homotopy-contraction A is-contr-A (center-contraction A is-contr-A))) - ( refl)) - ( u) -``` - -```rzk -#def has-section-sigma-is-contr-base +#def has-section-total-type-to-second-center-is-contr-base ( A : U) ( is-contr-A : is-contr A) ( C : A → U) : has-section ( Σ ( x : A) , C x) ( C (center-contraction A is-contr-A)) - ( sigma-is-contr-base-2 A is-contr-A C) + ( total-type-to-second-center-is-contr-base A is-contr-A C) := - ( ( sigma-is-contr-base-1 A is-contr-A C) + ( ( second-center-to-total-type-is-contr-base A is-contr-A C) , \ u → ( concat ( C (center-contraction A is-contr-A)) - ( sigma-is-contr-base-2 A is-contr-A C - ( sigma-is-contr-base-1 A is-contr-A C u)) + ( total-type-to-second-center-is-contr-base A is-contr-A C + ( second-center-to-total-type-is-contr-base A is-contr-A C u)) ( transport A C ( center-contraction A is-contr-A) ( center-contraction A is-contr-A) @@ -704,12 +641,39 @@ type evaluated at the point of contraction. ( refl)) ( u)) ( u) - ( test3 A is-contr-A C u) - ( test2 A is-contr-A C u))) + ( transport2 + ( A) + ( C) + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( rev + ( A) + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( homotopy-contraction A is-contr-A + ( center-contraction A is-contr-A))) + ( refl) + ( all-paths-equal-is-contr + ( A) + ( is-contr-A) + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( rev + ( A) + ( center-contraction A is-contr-A) + ( center-contraction A is-contr-A) + ( homotopy-contraction A is-contr-A + ( center-contraction A is-contr-A))) + ( refl)) + ( u)) + ( second-path-Σ A C + ( ( center-contraction A is-contr-A) , u) + ( ( center-contraction A is-contr-A) , u) + ( refl)))) ``` ```rzk -#def equiv-sigma-is-contr-base +#def equiv-total-type-second-center-is-contr-base ( A : U) ( is-contr-A : is-contr A) ( C : A → U) @@ -717,7 +681,9 @@ type evaluated at the point of contraction. ( Σ ( x : A) , C x) ( C (center-contraction A is-contr-A)) := - ( ( sigma-is-contr-base-2 A is-contr-A C) - , ( ( ( has-retraction-sigma-is-contr-base A is-contr-A C) - , ( has-section-sigma-is-contr-base A is-contr-A C)))) + ( ( total-type-to-second-center-is-contr-base A is-contr-A C) + , ( ( ( has-retraction-total-type-to-second-center-is-contr-base + A is-contr-A C) + , ( has-section-total-type-to-second-center-is-contr-base + A is-contr-A C)))) ``` From 15e947d590c25007c947693e67034d0dba92cd73 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 18 Jun 2024 11:10:27 +0200 Subject: [PATCH 25/37] formatting --- src/hott/06-contractible.rzk.md | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index d26be1af..03a6fa3a 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -552,16 +552,15 @@ together the two identifications to the out and back path. ## Total type over a contractible type -We show that a ∑-type with contractible base is equivalent to the dependent -type evaluated at the point of contraction. +We show that a ∑-type with contractible base is equivalent to the dependent type +evaluated at the point of contraction. ```rzk #def second-center-to-total-type-is-contr-base ( A : U) ( is-contr-A : is-contr A) ( C : A → U) - : - ( C (center-contraction A is-contr-A)) + : ( C (center-contraction A is-contr-A)) → ( Σ ( x : A) , C x) := \ v → ((center-contraction A is-contr-A) , v) @@ -572,8 +571,7 @@ type evaluated at the point of contraction. ( A : U) ( is-contr-A : is-contr A) ( C : A → U) - : - ( Σ ( x : A) , C x) + : ( Σ ( x : A) , C x) → ( C (center-contraction A is-contr-A)) := \ (x , u) → @@ -684,6 +682,6 @@ type evaluated at the point of contraction. ( ( total-type-to-second-center-is-contr-base A is-contr-A C) , ( ( ( has-retraction-total-type-to-second-center-is-contr-base A is-contr-A C) - , ( has-section-total-type-to-second-center-is-contr-base + , ( has-section-total-type-to-second-center-is-contr-base A is-contr-A C)))) ``` From 19b1fef6fa3ae32466a8f7a87b2669973dad7086 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Tue, 18 Jun 2024 11:18:03 +0200 Subject: [PATCH 26/37] formatting --- src/hott/06-contractible.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index 03a6fa3a..964b742d 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -550,7 +550,7 @@ together the two identifications to the out and back path. ( path-eq-path-through-center-is-contr A is-contr-A x y q) ``` -## Total type over a contractible type +## Total type over a contractible base type We show that a ∑-type with contractible base is equivalent to the dependent type evaluated at the point of contraction. From 999e8d8abb53ce5d6a652cc608be2efd556a3570 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 19 Jun 2024 09:10:25 +0200 Subject: [PATCH 27/37] dependent comp --- src/simplicial-hott/08-covariant.rzk.md | 154 ++++++++++++++++++++++++ 1 file changed, 154 insertions(+) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 3eb662b7..5f71223e 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -470,6 +470,160 @@ Segal, then so is `Σ A, C`. ## Dependent composition +```rzk +-- Here is a path way to solve the problem. It includes the problem you are already working on. +#def has-unique-inner-extensions-is-segal-case uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + : has-unique-extensions (2 × 2) Δ² (\ t → Λ t) (Σ (x : A) , C x) + := U + -- Hint: use has-unique-inner-extensions-is-segal + + +#def has-unique-inner-extensions-is-segal-case-consequence uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( a : (t : Λ) → A) + ( c : (t : Λ) → C (a t)) + : is-contr ((t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) + := U + +#def axiom-choice-case + ( A : U) + ( C : A → U) + ( a : (t : Λ) → A) + ( c : (t : Λ) → C (a t)) + : Equiv + ( ( t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) + ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) + , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) + := U + +#def axiom-choice-case-consequence uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( a : (t : Λ) → A) + ( c : (t : Λ) → C (a t)) + : is-contr + ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) + , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) + := U +-- Hint: Use is-contr-equiv-is-contr + + +-- This one I think you are already working on. +-- If you have it in some other file then delete this. +#def equiv-sigma-is-contr-base + ( A : U) + ( is-contr-A : is-contr A) + ( C : A → U) + : Equiv + ( Σ ( x : A) , C x) + ( C (center-contraction A is-contr A)) + := U + +#def equiv-ext-is-segal-base + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( a : (t : Λ) → A) + ( c : (t : Λ) → C (a t)) + : Equiv + ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) + , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) + ( ( t : Δ²) + → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) + ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) + := U + -- Hint: Use the last exercise. This one is hard! + +#def is-contr-horn-ext-is-covariant uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( a : (t : Λ) → A) + ( c : (t : Λ) → C (a t)) + : is-contr + ( ( t : Δ²) + → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) + ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) + := U + -- Hint: Start from is-contr-equiv-is-contr + -- You also need: + -- equiv-ext-is-segal-base + -- quiv-sigma-is-contr-base + -- axiom-choice-case-consequence + +#def dhorn + ( A : U) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( C : A → U) + ( u : C x) + ( v : C y) + ( w : C z) + ( k : dhom A x y f C u v) + ( m : dhom A y z g C v w) + : ( ( t : Λ) → C (horn A x y z f g t)) + := U + -- Hint: Use recOR from one of the first files. + +#def compositions-are-dhorn-fillings + ( A : U) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( h : hom A x z) + ( α : hom2 A x y z f g h) + ( C : A → U) + ( u : C x) + ( v : C y) + ( w : C z) + ( k : dhom A x y f C u v) + ( m : dhom A y z g C v w) + : Equiv + ( Σ ( n : dhom A x z h C u w) + , ( dhom2 A x y z f g h α C u v w k m n)) + ( ( t : Δ²) → C (α t) + [Λ t ↦ dhorn A x y z f g C u v w k m t]) + := U + +#def is-contr-ext-is-covariant uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( u : C x) + ( v : C y) + ( w : C z) + ( k : dhom A x y f C u v) + ( m : dhom A y z g C v w) + : is-contr + ( Σ ( n : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) + , dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w k m n) + := U + -- Hint: Use is-contr-equiv-is-contr' and the previous results. + -- Again you need equiv-sigma-is-contr-base + + +-- What is missing: a term that extracts the composition from the contractibility! +``` + +## Dependent composition try + + ```rzk #def dhom-to-hom-total-type ( A : U) From ac57b2be056f68800bfe5c884aba3b4ea922d7b7 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 19 Jun 2024 13:52:58 +0200 Subject: [PATCH 28/37] start --- src/simplicial-hott/08-covariant.rzk.md | 32 +++++++++++++++---------- 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 5f71223e..2f5e9509 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -478,9 +478,11 @@ Segal, then so is `Σ A, C`. ( C : A → U) ( is-covariant-C : is-covariant A C) : has-unique-extensions (2 × 2) Δ² (\ t → Λ t) (Σ (x : A) , C x) - := U - -- Hint: use has-unique-inner-extensions-is-segal - + := + has-unique-inner-extensions-is-segal + ( Σ ( x : A) , C x) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) #def has-unique-inner-extensions-is-segal-case-consequence uses (extext) ( A : U) @@ -490,7 +492,13 @@ Segal, then so is `Σ A, C`. ( a : (t : Λ) → A) ( c : (t : Λ) → C (a t)) : is-contr ((t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) - := U + := + has-unique-inner-extensions-is-segal-case + ( A) + ( is-segal-A) + ( C) + ( is-covariant-C) + ( \ t → (a t , c t)) #def axiom-choice-case ( A : U) @@ -519,14 +527,14 @@ Segal, then so is `Σ A, C`. -- This one I think you are already working on. -- If you have it in some other file then delete this. -#def equiv-sigma-is-contr-base - ( A : U) - ( is-contr-A : is-contr A) - ( C : A → U) - : Equiv - ( Σ ( x : A) , C x) - ( C (center-contraction A is-contr A)) - := U +-- #def equiv-sigma-is-contr-base +-- ( A : U) +-- ( is-contr-A : is-contr A) +-- ( C : A → U) +-- : Equiv +-- ( Σ ( x : A) , C x) +-- ( C (center-contraction A is-contr A)) +-- := U #def equiv-ext-is-segal-base ( A : U) From 2315266f6061fa1e88a2aa2538b84f1bd363d3e7 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Wed, 19 Jun 2024 23:48:40 +0200 Subject: [PATCH 29/37] progress --- src/simplicial-hott/08-covariant.rzk.md | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 2f5e9509..e660ee07 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -509,7 +509,15 @@ Segal, then so is `Σ A, C`. ( ( t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) - := U + := + axiom-choice + ( 2 × 2) + ( Δ²) + ( \ t → Λ t) + ( \ t → A) + ( \ t → \ x → C x) + ( a) + ( c) #def axiom-choice-case-consequence uses (extext) ( A : U) @@ -521,9 +529,14 @@ Segal, then so is `Σ A, C`. : is-contr ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) - := U --- Hint: Use is-contr-equiv-is-contr - + := + is-contr-equiv-is-contr + ( ( t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) + ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) + , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) + ( axiom-choice-case A C a c) + ( has-unique-inner-extensions-is-segal-case-consequence + A is-segal-A C is-covariant-C a c) -- This one I think you are already working on. -- If you have it in some other file then delete this. From 9a2de67dc54aff6765b719b2c9c5ca12447357e6 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Thu, 20 Jun 2024 19:58:06 +0200 Subject: [PATCH 30/37] dependent composition? --- src/simplicial-hott/08-covariant.rzk.md | 130 +++++++++++++----------- 1 file changed, 73 insertions(+), 57 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index e660ee07..51c587d9 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -538,17 +538,6 @@ Segal, then so is `Σ A, C`. ( has-unique-inner-extensions-is-segal-case-consequence A is-segal-A C is-covariant-C a c) --- This one I think you are already working on. --- If you have it in some other file then delete this. --- #def equiv-sigma-is-contr-base --- ( A : U) --- ( is-contr-A : is-contr A) --- ( C : A → U) --- : Equiv --- ( Σ ( x : A) , C x) --- ( C (center-contraction A is-contr A)) --- := U - #def equiv-ext-is-segal-base ( A : U) ( is-segal-A : is-segal A) @@ -561,8 +550,13 @@ Segal, then so is `Σ A, C`. ( ( t : Δ²) → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) - := U - -- Hint: Use the last exercise. This one is hard! + := + transport-equiv-total-type-second-center-is-contr-base + ( ( t : Δ²) → A [Λ t ↦ a t]) + ( has-unique-inner-extensions-is-segal A is-segal-A a) + ( \ f → ((t : Δ²) → C (f t) [Λ t ↦ c t])) + ( witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) + ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s))) #def is-contr-horn-ext-is-covariant uses (extext) ( A : U) @@ -575,12 +569,15 @@ Segal, then so is `Σ A, C`. ( ( t : Δ²) → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) - := U - -- Hint: Start from is-contr-equiv-is-contr - -- You also need: - -- equiv-ext-is-segal-base - -- quiv-sigma-is-contr-base - -- axiom-choice-case-consequence + := + is-contr-equiv-is-contr + ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) + , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) + ( ( t : Δ²) + → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) + ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) + ( equiv-ext-is-segal-base A is-segal-A C a c) + ( axiom-choice-case-consequence A is-segal-A C is-covariant-C a c) #def dhorn ( A : U) @@ -591,11 +588,14 @@ Segal, then so is `Σ A, C`. ( u : C x) ( v : C y) ( w : C z) - ( k : dhom A x y f C u v) - ( m : dhom A y z g C v w) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) : ( ( t : Λ) → C (horn A x y z f g t)) - := U - -- Hint: Use recOR from one of the first files. + := + \ (t , s) → + recOR + ( s ≡ 0₂ ↦ ff t + , t ≡ 1₂ ↦ gg s) #def compositions-are-dhorn-fillings ( A : U) @@ -608,14 +608,18 @@ Segal, then so is `Σ A, C`. ( u : C x) ( v : C y) ( w : C z) - ( k : dhom A x y f C u v) - ( m : dhom A y z g C v w) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) : Equiv - ( Σ ( n : dhom A x z h C u w) - , ( dhom2 A x y z f g h α C u v w k m n)) - ( ( t : Δ²) → C (α t) - [Λ t ↦ dhorn A x y z f g C u v w k m t]) - := U + ( Σ ( hh : dhom A x z h C u w) + , ( dhom2 A x y z f g h α C u v w ff gg hh)) + ( ( t : Δ²) → C (α t) [Λ t ↦ dhorn A x y z f g C u v w ff gg t]) + := + ( \ (hh , H) t → H t + , ( ( \ k → (\ t → k (t , t) , \ (t , s) → k (t , s)) + , \ (hh , H) → refl) + , ( \ k → (\ t → k (t , t) , \ (t , s) → k (t , s)) + , \ (hh , H) → refl))) #def is-contr-ext-is-covariant uses (extext) ( A : U) @@ -628,23 +632,51 @@ Segal, then so is `Σ A, C`. ( u : C x) ( v : C y) ( w : C z) - ( k : dhom A x y f C u v) - ( m : dhom A y z g C v w) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) : is-contr - ( Σ ( n : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) + ( Σ ( hh : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) , dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) - ( witness-comp-is-segal A is-segal-A x y z f g) C u v w k m n) - := U - -- Hint: Use is-contr-equiv-is-contr' and the previous results. - -- Again you need equiv-sigma-is-contr-base - - --- What is missing: a term that extracts the composition from the contractibility! + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg hh) + := + is-contr-equiv-is-contr' + ( Σ ( hh : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) + , dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg hh) + ( ( t : Δ²) → C ((witness-comp-is-segal A is-segal-A x y z f g) t) + [Λ t ↦ dhorn A x y z f g C u v w ff gg t]) + ( compositions-are-dhorn-fillings A x y z f g + ( comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) + C u v w ff gg) + ( is-contr-horn-ext-is-covariant A is-segal-A C is-covariant-C + ( horn A x y z f g) + ( dhorn A x y z f g C u v w ff gg)) + +#def dcomp uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w + := + \ t → + ( second + ( first + ( is-contr-ext-is-covariant + A is-segal-A C is-covariant-C x y z f g u v w ff gg))) (t , t) ``` ## Dependent composition try - ```rzk #def dhom-to-hom-total-type ( A : U) @@ -894,22 +926,6 @@ Segal, then so is `Σ A, C`. -- The thing above but unfolded, also crashes ``` -```rzk -#def test-comp - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - : ( ( t₁ , t₂) : Δ²) → A - [ t₂ ≡ 0₂ ↦ f t₁ - , t₁ ≡ 1₂ ↦ g t₂ - , t₂ ≡ t₁ ↦ (comp-is-segal A is-segal-A x y z f g) t₂ - ] - := - witness-comp-is-segal A is-segal-A x y z f g -``` - ```rzk -- #def is-comp-proj-comp-total-type uses (extext) -- ( A : U) From 80767a8411da1449518c796d2b59f1b0d1e54df0 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Fri, 21 Jun 2024 10:59:15 +0200 Subject: [PATCH 31/37] dcomp --- src/simplicial-hott/08-covariant.rzk.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 51c587d9..d2ba46c7 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -648,7 +648,7 @@ Segal, then so is `Σ A, C`. ( compositions-are-dhorn-fillings A x y z f g ( comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g) - C u v w ff gg) + C u v w ff gg) ( is-contr-horn-ext-is-covariant A is-segal-A C is-covariant-C ( horn A x y z f g) ( dhorn A x y z f g C u v w ff gg)) @@ -675,6 +675,8 @@ Segal, then so is `Σ A, C`. A is-segal-A C is-covariant-C x y z f g u v w ff gg))) (t , t) ``` +-- Do I want to prove an analogue of is-segal-is-local-horn-inclusion or other? + ## Dependent composition try ```rzk From b1ccbb47d7b972623e9284fe3af236ed77f65a53 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Fri, 21 Jun 2024 17:20:36 +0200 Subject: [PATCH 32/37] dcomp --- src/simplicial-hott/08-covariant.rzk.md | 584 +----------------------- 1 file changed, 20 insertions(+), 564 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index d2ba46c7..9fcd9257 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -467,59 +467,12 @@ Segal, then so is `Σ A, C`. ( is-naive-left-fibration-is-covariant A C is-covariant-C)) ``` - ## Dependent composition -```rzk --- Here is a path way to solve the problem. It includes the problem you are already working on. -#def has-unique-inner-extensions-is-segal-case uses (extext) - ( A : U) - ( is-segal-A : is-segal A) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - : has-unique-extensions (2 × 2) Δ² (\ t → Λ t) (Σ (x : A) , C x) - := - has-unique-inner-extensions-is-segal - ( Σ ( x : A) , C x) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - -#def has-unique-inner-extensions-is-segal-case-consequence uses (extext) - ( A : U) - ( is-segal-A : is-segal A) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( a : (t : Λ) → A) - ( c : (t : Λ) → C (a t)) - : is-contr ((t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) - := - has-unique-inner-extensions-is-segal-case - ( A) - ( is-segal-A) - ( C) - ( is-covariant-C) - ( \ t → (a t , c t)) - -#def axiom-choice-case - ( A : U) - ( C : A → U) - ( a : (t : Λ) → A) - ( c : (t : Λ) → C (a t)) - : Equiv - ( ( t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) - ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) - , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) - := - axiom-choice - ( 2 × 2) - ( Δ²) - ( \ t → Λ t) - ( \ t → A) - ( \ t → \ x → C x) - ( a) - ( c) +We can compose dependent arrows given a covariant type family. -#def axiom-choice-case-consequence uses (extext) +```rzk title="RS17, Remark 8.11" +#def is-contr-ext-is-covariant uses (extext) ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -534,9 +487,19 @@ Segal, then so is `Σ A, C`. ( ( t : Δ²) → (Σ (x : A) , C x) [Λ t ↦ (a t , c t)]) ( Σ ( f : ((t : Δ²) → A [Λ t ↦ a t])) , ( ( t : Δ²) → C (f t) [Λ t ↦ c t])) - ( axiom-choice-case A C a c) - ( has-unique-inner-extensions-is-segal-case-consequence - A is-segal-A C is-covariant-C a c) + ( axiom-choice + ( 2 × 2) + ( Δ²) + ( \ t → Λ t) + ( \ t → A) + ( \ t → \ x → C x) + ( a) + ( c)) + ( has-unique-inner-extensions-is-segal + ( Σ ( x : A) , C x) + ( is-segal-total-type-covariant-family-is-segal-base + A C is-covariant-C is-segal-A) + ( \ t → (a t , c t))) #def equiv-ext-is-segal-base ( A : U) @@ -551,7 +514,7 @@ Segal, then so is `Σ A, C`. → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) := - transport-equiv-total-type-second-center-is-contr-base + transport-equiv-center-fiber-total-type-is-contr-base ( ( t : Δ²) → A [Λ t ↦ a t]) ( has-unique-inner-extensions-is-segal A is-segal-A a) ( \ f → ((t : Δ²) → C (f t) [Λ t ↦ c t])) @@ -577,7 +540,7 @@ Segal, then so is `Σ A, C`. → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) ( equiv-ext-is-segal-base A is-segal-A C a c) - ( axiom-choice-case-consequence A is-segal-A C is-covariant-C a c) + ( is-contr-ext-is-covariant A is-segal-A C is-covariant-C a c) #def dhorn ( A : U) @@ -621,7 +584,7 @@ Segal, then so is `Σ A, C`. , ( \ k → (\ t → k (t , t) , \ (t , s) → k (t , s)) , \ (hh , H) → refl))) -#def is-contr-ext-is-covariant uses (extext) +#def is-contr-ext-dhom-is-covariant uses (extext) ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -671,517 +634,10 @@ Segal, then so is `Σ A, C`. \ t → ( second ( first - ( is-contr-ext-is-covariant + ( is-contr-ext-dhom-is-covariant A is-segal-A C is-covariant-C x y z f g u v w ff gg))) (t , t) ``` --- Do I want to prove an analogue of is-segal-is-local-horn-inclusion or other? - -## Dependent composition try - -```rzk -#def dhom-to-hom-total-type - ( A : U) - ( x y : A) - ( f : hom A x y) - ( C : A → U) - ( u : C x) - ( v : C y) - ( ff : dhom A x y f C u v) - : hom (total-type A C) (x , u) (y , v) - := \ t → (f t , ff t) -``` - -```rzk -#def dhom-to-hom - ( A : U) - ( x y : A) - ( f : hom A x y) - ( C : A → U) - ( u : C x) - ( v : C y) - ( ff : dhom A x y f C u v) - : hom A x y - := f -``` - -```rzk -#def dhom-to-hom-total-type-on-pairs - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : product - ( hom (total-type A C) (x , u) (y , v)) - ( hom (total-type A C) (y , v) (z , w)) - := - ( ( dhom-to-hom-total-type A x y f C u v ff) - , ( dhom-to-hom-total-type A y z g C v w gg)) -``` - -```rzk -#def hom-total-type-to-dhom - ( A : U) - ( is-segal-A : is-segal A) - ( x y : A) - ( f : hom A x y) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - : ( Σ ( k : hom (total-type A C) (x , u) (y , v)) - , ( ( \ t → first (k t)) =_{hom A x y} f)) - → dhom A x y f C u v - := \ (k , p) → - \ t → - ( transport - ( hom A x y) - ( \ g → dhom A x y g C u v) - ( \ t → first (k t)) f p (\ t → second (k t)) t) -``` - -```rzk -#def dhom-to-hom-total-type-over - ( A : U) - ( is-segal-A : is-segal A) - ( x y : A) - ( f : hom A x y) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - : dhom A x y f C u v - → ( Σ ( k : hom (total-type A C) (x , u) (y , v)) - , ( ( \ t → first (k t)) =_{hom A x y} f)) - := - \ ff → - ( dhom-to-hom-total-type A x y f C u v ff - , refl) -``` - -```rzk -#def is-over-dhom-to-hom-total-type - ( A : U) - ( is-segal-A : is-segal A) - ( x y : A) - ( f : hom A x y) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( ff : dhom A x y f C u v) - : ( \ t → first (dhom-to-hom-total-type A x y f C u v ff t)) =_{hom A x y} f - := refl -``` - -```rzk -#def comp-total-type uses (extext) - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : hom (total-type A C) (x , u) (z , w) - := - -- \ t → (witness-comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg) (t , t)) - comp-is-segal - ( total-type A C) - ( is-segal-total-type-covariant-family-is-segal-base - A C is-covariant-C is-segal-A) - ( x , u) (y , v) (z , w) - ( dhom-to-hom-total-type A x y f C u v ff) - ( dhom-to-hom-total-type A y z g C v w gg) -``` - -```rzk -#def proj-comp-total-type uses (extext) - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : hom A x z - := - \ t → first - ( comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg t) -``` - -```rzk --- #def is-comp-proj-comp-total-type uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : --- hom2 (total-type A C) (x , u) (y , v) (z , w) --- ( dhom-to-hom-total-type A x y f C u v ff) --- ( dhom-to-hom-total-type A y z g C v w gg) --- ( comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) --- := --- witness-comp-is-segal --- ( total-type A C) --- ( is-segal-total-type-covariant-family-is-segal-base --- A C is-covariant-C is-segal-A) --- ( x , u) (y , v) (z , w) --- ( dhom-to-hom-total-type A x y f C u v ff) --- ( dhom-to-hom-total-type A y z g C v w gg) -``` - -```rzk --- #set-option "max-whnf-depth" = "20" --- #def is-comp-proj-comp-total-type uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : --- hom2 A x y z f g --- ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) --- := --- \ (t₁ , t₂) → --- ( first (witness-comp-is-segal --- ( total-type A C) --- ( is-segal-total-type-covariant-family-is-segal-base --- A C is-covariant-C is-segal-A) --- ( x , u) (y , v) (z , w) --- ( dhom-to-hom-total-type A x y f C u v ff) --- ( dhom-to-hom-total-type A y z g C v w gg) (t₁ , t₂))) -``` - -```rzk --- #def is-comp-proj-comp-total-type uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : hom2 A x y z f g --- ( \ t → first --- ( comp-is-segal --- ( total-type A C) --- ( is-segal-total-type-covariant-family-is-segal-base --- A C is-covariant-C is-segal-A) --- ( x , u) (y , v) (z , w) --- ( \ r → (f r , ff r)) --- ( \ s → (g s , gg s)) t)) --- := --- \ (t₁ , t₂) → --- ( first (witness-comp-is-segal --- ( total-type A C) --- ( is-segal-total-type-covariant-family-is-segal-base --- A C is-covariant-C is-segal-A) --- ( x , u) (y , v) (z , w) --- ( \ r → (f r , ff r)) --- ( \ s → (g s , gg s)) (t₁ , t₂))) - --- The thing above but unfolded, also crashes -``` - -```rzk --- #def is-comp-proj-comp-total-type uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : Σ ( h : hom A x z) , hom2 A x y z f g h --- := U - -- ( \ t → first (comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg) t) - -- , \ t → first (witness-comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg) t) -``` - -```rzk --- #def eq-comp-total-type uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : ( comp-is-segal A is-segal-A x y z f g) --- =_{hom A x z} --- ( proj-comp-total-type A is-segal-A x y z f g C is-covariant-C u v w ff gg) --- := U --- Strategy: Show in the previous statement that this is indeed a composition --- and then just use uniqueness-comp-is-segal -``` - -```rzk --- #def dhom-dhom-to-dhom2 --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( h : hom A x z) --- ( α : hom2 A x y z f g h) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- ( hh : dhom A x z h C u w) --- : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) --- , ( hom2 (total-type A C) (x , u) (y , v) (z , w) --- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) k)) -``` - -```rzk -#def dhom2-to-dhom - ( A : U) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( h : hom A x z) - ( α : hom2 A x y z f g h) - ( C : A → U) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - ( hh : dhom A x z h C u w) - : dhom2 A x y z f g h α C u v w ff gg hh - → dhom A x z h C u w - := - \ k → - \ t → - k (t , t) -``` - -```rzk -#def dhom2-to-hom2-total-type - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : ( Σ ( h : hom A x z) - , Σ ( α : hom2 A x y z f g h) - , ( Σ ( hh : dhom A x z h C u w) - , dhom2 A x y z f g h α C u v w ff gg hh)) - → ( Σ ( k : hom (total-type A C) (x , u) (z , w)) - , ( hom2 (total-type A C) (x , u) (y , v) (z , w) - ( dhom-to-hom-total-type A x y f C u v ff) - ( dhom-to-hom-total-type A y z g C v w gg) k)) - := - \ (h , (α , (hh , k))) → - ( dhom-to-hom-total-type A x z h C u w hh , \ t → (α t , k t)) -``` - -```rzk -#def hom2-total-type-to-dhom2 - ( A : U) - ( is-segal-A : is-segal A) - ( x y z : A) - ( f : hom A x y) - ( g : hom A y z) - ( C : A → U) - ( is-covariant-C : is-covariant A C) - ( u : C x) - ( v : C y) - ( w : C z) - ( ff : dhom A x y f C u v) - ( gg : dhom A y z g C v w) - : ( Σ ( k : hom (total-type A C) (x , u) (z , w)) - , ( hom2 (total-type A C) (x , u) (y , v) (z , w) - ( dhom-to-hom-total-type A x y f C u v ff) - ( dhom-to-hom-total-type A y z g C v w gg) k)) - → Σ ( h : hom A x z) - , Σ ( α : hom2 A x y z f g h) - , ( Σ ( hh : dhom A x z h C u w) - , dhom2 A x y z f g h α C u v w ff gg hh) - := - \ (k , kk) → - ( \ t → first (k t) - , ( \ t → first (kk t) - , ( \ t → second (kk (t , t)) , \ t → second (kk t)))) -``` - -```rzk title="RS17, Remark 8.11" ---This probably doesn't work, same "being over comp f g" problems as the previous approach. --- #def dcomp uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w --- := --- dhom2-to-dhom A x y z f g (comp-is-segal A is-segal-A x y z f g) --- ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg - -- This crashed when I added the same thing as below, but with a first instead of a second in front - -- ( second (second (second (hom2-total-type-to-dhom2 - -- A is-segal-A x y z f g C is-covariant-C u v w ff gg - -- ( comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg) - -- , witness-comp-is-segal - -- ( total-type A C) - -- ( is-segal-total-type-covariant-family-is-segal-base - -- A C is-covariant-C is-segal-A) - -- ( x , u) (y , v) (z , w) - -- ( dhom-to-hom-total-type A x y f C u v ff) - -- ( dhom-to-hom-total-type A y z g C v w gg)))))) -``` - -```rzk --- #def test uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( h : hom A x z) --- ( α : hom2 A x y z f g h) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : is-contr (Σ (hh : dhom A x z h C u w) --- , dhom2 A x y z f g h α C u v w ff gg hh) --- := - - - --- #def total-hom-to-dhom --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y : A) --- ( C : A → U) --- ( f : hom A x y) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( k : hom (total-type A C) (x , u) (y , v)) --- : dhom A x y f C u v --- := \ t → second (k t) - --[t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y] - --- #def dcomp uses (extext) --- ( A : U) --- ( is-segal-A : is-segal A) --- ( x y z : A) --- ( f : hom A x y) --- ( g : hom A y z) --- ( C : A → U) --- ( is-covariant-C : is-covariant A C) --- ( u : C x) --- ( v : C y) --- ( w : C z) --- ( ff : dhom A x y f C u v) --- ( gg : dhom A y z g C v w) --- : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w --- := --- \ t → second --- ( comp-is-segal --- ( total-type A C) --- ( is-segal-total-type-covariant-family-is-segal-base --- A C is-covariant-C is-segal-A) --- ( x , u) (y , v) (z , w) --- ( \ r → (f r , ff r)) (\ s → (g s , gg s)) t) --- This crashed. -``` - ## Covariant lifts, transport, and uniqueness In a covariant family C over a base type A , a term u : C x may be transported From 4c980e11f6ee48fc8f78cde76b3561338c98fb86 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis <116834840+thchatzidiamantis@users.noreply.github.com> Date: Fri, 21 Jun 2024 17:41:43 +0200 Subject: [PATCH 33/37] Update 08-covariant.rzk.md From a2feb937b7466bf6b9d0b8d91e240ddce1a4e4df Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Fri, 21 Jun 2024 21:59:47 +0200 Subject: [PATCH 34/37] added witness and uniqueness --- src/simplicial-hott/08-covariant.rzk.md | 73 +++++++++++++++++++++++-- 1 file changed, 67 insertions(+), 6 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 9fcd9257..e17a8f11 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -616,7 +616,7 @@ We can compose dependent arrows given a covariant type family. ( horn A x y z f g) ( dhorn A x y z f g C u v w ff gg)) -#def dcomp uses (extext) +#def dcomp-is-covariant-family-is-segal-base uses (extext) ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -631,11 +631,72 @@ We can compose dependent arrows given a covariant type family. ( gg : dhom A y z g C v w) : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w := - \ t → - ( second - ( first - ( is-contr-ext-dhom-is-covariant - A is-segal-A C is-covariant-C x y z f g u v w ff gg))) (t , t) + ( first + ( first + ( is-contr-ext-dhom-is-covariant + A is-segal-A C is-covariant-C x y z f g u v w ff gg))) + +#def witness-dcomp-is-covariant-family-is-segal-base uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + : dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg + ( dcomp-is-covariant-family-is-segal-base + A is-segal-A C is-covariant-C x y z f g u v w ff gg) + := + ( second + ( first + ( is-contr-ext-dhom-is-covariant + A is-segal-A C is-covariant-C x y z f g u v w ff gg))) +``` + +```rzk +#def uniqueness-dcomp-is-covariant-family-is-segal-base uses (extext) + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( x y z : A) + ( f : hom A x y) + ( g : hom A y z) + ( u : C x) + ( v : C y) + ( w : C z) + ( ff : dhom A x y f C u v) + ( gg : dhom A y z g C v w) + ( hh : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) + ( H : dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg hh) + : ( dcomp-is-covariant-family-is-segal-base + A is-segal-A C is-covariant-C x y z f g u v w ff gg) = hh + := + first-path-Σ + ( dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) + ( \ hh → + dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg hh) + ( ( dcomp-is-covariant-family-is-segal-base + A is-segal-A C is-covariant-C x y z f g u v w ff gg) + , ( witness-dcomp-is-covariant-family-is-segal-base + A is-segal-A C is-covariant-C x y z f g u v w ff gg)) + ( hh , H) + ( homotopy-contraction + ( ( Σ ( hh : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) + , dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) + ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg hh)) + ( is-contr-ext-dhom-is-covariant + A is-segal-A C is-covariant-C x y z f g u v w ff gg) + ( hh , H)) ``` ## Covariant lifts, transport, and uniqueness From c45f467517d3ce8ee849759d9f78c81523a907c7 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Fri, 12 Jul 2024 12:54:26 +0200 Subject: [PATCH 35/37] renamings --- src/simplicial-hott/08-covariant.rzk.md | 39 +++++++++++++++---------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index e17a8f11..0ee59843 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -469,10 +469,8 @@ Segal, then so is `Σ A, C`. ## Dependent composition -We can compose dependent arrows given a covariant type family. - -```rzk title="RS17, Remark 8.11" -#def is-contr-ext-is-covariant uses (extext) +```rzk +#def is-contr-horn-ext-is-covariant-family-is-segal-base uses (extext) ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -501,7 +499,7 @@ We can compose dependent arrows given a covariant type family. A C is-covariant-C is-segal-A) ( \ t → (a t , c t))) -#def equiv-ext-is-segal-base +#def equiv-comp-horn-ext-is-segal-base ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -521,7 +519,7 @@ We can compose dependent arrows given a covariant type family. ( witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s))) -#def is-contr-horn-ext-is-covariant uses (extext) +#def is-contr-comp-horn-ext-is-covariant-family-is-segal-base uses (extext) ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -539,8 +537,9 @@ We can compose dependent arrows given a covariant type family. ( ( t : Δ²) → C (witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s)) t) [Λ t ↦ c t]) - ( equiv-ext-is-segal-base A is-segal-A C a c) - ( is-contr-ext-is-covariant A is-segal-A C is-covariant-C a c) + ( equiv-comp-horn-ext-is-segal-base A is-segal-A C a c) + ( is-contr-horn-ext-is-covariant-family-is-segal-base + A is-segal-A C is-covariant-C a c) #def dhorn ( A : U) @@ -560,7 +559,7 @@ We can compose dependent arrows given a covariant type family. ( s ≡ 0₂ ↦ ff t , t ≡ 1₂ ↦ gg s) -#def compositions-are-dhorn-fillings +#def dcompositions-are-dhorn-fillings ( A : U) ( x y z : A) ( f : hom A x y) @@ -583,8 +582,12 @@ We can compose dependent arrows given a covariant type family. , \ (hh , H) → refl) , ( \ k → (\ t → k (t , t) , \ (t , s) → k (t , s)) , \ (hh , H) → refl))) +``` -#def is-contr-ext-dhom-is-covariant uses (extext) +We can compose dependent arrows given a covariant type family. + +```rzk title="RS17, Remark 8.11" +#def is-contr-dhom2-comp-is-covariant-family-is-segal-base uses (extext) ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -608,11 +611,15 @@ We can compose dependent arrows given a covariant type family. ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg hh) ( ( t : Δ²) → C ((witness-comp-is-segal A is-segal-A x y z f g) t) [Λ t ↦ dhorn A x y z f g C u v w ff gg t]) - ( compositions-are-dhorn-fillings A x y z f g + ( dcompositions-are-dhorn-fillings A x y z f g ( comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg) - ( is-contr-horn-ext-is-covariant A is-segal-A C is-covariant-C + ( is-contr-comp-horn-ext-is-covariant-family-is-segal-base + ( A) + ( is-segal-A) + ( C) + ( is-covariant-C) ( horn A x y z f g) ( dhorn A x y z f g C u v w ff gg)) @@ -633,7 +640,7 @@ We can compose dependent arrows given a covariant type family. := ( first ( first - ( is-contr-ext-dhom-is-covariant + ( is-contr-dhom2-comp-is-covariant-family-is-segal-base A is-segal-A C is-covariant-C x y z f g u v w ff gg))) #def witness-dcomp-is-covariant-family-is-segal-base uses (extext) @@ -656,10 +663,12 @@ We can compose dependent arrows given a covariant type family. := ( second ( first - ( is-contr-ext-dhom-is-covariant + ( is-contr-dhom2-comp-is-covariant-family-is-segal-base A is-segal-A C is-covariant-C x y z f g u v w ff gg))) ``` +Dependent composition is unique. + ```rzk #def uniqueness-dcomp-is-covariant-family-is-segal-base uses (extext) ( A : U) @@ -694,7 +703,7 @@ We can compose dependent arrows given a covariant type family. ( ( Σ ( hh : dhom A x z (comp-is-segal A is-segal-A x y z f g) C u w) , dhom2 A x y z f g (comp-is-segal A is-segal-A x y z f g) ( witness-comp-is-segal A is-segal-A x y z f g) C u v w ff gg hh)) - ( is-contr-ext-dhom-is-covariant + ( is-contr-dhom2-comp-is-covariant-family-is-segal-base A is-segal-A C is-covariant-C x y z f g u v w ff gg) ( hh , H)) ``` From 07bcfee5eca1eed0ed362f56e0aabc27cdc7d810 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sun, 14 Jul 2024 18:07:40 +0200 Subject: [PATCH 36/37] improved comments --- src/simplicial-hott/08-covariant.rzk.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 0ee59843..4e8185a6 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -469,6 +469,9 @@ Segal, then so is `Σ A, C`. ## Dependent composition +In a covariant family over a Segal type, we will define dependent composition +of arrows. We first apply the result that the total type is Segal as follows. + ```rzk #def is-contr-horn-ext-is-covariant-family-is-segal-base uses (extext) ( A : U) @@ -584,7 +587,8 @@ Segal, then so is `Σ A, C`. , \ (hh , H) → refl))) ``` -We can compose dependent arrows given a covariant type family. +We now prove contractibility of a type that will be used to define dependent +composition. ```rzk title="RS17, Remark 8.11" #def is-contr-dhom2-comp-is-covariant-family-is-segal-base uses (extext) From 32dd9535c1c18f8ad9ece1f31784ee09f5384a61 Mon Sep 17 00:00:00 2001 From: Theofanis Chatzidiamantis-Christoforidis Date: Mon, 15 Jul 2024 19:52:39 +0200 Subject: [PATCH 37/37] formatting+settings --- .vscode/settings.json | 3 +-- src/simplicial-hott/08-covariant.rzk.md | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 25d32da2..ffa59b7e 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -62,6 +62,5 @@ "editor.detectIndentation": false, "editor.insertSpaces": true }, - "rzk.format.enable": true, - "agdaMode.connection.agdaLanguageServer": true + "rzk.format.enable": true } diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index 4e8185a6..824441ec 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -469,8 +469,8 @@ Segal, then so is `Σ A, C`. ## Dependent composition -In a covariant family over a Segal type, we will define dependent composition -of arrows. We first apply the result that the total type is Segal as follows. +In a covariant family over a Segal type, we will define dependent composition of +arrows. We first apply the result that the total type is Segal as follows. ```rzk #def is-contr-horn-ext-is-covariant-family-is-segal-base uses (extext)