From fb364f8bc770b89b1d2670eba99110f190a111e3 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 11 Sep 2015 18:53:08 -0400 Subject: [PATCH] feat(types): add more equivalences between combinations of type constructors --- hott/types/arrow.hlean | 34 +++++++++++++++++++++- hott/types/eq.hlean | 2 ++ hott/types/pi.hlean | 55 ++++++++++++++++++++++++++++++++--- hott/types/prod.hlean | 2 +- hott/types/sigma.hlean | 66 +++++++++++++++++++++++++++++++++++++----- hott/types/sum.hlean | 2 ++ 6 files changed, 147 insertions(+), 14 deletions(-) diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean index 33034235a..5e0fa9050 100644 --- a/hott/types/arrow.hlean +++ b/hott/types/arrow.hlean @@ -9,7 +9,7 @@ Theorems about arrow types (function spaces) import types.pi -open eq equiv is_equiv funext pi equiv.ops +open eq equiv is_equiv funext pi equiv.ops is_trunc unit namespace pi @@ -51,6 +51,30 @@ namespace pi definition arrow_equiv_arrow_right' [constructor] (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') := pi_equiv_pi_id f1 + /- Equivalence if one of the types is contractible -/ + + variables (A B) + definition arrow_equiv_of_is_contr_left [constructor] [H : is_contr A] : (A → B) ≃ B := + !pi_equiv_of_is_contr_left + + definition arrow_equiv_of_is_contr_right [constructor] [H : is_contr B] : (A → B) ≃ unit := + !pi_equiv_of_is_contr_right + + /- Interaction with other type constructors -/ + + -- most of these are in the file of the other type constructor + + definition arrow_empty_left [constructor] : (empty → B) ≃ unit := + !pi_empty_left + + definition arrow_unit_left [constructor] : (unit → B) ≃ B := + !arrow_equiv_of_is_contr_left + + definition arrow_unit_right [constructor] : (A → unit) ≃ unit := + !arrow_equiv_of_is_contr_right + + variables {A B} + /- Transport -/ definition arrow_transport {B C : A → Type} (p : a = a') (f : B a → C a) @@ -87,4 +111,12 @@ namespace pi {p : a = a'} (r : Π(b : B), f b =[p] g b) : f =[p] g := pi_pathover_constant r + /- + The fact that the arrow type preserves truncation level is a direct consequence + of the fact that pi's preserve truncation level + -/ + + definition is_trunc_arrow (B : Type) (n : trunc_index) [H : is_trunc n B] : is_trunc n (A → B) := + _ + end pi diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 578193fc5..69345ce71 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -433,6 +433,8 @@ namespace eq -- a lot of this library still needs to be ported from Coq HoTT + -- the behavior of equality in other types is described in the corresponding type files + -- encode decode method open is_trunc diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 2e1b82a31..67f66bd18 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -9,7 +9,7 @@ Theorems about pi-types (dependent function spaces) import types.sigma arity -open eq equiv is_equiv funext sigma +open eq equiv is_equiv funext sigma unit bool is_trunc prod namespace pi variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type} @@ -199,9 +199,56 @@ namespace pi : (Πa, P a) ≃ (Πa, Q a) := pi_equiv_pi equiv.refl g + /- Equivalence if one of the types is contractible -/ + + definition pi_equiv_of_is_contr_left [constructor] (B : A → Type) [H : is_contr A] + : (Πa, B a) ≃ B (center A) := + begin + fapply equiv.MK, + { intro f, exact f (center A)}, + { intro b a, exact (center_eq a) ▸ b}, + { intro b, rewrite [hprop_eq_of_is_contr (center_eq (center A)) idp]}, + { intro f, apply eq_of_homotopy, intro a, induction (center_eq a), + rewrite [hprop_eq_of_is_contr (center_eq (center A)) idp]} + end + + definition pi_equiv_of_is_contr_right [constructor] [H : Πa, is_contr (B a)] + : (Πa, B a) ≃ unit := + begin + fapply equiv.MK, + { intro f, exact star}, + { intro u a, exact !center}, + { intro u, induction u, reflexivity}, + { intro f, apply eq_of_homotopy, intro a, apply is_hprop.elim} + end + + /- Interaction with other type constructors -/ + + -- most of these are in the file of the other type constructor + + definition pi_empty_left [constructor] (B : empty → Type) : (Πx, B x) ≃ unit := + begin + fapply equiv.MK, + { intro f, exact star}, + { intro x y, contradiction}, + { intro x, induction x, reflexivity}, + { intro f, apply eq_of_homotopy, intro y, contradiction}, + end + + definition pi_unit_left [constructor] (B : unit → Type) : (Πx, B x) ≃ B star := + !pi_equiv_of_is_contr_left + + definition pi_bool_left [constructor] (B : bool → Type) : (Πx, B x) ≃ B ff × B tt := + begin + fapply equiv.MK, + { intro f, exact (f ff, f tt)}, + { intro x b, induction x, induction b: assumption}, + { intro x, induction x, reflexivity}, + { intro f, apply eq_of_homotopy, intro b, induction b: reflexivity}, + end + /- Truncatedness: any dependent product of n-types is an n-type -/ - open is_trunc definition is_trunc_pi (B : A → Type) (n : trunc_index) [H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) := begin @@ -222,7 +269,7 @@ namespace pi is_trunc_eq n (f a) (g a)} end local attribute is_trunc_pi [instance] - definition is_trunc_eq_pi [instance] [priority 500] (n : trunc_index) (f g : Πa, B a) + definition is_trunc_pi_eq [instance] [priority 500] (n : trunc_index) (f g : Πa, B a) [H : ∀a, is_trunc n (f a = g a)] : is_trunc n (f = g) := begin apply is_trunc_equiv_closed_rev, @@ -254,4 +301,4 @@ namespace pi end pi -attribute pi.is_trunc_pi [instance] [priority 1510] +attribute pi.is_trunc_pi [instance] [priority 1520] diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index d9dc2dd70..a131e5d7f 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -214,4 +214,4 @@ namespace prod end prod -attribute prod.is_trunc_prod [instance] [priority 1505] +attribute prod.is_trunc_prod [instance] [priority 1510] diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 3ec7e10f1..041566573 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -9,7 +9,7 @@ Theorems about sigma-types (dependent sums) import types.prod -open eq sigma sigma.ops equiv is_equiv function is_trunc +open eq sigma sigma.ops equiv is_equiv function is_trunc sum unit namespace sigma variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type} @@ -243,25 +243,26 @@ namespace sigma /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/ - definition is_equiv_pr1 [instance] (B : A → Type) [H : Π a, is_contr (B a)] + definition is_equiv_pr1 [instance] [constructor] (B : A → Type) [H : Π a, is_contr (B a)] : is_equiv (@pr1 A B) := adjointify pr1 (λa, ⟨a, !center⟩) (λa, idp) (λu, sigma_eq idp (pathover_idp_of_eq !center_eq)) - definition sigma_equiv_of_is_contr_pr2 [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A := + definition sigma_equiv_of_is_contr_right [constructor] [H : Π a, is_contr (B a)] + : (Σa, B a) ≃ A := equiv.mk pr1 _ /- definition 3.11.9(ii): Dually, summing up over a contractible type does nothing. -/ - definition sigma_equiv_of_is_contr_pr1 (B : A → Type) [H : is_contr A] : (Σa, B a) ≃ B (center A) - := - equiv.mk _ (adjointify + definition sigma_equiv_of_is_contr_left [constructor] (B : A → Type) [H : is_contr A] + : (Σa, B a) ≃ B (center A) := + equiv.MK (λu, (center_eq u.1)⁻¹ ▸ u.2) (λb, ⟨!center, b⟩) (λb, ap (λx, x ▸ b) !hprop_eq_of_is_contr) - (λu, sigma_eq !center_eq !tr_pathover)) + (λu, sigma_eq !center_eq !tr_pathover) /- Associativity -/ @@ -306,6 +307,55 @@ namespace sigma ... ≃ B × A : prod_comm_equiv ... ≃ Σ(b : B), A : equiv_prod + /- Interaction with other type constructors -/ + + definition sigma_empty_left [constructor] (B : empty → Type) : (Σx, B x) ≃ empty := + begin + fapply equiv.MK, + { intro v, induction v, contradiction}, + { intro x, contradiction}, + { intro x, contradiction}, + { intro v, induction v, contradiction}, + end + + definition sigma_empty_right [constructor] (A : Type) : (Σ(a : A), empty) ≃ empty := + begin + fapply equiv.MK, + { intro v, induction v, contradiction}, + { intro x, contradiction}, + { intro x, contradiction}, + { intro v, induction v, contradiction}, + end + + definition sigma_unit_left [constructor] (B : unit → Type) : (Σx, B x) ≃ B star := + !sigma_equiv_of_is_contr_left + + definition sigma_unit_right [constructor] (A : Type) : (Σ(a : A), unit) ≃ A := + !sigma_equiv_of_is_contr_right + + definition sigma_sum_left [constructor] (B : A + A' → Type) + : (Σp, B p) ≃ (Σa, B (inl a)) + (Σa, B (inr a)) := + begin + fapply equiv.MK, + { intro v, + induction v with p b, induction p: append (apply inl) (apply inr); constructor; assumption }, + { intro p, induction p with v v: induction v; constructor; assumption}, + { intro p, induction p with v v: induction v; reflexivity}, + { intro v, induction v with p b, induction p: reflexivity}, + end + + definition sigma_sum_right [constructor] (B C : A → Type) + : (Σa, B a + C a) ≃ (Σa, B a) + (Σa, C a) := + begin + fapply equiv.MK, + { intro v, + induction v with a p, induction p: append (apply inl) (apply inr); constructor; assumption}, + { intro p, + induction p with v v: induction v; constructor; append (apply inl) (apply inr); assumption}, + { intro p, induction p with v v: induction v; reflexivity}, + { intro v, induction v with a p, induction p: reflexivity}, + end + /- ** Universal mapping properties -/ /- *** The positive universal property. -/ @@ -365,7 +415,7 @@ namespace sigma begin revert A B HA HB, induction n with n IH, - { intro A B HA HB, fapply is_trunc_equiv_closed_rev, apply sigma_equiv_of_is_contr_pr1}, + { intro A B HA HB, fapply is_trunc_equiv_closed_rev, apply sigma_equiv_of_is_contr_left}, { intro A B HA HB, apply is_trunc_succ_intro, intro u v, apply is_trunc_equiv_closed_rev, apply sigma_eq_equiv, diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index 1d08ea8f2..e380e49c8 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -260,3 +260,5 @@ namespace decidable end end decidable + +attribute sum.is_trunc_sum [instance] [priority 1480]