From da9b3099387a692ba7bd1c44620b869e01b5be2a Mon Sep 17 00:00:00 2001 From: Hyunggyu Jang Date: Fri, 4 Nov 2022 10:30:57 +0900 Subject: [PATCH 1/4] Solve exercise 3.15 and 3.17 --- contrib/HoTTBookExercises.v | 34 ++++++++++++++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v index b9be4685730..d9a6d2745e9 100644 --- a/contrib/HoTTBookExercises.v +++ b/contrib/HoTTBookExercises.v @@ -939,7 +939,23 @@ End Book_3_14. (* ================================================== ex:impred-brck *) (** Exercise 3.15 *) - +Section Book_3_15. + Definition Book_3_15_rec {A B} `{IsHProp B} + : (A -> B) -> (forall P : HProp, (A -> P) -> P) -> B. + Proof. + intros f trA. + set (B' := Build_HProp B). + specialize (trA B'). + apply trA. + assumption. + Defined. + Lemma Book_3_15_eq {A B} `{IsHProp B} (f : A -> B) + : forall a, f a = Book_3_15_rec f (fun _ f' => f' a). + Proof. + intro a. reflexivity. + Qed. + (* proportional resizing is needed? *) +End Book_3_15. (* ================================================== ex:lem-impl-dn-commutes *) (** Exercise 3.16 *) @@ -949,7 +965,21 @@ End Book_3_14. (* ================================================== ex:prop-trunc-ind *) (** Exercise 3.17 *) - +Section Book_3_17. + Theorem prop_trunc_ind + : forall A (B : merely A -> Type), + (forall a, B (tr a)) + -> (forall x, IsHProp (B x)) + -> forall x, B x. + Proof. + intros A B base p x. + specialize (p x). + refine (Trunc_rec _ x). + intro a. + assert (H: tr a = x) by (apply path_ishprop). + destruct H. exact (base a). + Defined. +End Book_3_17. (* ================================================== ex:lem-ldn *) (** Exercise 3.18 *) From 09102873e3e89f34087adaa752958132b97307b3 Mon Sep 17 00:00:00 2001 From: Hyunggyu Jang Date: Wed, 30 Nov 2022 09:12:59 +0000 Subject: [PATCH 2/4] Reflect reviews --- contrib/HoTTBookExercises.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v index d9a6d2745e9..2ec5fce432c 100644 --- a/contrib/HoTTBookExercises.v +++ b/contrib/HoTTBookExercises.v @@ -940,6 +940,7 @@ End Book_3_14. (** Exercise 3.15 *) Section Book_3_15. + (* Propositional resizing is (implicitly) used for [forall P : HProp, (A -> P) -> P] to be on the same universe as [A] *) Definition Book_3_15_rec {A B} `{IsHProp B} : (A -> B) -> (forall P : HProp, (A -> P) -> P) -> B. Proof. @@ -954,7 +955,6 @@ Section Book_3_15. Proof. intro a. reflexivity. Qed. - (* proportional resizing is needed? *) End Book_3_15. (* ================================================== ex:lem-impl-dn-commutes *) @@ -968,12 +968,11 @@ End Book_3_15. Section Book_3_17. Theorem prop_trunc_ind : forall A (B : merely A -> Type), - (forall a, B (tr a)) - -> (forall x, IsHProp (B x)) + (forall x, IsHProp (B x)) + -> (forall a, B (tr a)) -> forall x, B x. Proof. - intros A B base p x. - specialize (p x). + intros A B p base x. refine (Trunc_rec _ x). intro a. assert (H: tr a = x) by (apply path_ishprop). From fea4f106c1faa400795558f9de710243edf102bf Mon Sep 17 00:00:00 2001 From: Hyunggyu Jang Date: Thu, 1 Dec 2022 02:12:52 +0400 Subject: [PATCH 3/4] Reflect review --- contrib/HoTTBookExercises.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v index 2ec5fce432c..036a16ee6fe 100644 --- a/contrib/HoTTBookExercises.v +++ b/contrib/HoTTBookExercises.v @@ -940,7 +940,7 @@ End Book_3_14. (** Exercise 3.15 *) Section Book_3_15. - (* Propositional resizing is (implicitly) used for [forall P : HProp, (A -> P) -> P] to be on the same universe as [A] *) + (* Propositional resizing is (implicitly) used for [forall P : HProp, (A -> P) -> P] to be in the same universe as [A]. *) Definition Book_3_15_rec {A B} `{IsHProp B} : (A -> B) -> (forall P : HProp, (A -> P) -> P) -> B. Proof. @@ -950,6 +950,7 @@ Section Book_3_15. apply trA. assumption. Defined. + Lemma Book_3_15_eq {A B} `{IsHProp B} (f : A -> B) : forall a, f a = Book_3_15_rec f (fun _ f' => f' a). Proof. @@ -966,17 +967,14 @@ End Book_3_15. (** Exercise 3.17 *) Section Book_3_17. - Theorem prop_trunc_ind - : forall A (B : merely A -> Type), - (forall x, IsHProp (B x)) - -> (forall a, B (tr a)) - -> forall x, B x. + Theorem prop_trunc_ind (A: Type) (B : merely A -> Type) `{forall x, IsHProp (B x)} + : (forall a, B (tr a)) -> forall x, B x. Proof. - intros A B p base x. + intros base x. refine (Trunc_rec _ x). intro a. - assert (H: tr a = x) by (apply path_ishprop). - destruct H. exact (base a). + assert (H': tr a = x) by (apply path_ishprop). + destruct H'. exact (base a). Defined. End Book_3_17. From 2b657ab9678f27728304ac340b9f1fa6ba4f0ec7 Mon Sep 17 00:00:00 2001 From: Hyunggyu Jang Date: Fri, 2 Dec 2022 11:03:59 +0900 Subject: [PATCH 4/4] Make propositional resizing assumption explicit --- contrib/HoTTBookExercises.v | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v index 036a16ee6fe..67d504a2c0c 100644 --- a/contrib/HoTTBookExercises.v +++ b/contrib/HoTTBookExercises.v @@ -940,21 +940,33 @@ End Book_3_14. (** Exercise 3.15 *) Section Book_3_15. - (* Propositional resizing is (implicitly) used for [forall P : HProp, (A -> P) -> P] to be in the same universe as [A]. *) - Definition Book_3_15_rec {A B} `{IsHProp B} - : (A -> B) -> (forall P : HProp, (A -> P) -> P) -> B. + Definition Book_3_15_trunc@{u +} `{PropResizing} `{Funext} (A : Type@{u}) + : Type@{u}. + Proof. + exact (resize_hprop@{_ u} (forall P : HProp@{u}, (A -> P) -> P)). + Defined. + + Definition Book_3_15_ishprop `{PropResizing} `{Funext} (A : Type) + : IsHProp (Book_3_15_trunc A) + := _. + + Definition Book_3_15_rec `{PropResizing} `{Funext} {A B} `{IsHProp B} + : (A -> B) -> (Book_3_15_trunc A) -> B. Proof. intros f trA. set (B' := Build_HProp B). + apply equiv_resize_hprop in trA. specialize (trA B'). apply trA. assumption. Defined. - Lemma Book_3_15_eq {A B} `{IsHProp B} (f : A -> B) - : forall a, f a = Book_3_15_rec f (fun _ f' => f' a). + Lemma Book_3_15_eq `{PropResizing} `{Funext} {A B} `{IsHProp B} (f : A -> B) + : forall a, f a = Book_3_15_rec f (equiv_resize_hprop _ (fun _ f' => f' a)). Proof. - intro a. reflexivity. + intro a. + (* Now judgemental computation rule does not hold in Coq, as in Coq, propositional resizing isn't definitional; judgemental equality doesn't hold. *) + apply path_ishprop. Qed. End Book_3_15.