From f5a844a68afac48dbfb218e55ceed86d28a22b7b Mon Sep 17 00:00:00 2001 From: Meven Date: Thu, 15 Apr 2021 09:45:38 +0200 Subject: [PATCH 1/3] another set of solutions --- .../solutionsMevenLennonBertrand.v | 360 ++++++++++++++++++ 1 file changed, 360 insertions(+) create mode 100644 01-introduction-to-hott/solutionsMevenLennonBertrand.v diff --git a/01-introduction-to-hott/solutionsMevenLennonBertrand.v b/01-introduction-to-hott/solutionsMevenLennonBertrand.v new file mode 100644 index 0000000..361ad69 --- /dev/null +++ b/01-introduction-to-hott/solutionsMevenLennonBertrand.v @@ -0,0 +1,360 @@ +(* If loading this file in emacs, remove first the last few lines that force to call `hoqtop` and rather use the `_CoqProject` method described in the installation instructions *) + +From HoTT Require Import HoTT. + +(* This file formalizes the exercises from the lectures "Introduction to HoTT". *) + +Section Part_1_Martin_Lof_Type_Theory. + + Section Exercise_1_1. + + (* Construct an element of + + (Π (x:A) . Σ (y:B) . C x y) → Σ (f : A → B) . Π (x : A) . C x (f x). + *) + + Theorem Exercise_1_1 (A : Type) (B : Type) (C : A -> B -> Type) : + (forall x, { y : B & C x y}) -> { f: A -> B & forall x, C x (f x) }. + Proof. + intros g. + exists (fun x => (g x).1). + intros x. + case (g x) as [y ?]. + assumption. + Defined. + + End Exercise_1_1. + + + Section Exercise_1_2. + + (* Use ind_ℕ to define double : ℕ → ℕ which doubles a number. *) + + Definition double : nat -> nat. + Proof. + apply nat_rect. + - exact 0%nat. + - intros _ s. exact (s.+2)%nat. + (* You should use nat_rect. *) + Defined. + + Eval compute in (double 3). + + End Exercise_1_2. + + Section Exercise_1_3. + + (* Define halve : ℕ → ℕ which halves a number (rounded down). *) + Definition halve : nat -> nat. + Proof. + assert (halve_aux : nat -> nat * Bool). + - apply nat_rect. + + exact (0%nat,true). + + intros _ [h b]. + exact (if b then (h,false) else ((S h),true)). + - intros n. exact (fst (halve_aux n)). + Defined. + + Eval compute in (halve 17). + + End Exercise_1_3. + +End Part_1_Martin_Lof_Type_Theory. + +Section Part_2_Identity_Types. + + Section Exercise_2_1. + + (* Construct a path between paths: p · idpath = p. *) + + Theorem Exercise_2_1 (A : Type) (x y : A) (p : x = y) : p @ idpath y = p. + Proof. + case p. reflexivity. + Defined. + + End Exercise_2_1. + + Section Exercise_2_2. + + (* Given a path p : x = y construct p⁻¹ : y = x and show that idpath⁻¹ = idpath. *) + + Definition inv {A : Type} {x y : A} : x = y -> y = x. + Proof. + intros []. reflexivity. + Defined. + + Definition inv_idpath {A : Type} {x : A} : inv (idpath x) = (idpath x). + Proof. + reflexivity. + Defined. + + End Exercise_2_2. + + Section Exercise_2_3. + + Theorem squirrel {A : Type} {B : A -> Type} : + forall (x y : A) (p : x = y), forall (u : B x) (v : B y) (q : p # u = v), (x ; u) = (y ; v). + Proof. + intros x y p. + induction p. + intros u v q. + induction q. + reflexivity. + Defined. + + Theorem Exercise_2_3 + {A : Type} {B : A -> Type} + {u v : {x : A & B x}} + (p : u.1 = v.1) + (q : p # u.2 = v.2) + : u = v. + Proof. + destruct u, v. + cbn in *. + destruct p. + cbn in *. + destruct q. + reflexivity. + Qed. + + End Exercise_2_3. + +End Part_2_Identity_Types. + +Section Part_3_Homotopy_Levels. + + Section Exercise_3_1. + + (* Construct a point if isContr A → Π (x y : A) . isContr (x = y) *) + + Theorem Exercise_3_1 (A : Type) : + Contr A -> forall (x y : A), Contr (x = y). + Proof. + intros [a c] x y. + exists ((c x)^@(c y)). + intros []. + case (c x). + reflexivity. + Defined. + + + End Exercise_3_1. + + Section Exercise_3_2. + + (* Is contractibility a property or a structure? *) + + (* Please formalize, use "Contr", "IsHProp". *) + + Theorem Exercise_3_2 `{Funext} (A : Type) : IsHProp (Contr A). + Proof. + apply hprop_allpath. + intros [x hx] [y hy]. + induction (hx y). + apply ap. + rapply path_contr. + rapply contr_forall. + apply Exercise_3_1. + eexists. + exact hx. + Defined. + + End Exercise_3_2. + + Section Exercise_3_3. + + (* Π (x : A) . isContr (Σ (y : A) . x = y *) + + (* Please formalize. *) + + Theorem Exercise_3_3 (A : Type) (x : A) : Contr (exists (y : A), x = y). + Proof. + exists (exist _ x (idpath x)). + intros [? []]. + reflexivity. + Defined. + + End Exercise_3_3. + +End Part_3_Homotopy_Levels. + +Section Part_4_Equivalences. + + Section Exercise_4_1. + + (* (a) If P and Q are propostions then (P → Q) × (Q → P) → P ≃ Q *) + + Variables P Q : hProp. + + Definition cow : (P -> Q) * (Q -> P) -> P <~> Q. + Proof. + cbn in *. + intros [f g]. + exists f. + apply isequiv_biinv. + split. + all: exists g ; intro. + - apply P. + - apply Q. + Defined. + + (* (b) The map above is an equivalence. *) + + Definition moo `{Funext} : IsEquiv cow. + Proof. + unshelve eexists. + + intros [f e]. + apply contr_map_isequiv in e. + split. + 1: exact f. + intros q. + specialize (e q). + destruct e as [[]]. + eassumption. + + cbn. + intros f. + apply path_equiv. + reflexivity. + + cbn. + intros [f g]. + apply path_prod ; cbn. + all: reflexivity. + + intros [f g]. + apply path_ishprop. + Defined. + + (* (c) If X and Y are sets then (X ≃ Y) ≃ (X ≅ Y). *) + + (* The library does not seem to have an explicit definition of isIso, + so we include it here. *) + + Definition isIso {A B} (f : A -> B) : Type := + { g : B -> A & (f o g == idmap) * (g o f == idmap) }%type. + + Theorem rabbit `{Funext} (X Y : hSet) : (X <~> Y) <~> { f : X -> Y & isIso f }. + Proof. + srapply equiv_adjointify. + - intros [f [g ]]. + exists f, g. + now split. + - intros (f&?&[]). + exists f. + unshelve econstructor. + 1-3: eassumption. + intros. apply Y. + - cbn. + intros (?&?&[]). + now repeat apply ap. + - cbn. + intros [? []]. + repeat apply ap. + apply path_forall. + intro. + apply hset_path2. + Qed. + + End Exercise_4_1. + + Section Exercise_4_2. + + (* Use equivalence to express the fact that | |₋₁ : A → ∣|A||₋₁ is the + universal map from A to proposition. *) + + (* Please formalize as follows: + + Given a map q : A → Q, define a map e such that IsEquiv e expresses + the fact that q : A → Q is the propositional truncation of A. + *) + + End Exercise_4_2. + +End Part_4_Equivalences. + +Section Part_5_Univalence. + + Section Exercise_5_1. + + (* Show that the type of true propositions is contractible. *) + + Theorem weasel : Univalence -> Contr { A : hProp & A }. + Proof. + exists (Unit_hp ; tt). + intros [A a]. + unshelve eapply path_sigma'. + - apply path_iff_hprop. + + exact (fun _ => a). + + exact (fun _ => tt). + - apply A. + Defined. + + End Exercise_5_1. + + Section Exercise_5_2. + + (* Show that Σ (A : U) . isSet A is not a set. Hint: (2 ≃ 2) ≃ 2. *) + + Lemma two_equiv_two `{Funext} : (Bool <~> Bool) <~> Bool. + Proof. + unshelve eapply equiv_adjointify. + - intros [f _]. + exact (f true). + - exact (fun b : Bool => if b then (equiv_idmap Bool) else equiv_negb). + - intros [] ; reflexivity. + - intros [f [g fg gf ?]]. + apply path_equiv. + apply path_forall. + intros b. + cbn. + remember (f true) as ft eqn:eft. + destruct ft. + + destruct b ; cbn. + 1: symmetry ; assumption. + remember (f false) as ff eqn: eff. + destruct ff. + 2: reflexivity. + rewrite <- (gf false), <- (gf true), eft, eff. + reflexivity. + + destruct b ; cbn. + 1: symmetry ; assumption. + remember (f false) as ff eqn: eff. + destruct ff. + 1: reflexivity. + rewrite <- (gf true), <- (gf false), eft, eff. + reflexivity. + Qed. + + Lemma set_not_set `{ua : Univalence} : IsHSet hSet -> Empty. + Proof. + intros H. + unshelve refine (let B : hSet := _ in _ ). + 1:{ exists Bool. apply hset_bool. } + assert (Contr (B = B)). + 1:{ + unshelve econstructor. + 1: exact idpath. + intros y. + apply hset_path2. + } + assert (Contr (Bool = Bool)). + { + eapply contr_equiv'. + 2: eassumption. + symmetry. + eapply equiv_path_trunctype'. + } + assert (Contr (Bool)) as [b eb]. + 1:{ eapply contr_equiv'. + 2: eassumption. + etransitivity. + 2: apply two_equiv_two. + etransitivity. + 2: exact (equiv_equiv_path Bool Bool). + reflexivity. + } + destruct b ; [specialize (eb false) | specialize (eb true)]. + all: inversion eb. + Qed. + + End Exercise_5_2. + +End Part_5_Univalence. From 1fa6b0bd34ef21e61d55de06fa30c8356ae7f7ae Mon Sep 17 00:00:00 2001 From: Meven Date: Thu, 15 Apr 2021 11:46:13 +0200 Subject: [PATCH 2/3] added a missing exercise --- 01-introduction-to-hott/solutionsMevenLennonBertrand.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/01-introduction-to-hott/solutionsMevenLennonBertrand.v b/01-introduction-to-hott/solutionsMevenLennonBertrand.v index 361ad69..e50644b 100644 --- a/01-introduction-to-hott/solutionsMevenLennonBertrand.v +++ b/01-introduction-to-hott/solutionsMevenLennonBertrand.v @@ -266,6 +266,13 @@ Section Part_4_Equivalences. the fact that q : A → Q is the propositional truncation of A. *) + Definition IsPropTrunc (A Q : Type) (q : A -> Q) := + forall P : hProp, IsEquiv (fun f : Q -> P => f ∘ q). + + Theorem univ_trunc (A : Type) : (IsPropTrunc A (Trunc (-1) A) tr). + Proof. + Admitted. + End Exercise_4_2. End Part_4_Equivalences. From d6258982160484c3aa332d407fee288f6c580602 Mon Sep 17 00:00:00 2001 From: Meven Date: Fri, 16 Apr 2021 13:47:54 +0200 Subject: [PATCH 3/3] universal property of the truncation --- .../solutionsMevenLennonBertrand.v | 37 ++++++++++++++----- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/01-introduction-to-hott/solutionsMevenLennonBertrand.v b/01-introduction-to-hott/solutionsMevenLennonBertrand.v index e50644b..71d7a88 100644 --- a/01-introduction-to-hott/solutionsMevenLennonBertrand.v +++ b/01-introduction-to-hott/solutionsMevenLennonBertrand.v @@ -269,10 +269,25 @@ Section Part_4_Equivalences. Definition IsPropTrunc (A Q : Type) (q : A -> Q) := forall P : hProp, IsEquiv (fun f : Q -> P => f ∘ q). - Theorem univ_trunc (A : Type) : (IsPropTrunc A (Trunc (-1) A) tr). + Theorem univ_trunc `{Funext} (A : Type) : (IsPropTrunc A (Trunc (-1) A) tr). Proof. - Admitted. - + intros Q. + srapply isequiv_adjointify. + - intros f a. + rapply Trunc_rec. + 1: apply Q. + all: eassumption. + - intros f. + apply path_forall. + reflexivity. + - intros f. + apply path_forall. + intros a. + pattern a. + srapply Trunc_ind. + reflexivity. + Qed. + End Exercise_4_2. End Part_4_Equivalences. @@ -285,13 +300,13 @@ Section Part_5_Univalence. Theorem weasel : Univalence -> Contr { A : hProp & A }. Proof. - exists (Unit_hp ; tt). - intros [A a]. - unshelve eapply path_sigma'. - - apply path_iff_hprop. - + exact (fun _ => a). - + exact (fun _ => tt). - - apply A. + exists (Unit_hp ; tt). + intros [A a]. + unshelve eapply path_sigma'. + - apply path_iff_hprop. + + exact (fun _ => a). + + exact (fun _ => tt). + - apply A. Defined. End Exercise_5_1. @@ -300,6 +315,8 @@ Section Part_5_Univalence. (* Show that Σ (A : U) . isSet A is not a set. Hint: (2 ≃ 2) ≃ 2. *) + + Lemma two_equiv_two `{Funext} : (Bool <~> Bool) <~> Bool. Proof. unshelve eapply equiv_adjointify.