From 39ae0a85de146415b2c5cc96989602dacc5f292d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Mart=C3=ADnez=20Carpena?= Date: Fri, 22 Sep 2023 11:12:51 +0200 Subject: [PATCH 1/5] Formalized Prop 10.7 of [RS17] --- src/simplicial-hott/10-rezk-types.rzk.md | 41 ++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index c7f126e6..b12dcea8 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -443,6 +443,47 @@ map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence. is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y) ``` +The following results show how `#!rzk idtoiso` mediates between the +type-theoretic operations on paths and the category-theoretic operations on +arrows. + +```rzk title="RS17, Lemma 10.7" +#def TODO10-7 + ( A : U) + ( is-segal-A : is-segal A) + ( C : A → U) + ( is-covariant-C : is-covariant A C) + ( x y : A) + ( e : x = y) + ( u : C x) + : covariant-transport + ( A) + ( x) + ( y) + ( first (iso-eq A is-segal-A x y e)) + ( C) + ( is-covariant-C) + ( u) + = transport A C x y e u + := + ind-path + ( A) + ( x) + ( \ y' e' → + covariant-transport + ( A) + ( x) + ( y') + ( first (iso-eq A is-segal-A x y' e')) + ( C) + ( is-covariant-C) + ( u) + = transport A C x y' e' u) + ( id-arr-covariant-transport A x C is-covariant-C u) + ( y) + ( e) +``` + ## Uniqueness of initial and final objects In a Segal type, initial objects are isomorphic. From 403e2248614e275b93870f88e510edce2cb93505 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Mart=C3=ADnez=20Carpena?= Date: Fri, 22 Sep 2023 11:13:30 +0200 Subject: [PATCH 2/5] Fix formatting inconsistency --- src/simplicial-hott/10-rezk-types.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index b12dcea8..fe90cb0e 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -435,7 +435,7 @@ map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence. ```rzk title="RS17, Definition 10.6" #def is-rezk - (A : U) + ( A : U) : U := Σ ( is-segal-A : is-segal A) , From d8ee5cd41d92762ba2d96a8a2fc9f63c75931cd2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Mart=C3=ADnez=20Carpena?= Date: Fri, 22 Sep 2023 11:20:24 +0200 Subject: [PATCH 3/5] Proposal name for Lemma 10.7 of [RS17] --- src/simplicial-hott/10-rezk-types.rzk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index fe90cb0e..4d302865 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -448,7 +448,7 @@ type-theoretic operations on paths and the category-theoretic operations on arrows. ```rzk title="RS17, Lemma 10.7" -#def TODO10-7 +#def covariant-transport-of-idtoiso-is-transport ( A : U) ( is-segal-A : is-segal A) ( C : A → U) From b72104ad9357f987e3ee7084621ac31fd82771f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Mart=C3=ADnez=20Carpena?= Date: Fri, 22 Sep 2023 14:32:19 +0200 Subject: [PATCH 4/5] Formalised Lemma 10.8 of [RS17] --- src/simplicial-hott/10-rezk-types.rzk.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 4d302865..43810886 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -484,6 +484,28 @@ arrows. ( e) ``` +```rzk title="RS17, Lemma 10.8" +#def ap-hom-of-idtoiso-is-idtoiso-of-ap + ( A B : U) + ( is-segal-A : is-segal A) + ( is-segal-B : is-segal B) + ( f : A → B) + ( x y : A) + ( e : x = y) + : ( ap-hom A B f x y (first (iso-eq A is-segal-A x y e))) = + ( first ( iso-eq B is-segal-B (f x) (f y) (ap A B x y f e))) + := + ind-path + ( A) + ( x) + ( \ y' e' → + ( ap-hom A B f x y' (first (iso-eq A is-segal-A x y' e'))) = + ( first (iso-eq B is-segal-B (f x) (f y') (ap A B x y' f e')))) + ( refl) + ( y) + ( e) +``` + ## Uniqueness of initial and final objects In a Segal type, initial objects are isomorphic. From 4156cbac14645eed9aa00e85344335793992eebb Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sat, 23 Sep 2023 21:12:37 +0200 Subject: [PATCH 5/5] renaming to compute --- src/simplicial-hott/10-rezk-types.rzk.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 43810886..ac35c6dd 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -443,12 +443,12 @@ map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence. is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y) ``` -The following results show how `#!rzk idtoiso` mediates between the +The following results show how `#!rzk iso-eq` mediates between the type-theoretic operations on paths and the category-theoretic operations on arrows. ```rzk title="RS17, Lemma 10.7" -#def covariant-transport-of-idtoiso-is-transport +#def compute-covariant-transport-of-hom-family-iso-eq-is-segal ( A : U) ( is-segal-A : is-segal A) ( C : A → U) @@ -485,7 +485,7 @@ arrows. ``` ```rzk title="RS17, Lemma 10.8" -#def ap-hom-of-idtoiso-is-idtoiso-of-ap +#def compute-ap-hom-of-iso-eq ( A B : U) ( is-segal-A : is-segal A) ( is-segal-B : is-segal B)