From dfa4035266e8f389caa087914865d5b8ce4d3b3a Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sun, 22 Oct 2023 18:13:19 -0400 Subject: [PATCH 1/3] proof that embeddings have propositional fibers; remains to prove the converse --- src/hott/09-propositions.rzk.md | 88 ++++++++++++++++++++++++++++++++- 1 file changed, 86 insertions(+), 2 deletions(-) diff --git a/src/hott/09-propositions.rzk.md b/src/hott/09-propositions.rzk.md index 781602ec..be4d8709 100644 --- a/src/hott/09-propositions.rzk.md +++ b/src/hott/09-propositions.rzk.md @@ -283,8 +283,8 @@ If each `C a` is a proposition, then so is the total type `total-type A C`. ( c')))) ``` -Conversely, if the total type `total-type A C` is a proposition, then so is -every fiber `C a`. +Conversely, if the total type `#!rzk total-type A C` is a proposition, then so +is every fiber `#!rzk C a`. ```rzk #def is-fiberwise-prop-is-prop-total-type-is-prop-base uses (is-prop-A) @@ -306,3 +306,87 @@ every fiber `C a`. #end families-over-propositions ``` + +## Propositions and embeddings + +A map `#!rzk f : A → B` is an embedding if and only if its fibers are +propositions. + +```rzk +#def is-contr-image-based-paths-is-emb + ( A B : U) + ( f : A → B) + ( is-emb-f : is-emb A B f) + ( x : A) + : is-contr (Σ (y : A) , f x = f y) + := + is-contr-total-are-equiv-from-paths A x + ( \ y → f x = f y) + ( \ y → ap A B x y f) + ( \ y → is-emb-f x y) + +#def is-contr-image-endpoint-based-paths-is-emb + ( A B : U) + ( f : A → B) + ( is-emb-f : is-emb A B f) + ( y : A) + : is-contr (Σ (x : A) , f x = f y) + := + is-contr-equiv-is-contr' + ( Σ (x : A) , f x = f y) + ( Σ (x : A) , f y = f x) + ( total-equiv-family-of-equiv A (\ x → f x = f y) (\ x → f y = f x) + ( \ x → equiv-rev B (f x) (f y))) + ( is-contr-image-based-paths-is-emb A B f is-emb-f y) + +#def is-contr-fib-over-image-is-emb + ( A B : U) + ( f : A → B) + ( is-emb-f : is-emb A B f) + ( y : A) + : is-contr (fib A B f (f y)) + := is-contr-image-endpoint-based-paths-is-emb A B f is-emb-f y + +#def is-contr-is-inhabited-fib-is-emb + ( A B : U) + ( f : A → B) + ( is-emb-f : is-emb A B f) + : ( b : B) → is-contr-is-inhabited (fib A B f b) + := + ind-fib A B f + ( \ b p → is-contr (fib A B f b)) + ( \ a → is-contr-fib-over-image-is-emb A B f is-emb-f a) + +#def is-prop-fib-is-emb + ( A B : U) + ( f : A → B) + ( is-emb-f : is-emb A B f) + ( b : B) + : is-prop (fib A B f b) + := + is-prop-is-contr-is-inhabited (fib A B f b) + ( is-contr-is-inhabited-fib-is-emb A B f is-emb-f b) + +``` + +## Subtypes + +A family of propositions `#!rzk P : A → U` over a type `#!rzk A` may be thought +of as a predicate. + +```rzk +#def is-predicate + ( A : U) + ( P : A → U) + : U + := (a : A) → is-prop (P a) +``` + +When `#!rzk P` is a predicate on `#!rzk A` then `#!rzk total-type A P` is +referred to a subtype of `#!rzk A`. + +#def is-emb-subtype-projection ( A : U) ( P : A → U) ( is-predicate-P : +is-predicate A P) : is-emb (total-type A P) A (projection-total-type A P) := \ a +→ equiv-with-contractible-domain-implies-contractible-codomain ( P a) ( fib +(total-type A P) A (projection-total-type A P) a) ( +equiv-homotopy-fiber-strict-fiber A P a) ( is-predicate-P a) From 7298844337b795ef05f9aeb1a9576e973dd16308 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Sun, 22 Oct 2023 20:47:04 -0400 Subject: [PATCH 2/3] bug reporting --- src/hott/09-propositions.rzk.md | 102 ++++++++++++++++++++++++++++++-- 1 file changed, 97 insertions(+), 5 deletions(-) diff --git a/src/hott/09-propositions.rzk.md b/src/hott/09-propositions.rzk.md index be4d8709..1686c719 100644 --- a/src/hott/09-propositions.rzk.md +++ b/src/hott/09-propositions.rzk.md @@ -367,6 +367,44 @@ propositions. is-prop-is-contr-is-inhabited (fib A B f b) ( is-contr-is-inhabited-fib-is-emb A B f is-emb-f b) +#def is-contr-image-based-paths-is-contr-is-inhabited-fib + ( A B : U) + ( f : A → B) + ( is-contr-is-inhabited-fib-f : (b : B) → is-contr-is-inhabited (fib A B f b)) + ( x : A) + : is-contr (Σ (y : A) , f x = f y) + := + is-contr-equiv-is-contr' + ( Σ (y : A) , f x = f y) + ( Σ (y : A) , f y = f x) + ( total-equiv-family-of-equiv A (\ y → f x = f y) (\ y → f y = f x) + ( \ y → equiv-rev B (f x) (f y))) + ( is-contr-is-inhabited-fib-f (f x) ((x, refl))) + +#def is-emb-is-contr-is-inhabited-fib + ( A B : U) + ( f : A → B) + ( is-contr-is-inhabited-fib-f : (b : B) → is-contr-is-inhabited (fib A B f b)) + : is-emb A B f + := + \ x y → + are-equiv-from-paths-is-contr-total A x (\ z → f x = f z)(\ z → ap A B x z f) + ( is-contr-image-based-paths-is-contr-is-inhabited-fib A B f is-contr-is-inhabited-fib-f x) y + +#def is-emb-is-prop-fib + ( A B : U) + ( f : A → B) + ( is-prop-fib-f : (b : B) → is-prop (fib A B f b)) + : is-emb A B f + := + is-emb-is-contr-is-inhabited-fib A B f + ( \ b → is-contr-is-inhabited-is-prop (fib A B f b) (is-prop-fib-f b)) + +#def is-emb-iff-is-prop-fib + ( A B : U) + ( f : A → B) + : iff (is-emb A B f) ((b : B) → is-prop (fib A B f b)) + := (is-prop-fib-is-emb A B f, is-emb-is-prop-fib A B f) ``` ## Subtypes @@ -385,8 +423,62 @@ of as a predicate. When `#!rzk P` is a predicate on `#!rzk A` then `#!rzk total-type A P` is referred to a subtype of `#!rzk A`. -#def is-emb-subtype-projection ( A : U) ( P : A → U) ( is-predicate-P : -is-predicate A P) : is-emb (total-type A P) A (projection-total-type A P) := \ a -→ equiv-with-contractible-domain-implies-contractible-codomain ( P a) ( fib -(total-type A P) A (projection-total-type A P) a) ( -equiv-homotopy-fiber-strict-fiber A P a) ( is-predicate-P a) +```rzk +#def is-emb-subtype-projection + ( A : U) + ( P : A → U) + ( is-predicate-P : is-predicate A P) + : is-emb (total-type A P) A (projection-total-type A P) + := + is-emb-is-prop-fib (total-type A P) A (projection-total-type A P) + ( \ a → + is-prop-Equiv-is-prop' + ( P a) ( fib (total-type A P) A (projection-total-type A P) a) + ( equiv-homotopy-fiber-strict-fiber A P a) (is-predicate-P a)) +``` + +The subtype projection embedding reflects identifications. + +```rzk +#def subtype-eq-reflection + ( A : U) + ( P : A → U) + ( is-predicate-P : is-predicate A P) + ( (a, p) (b, q) : total-type A P) + : (a = b) → (a, p) =_{total-type A P} (b, q) + := + inv-ap-is-emb (total-type A P) A (projection-total-type A P) + ( is-emb-subtype-projection A P is-predicate-P) ((a, p)) ((b, q)) + +#def subtype-eq-reflection-okay + ( A : U) + ( P : A → U) + ( is-predicate-P : is-predicate A P) + ( ap bq : total-type A P) + : ((projection-total-type A P ap) = (projection-total-type A P bq)) + → ap =_{total-type A P} bq + := + inv-ap-is-emb (total-type A P) A (projection-total-type A P) + ( is-emb-subtype-projection A P is-predicate-P) ap bq + +#def subtype-eq-reflection-fails + ( A : U) + ( P : A → U) + ( is-predicate-P : is-predicate A P) + : ( (a, p) (b, q) : total-type A P) + → (a = b) → (a, p) =_{total-type A P} (b, q) + := + inv-ap-is-emb (total-type A P) A (projection-total-type A P) + ( is-emb-subtype-projection A P is-predicate-P) + +#def subtype-eq-reflection-fails-also + ( A : U) + ( P : A → U) + ( is-predicate-P : is-predicate A P) + : ( ap bq : total-type A P) + → ((projection-total-type A P ap) = (projection-total-type A P bq)) + → ap =_{total-type A P} bq + := + inv-ap-is-emb (total-type A P) A (projection-total-type A P) + ( is-emb-subtype-projection A P is-predicate-P) +``` From 8ae2652f24ec02e3ef5d9fa8a3365aee5cdf5918 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Mon, 23 Oct 2023 09:48:18 -0400 Subject: [PATCH 3/3] removed broken functions --- src/hott/09-propositions.rzk.md | 35 ++------------------------------- 1 file changed, 2 insertions(+), 33 deletions(-) diff --git a/src/hott/09-propositions.rzk.md b/src/hott/09-propositions.rzk.md index 1686c719..c041a755 100644 --- a/src/hott/09-propositions.rzk.md +++ b/src/hott/09-propositions.rzk.md @@ -444,41 +444,10 @@ The subtype projection embedding reflects identifications. ( A : U) ( P : A → U) ( is-predicate-P : is-predicate A P) - ( (a, p) (b, q) : total-type A P) - : (a = b) → (a, p) =_{total-type A P} (b, q) - := - inv-ap-is-emb (total-type A P) A (projection-total-type A P) - ( is-emb-subtype-projection A P is-predicate-P) ((a, p)) ((b, q)) - -#def subtype-eq-reflection-okay - ( A : U) - ( P : A → U) - ( is-predicate-P : is-predicate A P) - ( ap bq : total-type A P) - : ((projection-total-type A P ap) = (projection-total-type A P bq)) - → ap =_{total-type A P} bq - := - inv-ap-is-emb (total-type A P) A (projection-total-type A P) - ( is-emb-subtype-projection A P is-predicate-P) ap bq - -#def subtype-eq-reflection-fails - ( A : U) - ( P : A → U) - ( is-predicate-P : is-predicate A P) - : ( (a, p) (b, q) : total-type A P) + : ( (a, p) : total-type A P) + → ( (b, q) : total-type A P) → (a = b) → (a, p) =_{total-type A P} (b, q) := inv-ap-is-emb (total-type A P) A (projection-total-type A P) ( is-emb-subtype-projection A P is-predicate-P) - -#def subtype-eq-reflection-fails-also - ( A : U) - ( P : A → U) - ( is-predicate-P : is-predicate A P) - : ( ap bq : total-type A P) - → ((projection-total-type A P ap) = (projection-total-type A P bq)) - → ap =_{total-type A P} bq - := - inv-ap-is-emb (total-type A P) A (projection-total-type A P) - ( is-emb-subtype-projection A P is-predicate-P) ```