feat(library): port more of truncation library from Coq HoTT

Everything directly about truncations in the basic truncation library is ported.
Some theorems about other structures still need to be ported.
Also made some minor changes in hott.equiv

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)
 

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)) :=
+  definition comp_closed [instance] (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) :=
-    IsEquiv_mk ((inv f) ∘ (inv g))
+    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) :=
+  definition ap_closed [instance] (x y : A) : IsEquiv (ap f) := 
-    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) := 
     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)
+    Equiv.mk (transport P p) (IsEquiv.transport P p)
-
-  theorem contr_closed (HA: Contr A) : (Contr B) :=
-    IsEquiv.contr f HA
 
   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

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

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))

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₊) :=
+-- TODO: everything definition with a hprop as codomain can be a theorem?
-mk :: (center : A) (contr : Π(a : A), center ≈ a)
 
-inductive trunc_index : Type :=
+/- truncation indices -/
-minus_two : trunc_index,
-trunc_S : trunc_index → trunc_index
 
 namespace truncation
 
-postfix `.+1`:max := trunc_index.trunc_S
+  inductive trunc_index : Type :=
-postfix `.+2`:max := λn, (n .+1 .+1)
+  minus_two : trunc_index,
-notation `-2` := trunc_index.minus_two
+  trunc_S : trunc_index → trunc_index
-notation `-1` := (-2.+1)
 
-definition trunc_index_add (n m : trunc_index) : trunc_index :=
+  postfix `.+1`:10000 := trunc_index.trunc_S
-trunc_index.rec_on m n (λ k l, l .+1)
+  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
+  namespace trunc_index
-infix `+2+`:65 := trunc_index_add
+  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₁ :=
+  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
+  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
+  -- Coq calls this `-2+`, but `+2+` looks more natural, since trunc_index_add 0 0 = 2
-notation x ≤ y := trunc_index_leq x y
+  infix `+2+`:65 := add
 
-definition nat_to_trunc_index [coercion] (n : nat) : trunc_index :=
+  notation x <= y := trunc_index.leq x y
-nat.rec_on n (-1.+1) (λ n k, k.+1)
+  notation x ≤ y := trunc_index.leq x y
 
-definition is_trunc_internal (n : trunc_index) : Type₁ → Type₁ :=
+  namespace trunc_index
-trunc_index.rec_on n (λA, contr_internal A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y)))
+  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) :=
+  definition nat_to_trunc_index [coercion] (n : nat) : trunc_index :=
-mk :: (to_internal : is_trunc_internal n A)
+  nat.rec_on n (-1.+1) (λ n k, k.+1)
 
--- should this be notation or definitions
+  /- truncated types -/
---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
 
-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 :=
+  structure contr_internal (A : Type₊) :=
-is_trunc.mk (contr_internal.mk center contr)
+  (center : A) (contr : Π(a : A), center ≈ a)
 
-definition center (A : Type₁) [H : is_contr A] : A :=
+  definition is_trunc_internal (n : trunc_index) : Type₁ → Type₁ :=
-@contr_internal.center A is_trunc.to_internal
+  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 :=
+  structure is_trunc [class] (n : trunc_index) (A : Type₁) :=
-@contr_internal.contr A is_trunc.to_internal a
+  (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)]
+  -- should this be notation or definitions?
-  : is_trunc (n.+1) A :=
+  notation `is_contr` := is_trunc -2
-is_trunc.mk (λ x y, is_trunc.to_internal)
+  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) :=
+  variables {A B : Type₁}
-is_trunc.mk (is_trunc.to_internal x y)
 
-definition path_contr [H : is_contr A] (x y : A) : x ≈ y :=
+  -- maybe rename to is_trunc_succ.mk
-(contr x)⁻¹ ⬝ (contr y)
+  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 :=
+  -- maybe rename to is_trunc_succ.elim
-have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp),
+  definition succ_is_trunc {n : trunc_index} [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) :=
-K p⁻¹ ⬝ K q
+  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) :=
+  /- contractibility -/
-is_contr.mk !path_contr (λ p, !path2_contr)
 
-definition trunc_succ (A : Type₁) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A :=
+  definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A :=
-trunc_index.rec_on n
+  is_trunc.mk (contr_internal.mk center contr)
-  (λ 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 contr_basedpaths [instance] {A : Type₁} (a : A) : is_contr (Σ(x : A), a ≈ x) :=
+  definition center (A : Type₁) [H : is_contr A] : A :=
-is_contr.mk (dpair a idp) (λp, sorry)
+  @contr_internal.center A is_trunc.to_internal
 
--- Definition trunc_contr {n} {A} `{Contr A} : IsTrunc n A
+  definition contr [H : is_contr A] (a : A) : !center ≈ a :=
---   := (@trunc_leq -2 n tt _ _).
+  @contr_internal.contr A is_trunc.to_internal a
 
--- Definition trunc_hprop {n} {A} `{IsHProp A} : IsTrunc n.+1 A
+  definition path_contr [H : is_contr A] (x y : A) : x ≈ y :=
---   := (@trunc_leq -1 n.+1 tt _ _).
+  contr x⁻¹ ⬝ (contr y)
 
--- Definition trunc_hset {n} {A} `{IsHSet A} : IsTrunc n.+1.+1 A
+  definition path2_contr {A : Type₁} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q :=
---   := (@trunc_leq 0 n.+1.+1 tt _ _).
+  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)
+  definition contr_paths_contr [instance] {A : Type₁} [H : is_contr A] (x y : A) : is_contr (x ≈ y) :=
-  [H : is_trunc m A] : is_trunc n A :=
+  is_contr.mk !path_contr (λ p, !path2_contr)
-sorry
 
-definition is_hprop.mk (A : Type₁) (H : ∀x y : A, x ≈ y) : is_hprop A := sorry
+  /- truncation is upward close -/
-definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y := sorry
 
-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