diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean index 0c32a6fed..1719eb5f9 100644 --- a/library/hott/axioms/ua.lean +++ b/library/hott/axioms/ua.lean @@ -13,7 +13,7 @@ private definition isequiv_path (H : A ≈ B) := (@IsEquiv.transport Type (λX, X) A B H) definition equiv_path (H : A ≈ B) : A ≃ B := - Equiv_mk _ (isequiv_path A B H) + Equiv.mk _ (isequiv_path A B H) axiom ua_equiv (A B : Type) : IsEquiv (equiv_path A B) diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean index d1cd543fe..c682a009d 100644 --- a/library/hott/equiv.lean +++ b/library/hott/equiv.lean @@ -2,7 +2,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jeremy Avigad, Jakob von Raumer -- Ported from Coq HoTT -import .path .trunc +import .path open path function -- Equivalences @@ -16,38 +16,37 @@ definition Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ -- Structure IsEquiv inductive IsEquiv [class] {A B : Type} (f : A → B) := -IsEquiv_mk : Π +mk : Π (inv : B → A) (retr : Sect inv f) (sect : Sect f inv) (adj : Πx, retr (f x) ≈ ap f (sect x)), IsEquiv f - namespace IsEquiv - definition inv [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] : B → A := + definition inv {A B : Type} (f : A → B) [H : IsEquiv f] : B → A := IsEquiv.rec (λinv retr sect adj, inv) H -- TODO: note: does not type check without giving the type - definition retr [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] : Sect (inv f) f := + definition retr {A B : Type} (f : A → B) [H : IsEquiv f] : Sect (inv f) f := IsEquiv.rec (λinv retr sect adj, retr) H - definition sect [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] : Sect f (inv f) := + definition sect {A B : Type} (f : A → B) [H : IsEquiv f] : Sect f (inv f) := IsEquiv.rec (λinv retr sect adj, sect) H - definition adj [coercion] {A B : Type} (f : A → B) [H : IsEquiv f] : + definition adj {A B : Type} (f : A → B) [H : IsEquiv f] : Πx, retr f (f x) ≈ ap f (sect f x) := IsEquiv.rec (λinv retr sect adj, adj) H - notation e `⁻¹` := inv e + postfix `⁻¹` := inv end IsEquiv -- Structure Equiv inductive Equiv (A B : Type) : Type := -Equiv_mk : Π +mk : Π (equiv_fun : A → B) (equiv_isequiv : IsEquiv equiv_fun), Equiv A B @@ -57,7 +56,7 @@ namespace Equiv definition equiv_fun [coercion] {A B : Type} (e : Equiv A B) : A → B := Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e - definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) := + definition equiv_isequiv [instance] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) := Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e infix `≃`:25 := Equiv @@ -71,12 +70,12 @@ namespace IsEquiv -- The identity function is an equivalence. - definition id_closed [instance] : (@IsEquiv A A id) := IsEquiv_mk id (λa, idp) (λa, idp) (λa, idp) + definition id_closed [instance] : (@IsEquiv A A id) := IsEquiv.mk id (λa, idp) (λa, idp) (λa, idp) -- The composition of two equivalences is, again, an equivalence. - definition comp_closed (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) := - IsEquiv_mk ((inv f) ∘ (inv g)) + definition comp_closed [instance] (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) := + IsEquiv.mk ((inv f) ∘ (inv g)) (λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c) (λa, ap (inv f) (sect g (f a)) ⬝ sect f a) (λa, (whiskerL _ (adj g (f a))) ⬝ @@ -123,7 +122,7 @@ namespace IsEquiv ... ≈ (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : {!ap_V⁻¹} ... ≈ ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : !ap_pp⁻¹, eq3) in - IsEquiv_mk (inv f) sect' retr' adj' + IsEquiv.mk (inv f) sect' retr' adj' end IsEquiv namespace IsEquiv @@ -165,15 +164,15 @@ namespace IsEquiv have eq4 : ret (f a) ≈ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a), from moveR_M1 _ _ eq3, eq4) in - IsEquiv_mk g ret sect' adj' + IsEquiv.mk g ret sect' adj' end end IsEquiv namespace IsEquiv - variables {A B: Type} {f : A → B} + variables {A B: Type} (f : A → B) --The inverse of an equivalence is, again, an equivalence. - definition inv_closed (Hf : IsEquiv f) : (IsEquiv (inv f)) := + definition inv_closed [instance] [Hf : IsEquiv f] : (IsEquiv (inv f)) := adjointify (inv f) f (sect f) (retr f) end IsEquiv @@ -185,10 +184,10 @@ namespace IsEquiv include Hf definition cancel_R (g : B → C) [Hgf : IsEquiv (g ∘ f)] : (IsEquiv g) := - homotopic (comp_closed (inv_closed Hf) Hgf) (λb, ap g (retr f b)) + homotopic (comp_closed !inv_closed Hgf) (λb, ap g (retr f b)) definition cancel_L (g : C → A) [Hgf : IsEquiv (f ∘ g)] : (IsEquiv g) := - homotopic (comp_closed Hgf (inv_closed Hf)) (λa, sect f (g a)) + homotopic (comp_closed Hgf !inv_closed) (λa, sect f (g a)) --Rewrite rules definition moveR_M {x : A} {y : B} (p : x ≈ (inv f) y) : (f x ≈ y) := @@ -203,10 +202,7 @@ namespace IsEquiv definition moveL_V {x : B} {y : A} (p : f y ≈ x) : y ≈ (inv f) x := (moveR_V f (p⁻¹))⁻¹ - definition contr (HA: Contr A) : (Contr B) := - Contr.Contr_mk (f (center HA)) (λb, moveR_M f (contr HA (inv f b))) - - definition ap_closed (x y : A) : IsEquiv (@ap A B f x y) := + definition ap_closed [instance] (x y : A) : IsEquiv (ap f) := adjointify (ap f) (λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y) (λq, !ap_pp @@ -247,7 +243,7 @@ namespace IsEquiv --Transporting is an equivalence definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (IsEquiv (transport P p)) := - IsEquiv_mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p) + IsEquiv.mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p) end IsEquiv @@ -256,31 +252,28 @@ namespace Equiv parameters {A B C : Type} (eqf : A ≃ B) private definition f : A → B := equiv_fun eqf - private definition Hf [instance] : IsEquiv f := equiv_isequiv eqf + private definition Hf : IsEquiv f := equiv_isequiv eqf - protected definition id : A ≃ A := Equiv_mk id IsEquiv.id_closed + protected definition id : A ≃ A := Equiv.mk id IsEquiv.id_closed theorem compose (eqg: B ≃ C) : A ≃ C := - Equiv_mk ((equiv_fun eqg) ∘ f) + Equiv.mk ((equiv_fun eqg) ∘ f) (IsEquiv.comp_closed Hf (equiv_isequiv eqg)) theorem path_closed (f' : A → B) (Heq : equiv_fun eqf ≈ f') : A ≃ B := - Equiv_mk f' (IsEquiv.path_closed Hf Heq) + Equiv.mk f' (IsEquiv.path_closed Hf Heq) theorem inv_closed : B ≃ A := - Equiv_mk (IsEquiv.inv f) (IsEquiv.inv_closed Hf) + Equiv.mk (IsEquiv.inv f) !IsEquiv.inv_closed theorem cancel_R {g : B → C} (Hgf : IsEquiv (g ∘ f)) : B ≃ C := - Equiv_mk g (IsEquiv.cancel_R f _) + Equiv.mk g (IsEquiv.cancel_R f _) theorem cancel_L {g : C → A} (Hgf : IsEquiv (f ∘ g)) : C ≃ A := - Equiv_mk g (IsEquiv.cancel_L f _) + Equiv.mk g (IsEquiv.cancel_L f _) theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) := - Equiv_mk (transport P p) (IsEquiv.transport P p) - - theorem contr_closed (HA: Contr A) : (Contr B) := - IsEquiv.contr f HA + Equiv.mk (transport P p) (IsEquiv.transport P p) end @@ -291,15 +284,3 @@ namespace Equiv calc_symm inv_closed end Equiv - -namespace Equiv - variables {A B : Type} {HA : Contr A} {HB : Contr B} - - --Each two contractible types are equivalent. - definition contr_contr : A ≃ B := - Equiv_mk - (λa, center HB) - (IsEquiv.adjointify (λa, center HB) (λb, center HA) - (contr HB) (contr HA)) - -end Equiv diff --git a/library/hott/equiv_precomp.lean b/library/hott/equiv_precomp.lean index 287fcb130..ae25b7e5d 100644 --- a/library/hott/equiv_precomp.lean +++ b/library/hott/equiv_precomp.lean @@ -72,11 +72,11 @@ namespace Equiv private definition Hf := equiv_isequiv eqf definition precompose : (B → C) ≃ (A → C) := - Equiv_mk (IsEquiv.precomp f C) + Equiv.mk (IsEquiv.precomp f C) (@IsEquiv.precompose A B f Hf C) definition postcompose : (C → A) ≃ (C → B) := - Equiv_mk (IsEquiv.postcomp f C) + Equiv.mk (IsEquiv.postcomp f C) (@IsEquiv.postcompose A B f Hf C) end diff --git a/library/hott/logic.lean b/library/hott/logic.lean new file mode 100644 index 000000000..bd41ed824 --- /dev/null +++ b/library/hott/logic.lean @@ -0,0 +1,9 @@ +import data.empty .path + +open path +inductive tdecidable [class] (A : Type) : Type := +inl : A → tdecidable A, +inr : ~A → tdecidable A + +structure decidable_paths [class] (A : Type) := +(elim : ∀(x y : A), tdecidable (x ≈ y)) diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index 39cc28321..d4a40f22c 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -1,114 +1,243 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad, Floris van Doorn +-- Authors: Jeremy Avigad, Floris van Doorn -- Ported from Coq HoTT -import .path data.nat.basic data.empty data.unit data.sigma -open path nat sigma + +import .path .logic data.nat.basic data.empty data.unit data.sigma .equiv +open path nat sigma unit -- Truncation levels -- ----------------- -- TODO: make everything universe polymorphic -structure contr_internal (A : Type₊) := -mk :: (center : A) (contr : Π(a : A), center ≈ a) +-- TODO: everything definition with a hprop as codomain can be a theorem? -inductive trunc_index : Type := -minus_two : trunc_index, -trunc_S : trunc_index → trunc_index +/- truncation indices -/ namespace truncation -postfix `.+1`:max := trunc_index.trunc_S -postfix `.+2`:max := λn, (n .+1 .+1) -notation `-2` := trunc_index.minus_two -notation `-1` := (-2.+1) + inductive trunc_index : Type := + minus_two : trunc_index, + trunc_S : trunc_index → trunc_index -definition trunc_index_add (n m : trunc_index) : trunc_index := -trunc_index.rec_on m n (λ k l, l .+1) + postfix `.+1`:10000 := trunc_index.trunc_S + postfix `.+2`:10000 := λn, (n .+1 .+1) + notation `-2` := trunc_index.minus_two + notation `-1` := (-2.+1) --- Coq calls this `-2+`, but `+2+` looks more natural, since trunc_index_add 0 0 = 2 -infix `+2+`:65 := trunc_index_add + namespace trunc_index + definition add (n m : trunc_index) : trunc_index := + trunc_index.rec_on m n (λ k l, l .+1) -definition trunc_index_leq (n m : trunc_index) : Type₁ := -trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m + definition leq (n m : trunc_index) : Type₁ := + trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m + end trunc_index -notation x <= y := trunc_index_leq x y -notation x ≤ y := trunc_index_leq x y + -- Coq calls this `-2+`, but `+2+` looks more natural, since trunc_index_add 0 0 = 2 + infix `+2+`:65 := add -definition nat_to_trunc_index [coercion] (n : nat) : trunc_index := -nat.rec_on n (-1.+1) (λ n k, k.+1) + notation x <= y := trunc_index.leq x y + notation x ≤ y := trunc_index.leq x y -definition is_trunc_internal (n : trunc_index) : Type₁ → Type₁ := -trunc_index.rec_on n (λA, contr_internal A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) + namespace trunc_index + definition succ_le {n m : trunc_index} (H : n ≤ m) : n.+1 ≤ m.+1 := H + definition succ_le_cancel {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m := H + definition minus_two_le (n : trunc_index) : -2 ≤ n := star + definition not_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty := H + end trunc_index -structure is_trunc [class] (n : trunc_index) (A : Type) := -mk :: (to_internal : is_trunc_internal n A) + definition nat_to_trunc_index [coercion] (n : nat) : trunc_index := + nat.rec_on n (-1.+1) (λ n k, k.+1) --- should this be notation or definitions ---prefix `is_contr`:max := is_trunc -2 -definition is_contr := is_trunc -2 -definition is_hprop := is_trunc -1 -definition is_hset := is_trunc nat.zero + /- truncated types -/ -variable {A : Type₁} + /- + Just as in Coq HoTT we define an internal version of contractibility and is_trunc, but we only + use `is_trunc` and `is_contr` + -/ -definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A := -is_trunc.mk (contr_internal.mk center contr) + structure contr_internal (A : Type₊) := + (center : A) (contr : Π(a : A), center ≈ a) -definition center (A : Type₁) [H : is_contr A] : A := -@contr_internal.center A is_trunc.to_internal + definition is_trunc_internal (n : trunc_index) : Type₁ → Type₁ := + trunc_index.rec_on n (λA, contr_internal A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) -definition contr [H : is_contr A] (a : A) : !center ≈ a := -@contr_internal.contr A is_trunc.to_internal a + structure is_trunc [class] (n : trunc_index) (A : Type₁) := + (to_internal : is_trunc_internal n A) -definition is_trunc_succ (A : Type₁) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)] - : is_trunc (n.+1) A := -is_trunc.mk (λ x y, is_trunc.to_internal) + -- should this be notation or definitions? + notation `is_contr` := is_trunc -2 + notation `is_hprop` := is_trunc -1 + notation `is_hset` := is_trunc nat.zero + -- definition is_contr := is_trunc -2 + -- definition is_hprop := is_trunc -1 + -- definition is_hset := is_trunc 0 -definition succ_is_trunc {n : trunc_index} [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) := -is_trunc.mk (is_trunc.to_internal x y) + variables {A B : Type₁} -definition path_contr [H : is_contr A] (x y : A) : x ≈ y := -(contr x)⁻¹ ⬝ (contr y) + -- maybe rename to is_trunc_succ.mk + definition is_trunc_succ (A : Type₁) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)] + : is_trunc n.+1 A := + is_trunc.mk (λ x y, is_trunc.to_internal) -definition path2_contr {A : Type₁} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q := -have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp), -K p⁻¹ ⬝ K q + -- maybe rename to is_trunc_succ.elim + definition succ_is_trunc {n : trunc_index} [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) := + is_trunc.mk (is_trunc.to_internal x y) -definition contr_paths_contr [instance] {A : Type₁} [H : is_contr A] (x y : A) : is_contr (x ≈ y) := -is_contr.mk !path_contr (λ p, !path2_contr) + /- contractibility -/ -definition trunc_succ (A : Type₁) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A := -trunc_index.rec_on n - (λ A (H : is_contr A), !is_trunc_succ) - (λ n IH A (H : is_trunc (n.+1) A), @is_trunc_succ _ _ (λ x y, IH _ !succ_is_trunc)) - A H ---in the proof the type of H is given explicitly to make it available for class inference + definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A := + is_trunc.mk (contr_internal.mk center contr) -definition contr_basedpaths [instance] {A : Type₁} (a : A) : is_contr (Σ(x : A), a ≈ x) := -is_contr.mk (dpair a idp) (λp, sorry) + definition center (A : Type₁) [H : is_contr A] : A := + @contr_internal.center A is_trunc.to_internal --- Definition trunc_contr {n} {A} `{Contr A} : IsTrunc n A --- := (@trunc_leq -2 n tt _ _). + definition contr [H : is_contr A] (a : A) : !center ≈ a := + @contr_internal.contr A is_trunc.to_internal a --- Definition trunc_hprop {n} {A} `{IsHProp A} : IsTrunc n.+1 A --- := (@trunc_leq -1 n.+1 tt _ _). + definition path_contr [H : is_contr A] (x y : A) : x ≈ y := + contr x⁻¹ ⬝ (contr y) --- Definition trunc_hset {n} {A} `{IsHSet A} : IsTrunc n.+1.+1 A --- := (@trunc_leq 0 n.+1.+1 tt _ _). + definition path2_contr {A : Type₁} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q := + have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp), + K p⁻¹ ⬝ K q -definition trunc_leq [instance] {A : Type₁} {m n : trunc_index} (H : m ≤ n) - [H : is_trunc m A] : is_trunc n A := -sorry + definition contr_paths_contr [instance] {A : Type₁} [H : is_contr A] (x y : A) : is_contr (x ≈ y) := + is_contr.mk !path_contr (λ p, !path2_contr) -definition is_hprop.mk (A : Type₁) (H : ∀x y : A, x ≈ y) : is_hprop A := sorry -definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y := sorry + /- truncation is upward close -/ -definition is_trunc_is_hprop {n : trunc_index} : is_hprop (is_trunc n A) := sorry + -- n-types are also (n+1)-types + definition trunc_succ [instance] (A : Type₁) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A := + trunc_index.rec_on n + (λ A (H : is_contr A), !is_trunc_succ) + (λ n IH A (H : is_trunc (n.+1) A), @is_trunc_succ _ _ (λ x y, IH _ !succ_is_trunc)) + A H + --in the proof the type of H is given explicitly to make it available for class inference -definition is_hset.mk (A : Type₁) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A := sorry -definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x ≈ y) : p ≈ q := sorry + definition trunc_leq (A : Type₁) (n m : trunc_index) (Hnm : n ≤ m) + [Hn : is_trunc n A] : is_trunc m A := + have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from + λ k A, trunc_index.cases_on k + (λh1 h2, h2) + (λk h1 h2, empty.elim (is_trunc -2 A) (trunc_index.not_succ_le_minus_two h1)), + have step : Π (m : trunc_index) + (IHm : Π (n : trunc_index) (A : Type₁), n ≤ m → is_trunc n A → is_trunc m A) + (n : trunc_index) (A : Type₁) + (Hnm : n ≤ m .+1) (Hn : is_trunc n A), is_trunc m .+1 A, from + λm IHm n, trunc_index.rec_on n + (λA Hnm Hn, @trunc_succ A m (IHm -2 A star Hn)) + (λn IHn A Hnm (Hn : is_trunc n.+1 A), + @is_trunc_succ A m (λx y, IHm n (x≈y) (trunc_index.succ_le_cancel Hnm) !succ_is_trunc)), + trunc_index.rec_on m base step n A Hnm Hn + + -- the following cannot be instances in their current form, because it is looping + definition trunc_contr (A : Type₁) (n : trunc_index) [H : is_contr A] : is_trunc n A := + trunc_index.rec_on n H _ + + definition trunc_hprop (A : Type₁) (n : trunc_index) [H : is_hprop A] + : is_trunc (n.+1) A := + trunc_leq A -1 (n.+1) star + + definition trunc_hset (A : Type₁) (n : trunc_index) [H : is_hset A] + : is_trunc (n.+2) A := + trunc_leq A 0 (n.+2) star + + /- hprops -/ + + definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y := + @center _ !succ_is_trunc + + definition contr_inhabited_hprop {A : Type₁} [H : is_hprop A] (x : A) : is_contr A := + is_contr.mk x (λy, !is_hprop.elim) + + --Coq has the following as instance, but doesn't look too useful + definition hprop_inhabited_contr {A : Type₁} (H : A → is_contr A) : is_hprop A := + @is_trunc_succ A -2 + (λx y, + have H2 [visible] : is_contr A, from H x, + !contr_paths_contr) + + definition is_hprop.mk {A : Type₁} (H : ∀x y : A, x ≈ y) : is_hprop A := + hprop_inhabited_contr (λ x, is_contr.mk x (H x)) + + /- hsets -/ + + definition is_hset.mk (A : Type₁) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A := + @is_trunc_succ _ _ (λ x y, is_hprop.mk (H x y)) + + definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x ≈ y) : p ≈ q := + @is_hprop.elim _ !succ_is_trunc p q + + /- instances -/ + + definition contr_basedpaths [instance] {A : Type₁} (a : A) : is_contr (Σ(x : A), a ≈ x) := + is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, path.rec_on q idp)) + + definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry + + definition unit_contr [instance] : is_contr unit := + is_contr.mk star (λp, unit.rec_on p idp) + + definition empty_hprop [instance] : is_hprop empty := + is_hprop.mk (λx, !empty.elim x) + + /- truncated universe -/ + + structure trunctype (n : trunc_index) := + (trunctype_type : Type₁) (is_trunc_trunctype_type : is_trunc n trunctype_type) + coercion trunctype.trunctype_type + + notation n `-Type` := trunctype n + notation `hprop` := -1-Type. + notation `hset` := 0-Type. + + definition hprop.mk := @trunctype.mk -1 + definition hset.mk := @trunctype.mk 0 + + --what does the following line in Coq do? + --Canonical Structure default_TruncType := fun n T P => (@BuildTruncType n T P). + + /- interaction with equivalences -/ + + section + open IsEquiv Equiv + + --should we remove the following two theorems as they are special cases of "trunc_equiv" + definition equiv_preserves_contr (f : A → B) [Hf : IsEquiv f] [HA: is_contr A] : (is_contr B) := + is_contr.mk (f (center A)) (λp, moveR_M f !contr) + + theorem contr_equiv (f : A ≃ B) [HA: is_contr A] : is_contr B := + equiv_preserves_contr f + + definition contr_equiv_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B := + Equiv.mk + (λa, center B) + (IsEquiv.adjointify (λa, center B) (λb, center A) contr contr) + + definition trunc_equiv (n : trunc_index) (f : A → B) [H : IsEquiv f] [HA : is_trunc n A] + : is_trunc n B := + trunc_index.rec_on n + (λA (HA : is_contr A) B f (H : IsEquiv f), !equiv_preserves_contr) + (λn IH A (HA : is_trunc n.+1 A) B f (H : IsEquiv f), @is_trunc_succ _ _ (λ x y : B, + IH (f⁻¹ x ≈ f⁻¹ y) !succ_is_trunc (x ≈ y) ((ap (f⁻¹))⁻¹) !inv_closed)) + A HA B f H + + definition trunc_equiv' (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] : is_trunc n B := + trunc_equiv n f + + definition isequiv_iff_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A) + : IsEquiv f := + IsEquiv.adjointify f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) + + -- definition equiv_iff_hprop_uncurried [HA : is_hprop A] [HB : is_hprop B] : (A ↔ B) → (A ≃ B) := sorry + + definition equiv_iff_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A) : A ≃ B := + Equiv.mk f (isequiv_iff_hprop f g) + end + + -- TODO: port "Truncated morphisms" end truncation