feat(hott): add definitions using truncations and theorems about them

define embedding, (split) surjection, retraction, existential quantifier, 'or' connective also add a whole bunch of theorems about these definitions still has two sorry's which can be solved after #564 is closed
2015-04-28 20:48:39 -04:00 · 2015-04-28 20:48:39 -04:00 · 297d50378d
commit 297d50378d
parent 15c2ee289f
17 changed files with 644 additions and 228 deletions
--- a/hott/algebra/category/adjoint.hlean
+++ b/hott/algebra/category/adjoint.hlean
@ -2,92 +2,111 @@
 Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

-Module: algebra.category.adjoint
+Module: algebra.precategory.adjoint
 Authors: Floris van Doorn
 -/

-import .constructions.functor
+import algebra.category.constructions .constructions types.function arity

-open category functor nat_trans eq is_trunc iso equiv prod
-
-variables {C D : Precategory} {F : C ⇒ D}
-
-- structure adjoint (F : C ⇒ D) (G : D ⇒ C) :=
--   (unit : functor.id ⟹ G ∘f F) -- η
--   (counit : F ∘f G ⟹ functor.id) -- ε
--   (H : (counit ∘nf F) ∘n (nat_trans_of_eq !functor.assoc) ∘n (F ∘fn unit)
--     = nat_trans_of_eq !functor.comp_id_eq_id_comp)
--   (K : (G ∘fn counit) ∘n (nat_trans_of_eq !functor.assoc⁻¹) ∘n (unit ∘nf G)
--     = nat_trans_of_eq !functor.comp_id_eq_id_comp⁻¹)
-
-- structure is_left_adjoint (F : C ⇒ D) :=
--   (right_adjoint : D ⇒ C) -- G
--   (is_adjoint : adjoint F right_adjoint)
-
-structure is_left_adjoint (F : C ⇒ D) :=
-  (right_adjoint : D ⇒ C) -- G
-  (unit : functor.id ⟹ right_adjoint ∘f F) -- η
-  (counit : F ∘f right_adjoint ⟹ functor.id) -- ε
-  (H : (counit ∘nf F) ∘n (nat_trans_of_eq !functor.assoc) ∘n (F ∘fn unit)
-    = nat_trans_of_eq !functor.comp_id_eq_id_comp)
-  (K : (right_adjoint ∘fn counit) ∘n (nat_trans_of_eq !functor.assoc⁻¹) ∘n (unit ∘nf right_adjoint)
-    = nat_trans_of_eq !functor.comp_id_eq_id_comp⁻¹)
-
-structure is_equivalence (F : C ⇒ D) extends is_left_adjoint F :=
-  mk' ::
-  (is_iso_unit : is_iso unit)
-  (is_iso_counit : is_iso counit)
-
-structure equivalence (C D : Precategory) :=
-  (to_functor : C ⇒ D)
-  (struct : is_equivalence to_functor)
-
--TODO: review and change
--TODO: make some or all of these structures?
-definition faithful (F : C ⇒ D) :=
-Π⦃c c' : C⦄, (Π(f f' : c ⟶ c'), to_fun_hom F f = to_fun_hom F f' → f = f')
-
-definition full (F : C ⇒ D) := Π⦃c c' : C⦄ (g : F c ⟶ F c'), Σ(f : c ⟶ c'), F f = g --merely
-
-definition fully_faithful (F : C ⇒ D) := Π⦃c c' : C⦄, is_equiv (@to_fun_hom _ _ F c c')
-
-definition split_essentially_surjective (F : C ⇒ D) :=
-Π⦃d : D⦄, Σ(c : C), F c ≅ d
-
-definition essentially_surjective (F : C ⇒ D) :=
-Π⦃d : D⦄, Σ(c : C), F c ≅ d --merely
-
-definition is_weak_equivalence (F : C ⇒ D) :=
-fully_faithful F × essentially_surjective F
-
-definition is_isomorphism (F : C ⇒ D) :=
-fully_faithful F × is_equiv (to_fun_ob F)
-
-structure isomorphism (C D : Precategory) :=
-  (to_functor : C ⇒ D)
-  (struct : is_isomorphism to_functor)
+open category functor nat_trans eq is_trunc iso equiv prod trunc function

 namespace category
+  variables {C D : Precategory} {F : C ⇒ D}

+  -- do we want to have a structure "is_adjoint" and define
+  -- structure is_left_adjoint (F : C ⇒ D) :=
+  --   (right_adjoint : D ⇒ C) -- G
+  --   (is_adjoint : adjoint F right_adjoint)
+
+  structure is_left_adjoint [class] (F : C ⇒ D) :=
+    (G : D ⇒ C)
+    (η : functor.id ⟹ G ∘f F)
+    (ε : F ∘f G ⟹ functor.id)
+    (H : Π(c : C), (ε (F c)) ∘ (F (η c)) = ID (F c))
+    (K : Π(d : D), (G (ε d)) ∘ (η (G d)) = ID (G d))
+
+  abbreviation right_adjoint := @is_left_adjoint.G
+  abbreviation unit          := @is_left_adjoint.η
+  abbreviation counit        := @is_left_adjoint.ε
+
+  -- structure is_left_adjoint [class] (F : C ⇒ D) :=
+  --   (right_adjoint : D ⇒ C) -- G
+  --   (unit : functor.id ⟹ right_adjoint ∘f F) -- η
+  --   (counit : F ∘f right_adjoint ⟹ functor.id) -- ε
+  --   (H : Π(c : C), (counit (F c)) ∘ (F (unit c)) = ID (F c))
+  --   (K : Π(d : D), (right_adjoint (counit d)) ∘ (unit (right_adjoint d)) = ID (right_adjoint d))
+
+  structure is_equivalence [class] (F : C ⇒ D) extends is_left_adjoint F :=
+    mk' ::
+    (is_iso_unit : is_iso η)
+    (is_iso_counit : is_iso ε)
+
+  structure equivalence (C D : Precategory) :=
+    (to_functor : C ⇒ D)
+    (struct : is_equivalence to_functor)
+
+  --TODO: review and change
+  --TODO: make some or all of these structures?
+  definition faithful (F : C ⇒ D) :=
+  Π⦃c c' : C⦄ (f f' : c ⟶ c'), F f = F f' → f = f'
+
+  definition full (F : C ⇒ D) := Π⦃c c' : C⦄ (g : F c ⟶ F c'), ∃(f : c ⟶ c'), F f = g
+
+  definition fully_faithful [reducible] (F : C ⇒ D) := Π⦃c c' : C⦄, is_equiv (@to_fun_hom _ _ F c c')
+
+  definition split_essentially_surjective (F : C ⇒ D) :=
+  Π⦃d : D⦄, Σ(c : C), F c ≅ d
+
+  definition essentially_surjective (F : C ⇒ D) :=
+  Π⦃d : D⦄, ∃(c : C), F c ≅ d
+
+  definition is_weak_equivalence (F : C ⇒ D) :=
+  fully_faithful F × essentially_surjective F
+
+  definition is_isomorphism (F : C ⇒ D) :=
+  fully_faithful F × is_equiv (to_fun_ob F)
+
+  structure isomorphism (C D : Precategory) :=
+    (to_functor : C ⇒ D)
+    (struct : is_isomorphism to_functor)
  --   infix `⊣`:55 := adjoint

-  infix `⋍`:25 := equivalence -- \backsimeq
-  infix `≌`:25 := isomorphism -- \backcong
-  --TODO: add shortcuts for Σ⋍≌▹
+  infix `⋍`:25 := equivalence -- \backsimeq or \equiv
+  infix `≌`:25 := isomorphism -- \backcong or \iso

  definition is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
    : is_hprop (is_left_adjoint F) :=
-  sorry
+  begin
+    apply is_hprop.mk,
+    intros [G, G'], cases G with [G, η, ε, H, K], cases G' with [G', η', ε', H', K'],
+    fapply (apd011111 is_left_adjoint.mk),
+    { fapply functor_eq,
+      { intro d, apply eq_of_iso, fapply iso.MK,
+        { exact (G' (ε d) ∘ η' (G d))},
+        { exact (G (ε' d) ∘ η (G' d))},
+        { apply sorry /-rewrite [assoc, -{((G (ε' d)) ∘ (η (G' d))) ∘ (G' (ε d))}(assoc)],-/
+--        apply concat, apply (ap (λc, c ∘ η' _)), rewrite -assoc, apply idp
+},
+--/-rewrite [-nat_trans.assoc]-/apply sorry
+---assoc (G (ε' d)) (η (G' d)) (G' (ε d))
+        { apply sorry}},
+      { apply sorry},
+},
+    { apply sorry},
+    { apply sorry},
+    { apply is_hprop.elim},
+    { apply is_hprop.elim},
+  end

  definition is_equivalence.mk (F : C ⇒ D) (G : D ⇒ C) (η : G ∘f F ≅ functor.id)
    (ε : F ∘f G ≅ functor.id) : is_equivalence F :=
  sorry

  definition full_of_fully_faithful (H : fully_faithful F) : full F :=
-  sorry
+  sorry --λc c' g, trunc.elim _ _

  definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F :=
-  sorry
+  λc c' f f' p, is_injective_of_is_embedding p

  definition fully_faithful_of_full_of_faithful (H : faithful F) (K : full F) : fully_faithful F :=
  sorry
@ -118,7 +137,7 @@ namespace category
  sorry

  definition is_isomorphism_equiv2 (F : C ⇒ D) : is_equivalence F
-    ≃ Σ/-MERELY-/(G : D ⇒ C), functor.id = G ∘f F × F ∘f G = functor.id :=
+    ≃ ∃(G : D ⇒ C), functor.id = G ∘f F × F ∘f G = functor.id :=
  sorry

  definition is_equivalence_of_isomorphism (H : is_isomorphism F) : is_equivalence F :=
--- a/hott/algebra/category/constructions/functor.hlean
+++ b/hott/algebra/category/constructions/functor.hlean
@ -159,14 +159,20 @@ namespace category

  end functor

-  definition Category_functor_of_precategory (D : Category) (C : Precategory) : Category :=
-  category.MK (D ^c C) (functor.is_univalent D C)
+  definition category_functor [instance] (D : Category) (C : Precategory)
+    : category (D ^c C) :=
+  category.mk (D ^c C) (functor.is_univalent D C)

-  definition Category_functor (D : Category) (C : Category) : Category :=
-  Category_functor_of_precategory D C
+  definition Category_functor (D : Category) (C : Precategory) : Category :=
+  category.Mk (D ^c C) !category_functor
+
+  --this definition is only useful if the exponent is a category,
+  --  and the elaborator has trouble with inserting the coercion
+  definition Category_functor' (D C : Category) : Category :=
+  Category_functor D C

  namespace ops
-    infixr `^c2`:35 := Category_functor_of_precategory
+    infixr `^c2`:35 := Category_functor
  end ops


--- a/hott/algebra/category/default.hlean
+++ b/hott/algebra/category/default.hlean
@ -0,0 +1,9 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.category.default
+Authors: Floris van Doorn
+-/
+
+import .category .strict .groupoid .constructions
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@ -230,11 +230,11 @@ namespace iso
  epi.mk
    (λ c g h H,
      calc
-        g = g ∘ id                 : by rewrite id_right
-      ... = g ∘ f ∘ section_of f   : by rewrite -comp_section
-      ... = h ∘ f ∘ section_of f   : by rewrite [assoc, H, -assoc]
-      ... = h ∘ id                 : by rewrite comp_section
-      ... = h                      : by rewrite id_right)
+        g = g ∘ id               : by rewrite id_right
+      ... = g ∘ f ∘ section_of f : by rewrite -comp_section
+      ... = h ∘ f ∘ section_of f : by rewrite [assoc, H, -assoc]
+      ... = h ∘ id               : by rewrite comp_section
+      ... = h                    : by rewrite id_right)

  definition mono_comp [instance] (g : b ⟶ c) (f : a ⟶ b) [Hf : mono f] [Hg : mono g]
    : mono (g ∘ f) :=
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@ -93,12 +93,16 @@ namespace nat_trans
        ... = F (η b ∘ G f)             : by rewrite (naturality η f)
        ... = F (η b) ∘ F (G f)         : by rewrite respect_comp)

-  infixr `∘nf`:60 := nat_trans_functor_compose
-  infixr `∘fn`:60 := functor_nat_trans_compose
+  infixr `∘nf`:62 := nat_trans_functor_compose
+  infixr `∘fn`:62 := functor_nat_trans_compose

-  definition functor_nat_trans_compose_commute (η : F ⟹ G) (θ : F' ⟹ G')
+  definition nf_fn_eq_fn_nf_pt (η : F ⟹ G) (θ : F' ⟹ G') (c : C)
+    : (θ (G c)) ∘ (F' (η c)) = (G' (η c)) ∘ (θ (F c)) :=
+  (naturality θ (η c))⁻¹
+
+  definition nf_fn_eq_fn_nf (η : F ⟹ G) (θ : F' ⟹ G')
    : (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) :=
-  nat_trans_eq (λc, (naturality θ (η c))⁻¹)
+  nat_trans_eq (λc, !nf_fn_eq_fn_nf_pt)

  definition fn_n_distrib (F' : D ⇒ E) (η : G ⟹ H) (θ : F ⟹ G)
    : F' ∘fn (η ∘n θ) = (F' ∘fn η) ∘n (F' ∘fn θ) :=
--- a/hott/arity.hlean
+++ b/hott/arity.hlean
@ -14,6 +14,7 @@ variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y}
          {b : B a} {b' : B a'}
          {c : C a b} {c' : C a' b'}
          {d : D a b c} {d' : D a' b' c'}
+          {e : E a b c d} {e' : E a' b' c' d'}

 namespace eq
  /-
@ -49,48 +50,54 @@ namespace eq
  notation f `∼3`:50 g := homotopy3 f g

  definition ap011 (f : U → V → W) (Hu : u = u') (Hv : v = v') : f u v = f u' v' :=
-  eq.rec_on Hu (ap (f u) Hv)
+  by cases Hu; exact (ap (f u) Hv)

  definition ap0111 (f : U → V → W → X) (Hu : u = u') (Hv : v = v') (Hw : w = w')
      : f u v w = f u' v' w' :=
-  eq.rec_on Hu (ap011 (f u) Hv Hw)
+  by cases Hu; exact (ap011 (f u) Hv Hw)

  definition ap01111 (f : U → V → W → X → Y) (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x')
      : f u v w x = f u' v' w' x' :=
-  eq.rec_on Hu (ap0111 (f u) Hv Hw Hx)
+  by cases Hu; exact (ap0111 (f u) Hv Hw Hx)

  definition ap011111 (f : U → V → W → X → Y → Z)
    (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') (Hy : y = y')
      : f u v w x y = f u' v' w' x' y' :=
-  eq.rec_on Hu (ap01111 (f u) Hv Hw Hx Hy)
+  by cases Hu; exact (ap01111 (f u) Hv Hw Hx Hy)

  definition ap0111111 (f : U → V → W → X → Y → Z → A)
    (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x') (Hy : y = y') (Hz : z = z')
      : f u v w x y z = f u' v' w' x' y' z' :=
-  eq.rec_on Hu (ap011111 (f u) Hv Hw Hx Hy Hz)
+  by cases Hu; exact (ap011111 (f u) Hv Hw Hx Hy Hz)

  definition ap010 (f : X → Πa, B a) (Hx : x = x') : f x ∼ f x' :=
-  λa, eq.rec_on Hx idp
+  λa, by cases Hx; exact idp

  definition ap0100 (f : X → Πa b, C a b) (Hx : x = x') : f x ∼2 f x' :=
-  λa b, eq.rec_on Hx idp
+  λa b, by cases Hx; exact idp

  definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ∼3 f x' :=
-  λa b c, eq.rec_on Hx idp
+  λa b c, by cases Hx; exact idp

  definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
      : f a b = f a' b' :=
-  eq.rec_on Hb (eq.rec_on Ha idp)
+  by cases Ha; cases Hb; exact idp

  definition apd0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
    (Hc : apd011 C Ha Hb ▹ c = c')
      : f a b c = f a' b' c' :=
-  eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp))
+  by cases Ha; cases Hb; cases Hc; exact idp

  definition apd01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
    (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d')
      : f a b c d = f a' b' c' d' :=
-  eq.rec_on Hd (eq.rec_on Hc (eq.rec_on Hb (eq.rec_on Ha idp)))
+  by cases Ha; cases Hb; cases Hc; cases Hd; exact idp
+
+  definition apd011111 (f : Πa b c d, E a b c d → Z) (Ha : a = a') (Hb : (Ha ▹ b) = b')
+    (Hc : apd011 C Ha Hb ▹ c = c') (Hd : apd0111 D Ha Hb Hc ▹ d = d')
+    (He : apd01111 E Ha Hb Hc Hd ▹ e = e')
+    : f a b c d e = f a' b' c' d' e' :=
+  by cases Ha; cases Hb; cases Hc; cases Hd; cases He; exact idp

  definition apd100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g :=
  λa b, apd10 (apd10 p a) b
--- a/hott/hit/circle.hlean
+++ b/hott/hit/circle.hlean
@ -91,10 +91,13 @@ namespace circle
    eq_inv_tr_of_tr_eq (tr_eq_of_eq_inv_tr q) = q :=
  by cases p; exact idp

+  definition con_refl {A : Type} {x y : A} (p : x = y) : p ⬝ refl _ = p :=
+  eq.rec_on p idp
+
  theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) :
    apd (rec Pbase Ploop) loop = Ploop :=
  begin
-    rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2],
+    rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap], --con_idp should work here
    apply concat, apply (ap (λx, x ⬝ _)), apply con_idp, esimp,
    rewrite [rec_loop_helper,inv_con_inv_left],
    apply con_inv_cancel_left
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@ -31,4 +31,106 @@ namespace trunc
    because the universe is generally not a set
  -/

+  --export is_trunc
+
+  variables {X Y Z : Type} {P : X → Type} (A B : Type) (n : trunc_index)
+
+  local attribute is_trunc_eq [instance]
+
+  definition is_equiv_tr [instance] [H : is_trunc n A] : is_equiv (@tr n A) :=
+  adjointify _
+             (trunc.rec id)
+             (λaa, trunc.rec_on aa (λa, idp))
+             (λa, idp)
+
+  definition equiv_trunc [H : is_trunc n A] : A ≃ trunc n A :=
+  equiv.mk tr _
+
+  definition is_trunc_of_is_equiv_tr [H : is_equiv (@tr n A)] : is_trunc n A :=
+  is_trunc_is_equiv_closed n tr⁻¹
+
+  definition untrunc_of_is_trunc [reducible] [H : is_trunc n A] : trunc n A → A :=
+  tr⁻¹
+
+  /- Functoriality -/
+  definition trunc_functor (f : X → Y) : trunc n X → trunc n Y :=
+  λxx, trunc.rec_on xx (λx, tr (f x))
+--  by intro xx; apply (trunc.rec_on xx); intro x; exact (tr (f x))
+--  by intro xx; fapply (trunc.rec_on xx); intro x; exact (tr (f x))
+--  by intro xx; exact (trunc.rec_on xx (λx, (tr (f x))))
+
+  definition trunc_functor_compose (f : X → Y) (g : Y → Z)
+    : trunc_functor n (g ∘ f) ∼ trunc_functor n g ∘ trunc_functor n f :=
+  λxx, trunc.rec_on xx (λx, idp)
+
+  definition trunc_functor_id : trunc_functor n (@id A) ∼ id :=
+  λxx, trunc.rec_on xx (λx, idp)
+
+  definition is_equiv_trunc_functor (f : X → Y) [H : is_equiv f] : is_equiv (trunc_functor n f) :=
+  adjointify _
+             (trunc_functor n f⁻¹)
+             (λyy, trunc.rec_on yy (λy, ap tr !right_inv))
+             (λxx, trunc.rec_on xx (λx, ap tr !left_inv))
+
+  section
+  open prod.ops
+  definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
+  sorry
+  -- equiv.MK (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))
+  --          (λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, tr (x,y))))
+  --          sorry --(λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, idp)))
+  --          (λpp, trunc.rec_on pp (λp, prod.rec_on p (λx y, idp)))
+
+  -- begin
+  --   fapply equiv.MK,
+  --     apply sorry, --{exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))},
+  --     apply sorry, /-{intro p, cases p with (xx, yy),
+  --       apply (trunc.rec_on xx), intro x,
+  --       apply (trunc.rec_on yy), intro y, exact (tr (x,y))},-/
+  --     apply sorry, /-{intro p, cases p with (xx, yy),
+  --       apply (trunc.rec_on xx), intro x,
+  --       apply (trunc.rec_on yy), intro y, apply idp},-/
+  --     apply sorry --{intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp},
+  -- end
+  end
+
+  /- Propositional truncation -/
+
+  -- should this live in hprop?
+  definition merely [reducible] (A : Type) : Type := trunc -1 A
+
+  notation `||`:max A `||`:0 := merely A
+  notation `∥`:max A `∥`:0   := merely A
+
+  definition Exists [reducible] (P : X → Type) : Type := ∥ sigma P ∥
+  definition or [reducible] (A B : Type) : Type := ∥ A ⊎ B ∥
+
+  notation `exists` binders `,` r:(scoped P, Exists P) := r
+  notation `∃` binders `,` r:(scoped P, Exists P) := r
+  notation A `\/` B := or A B
+  notation A ∨ B    := or A B
+
+  definition merely.intro   [reducible] (a : A) : ∥ A ∥                            := tr a
+  definition exists.intro   [reducible] (x : X) (p : P x) : ∃x, P x                := tr ⟨x, p⟩
+  definition or.intro_left  [reducible] (x : X) : X ∨ Y                            := tr (inl x)
+  definition or.intro_right [reducible] (y : Y) : X ∨ Y                            := tr (inr y)
+
+  definition is_contr_of_merely_hprop [H : is_hprop A] (aa : merely A) : is_contr A :=
+  is_contr_of_inhabited_hprop (trunc.rec_on aa id)
+
+  section
+  open sigma.ops
+  definition trunc_sigma_equiv : trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) :=
+  equiv.MK (λpp, trunc.rec_on pp (λp, tr ⟨p.1, tr p.2⟩))
+           (λpp, trunc.rec_on pp (λp, trunc.rec_on p.2 (λb, tr ⟨p.1, b⟩)))
+           (λpp, trunc.rec_on pp (λp, sigma.rec_on p (λa bb, trunc.rec_on bb (λb, by esimp))))
+           (λpp, trunc.rec_on pp (λp, sigma.rec_on p (λa b, by esimp)))
+
+  definition trunc_sigma_equiv_of_is_trunc [H : is_trunc n X]
+    : trunc n (Σ x, P x) ≃ Σ x, trunc n (P x) :=
+  calc
+    trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) : trunc_sigma_equiv
+      ... ≃ Σ x, trunc n (P x) : equiv.symm !equiv_trunc
+  end
+
 end trunc
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@ -218,7 +218,6 @@ namespace is_equiv
  definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) :=
    is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr p) (inv_tr_tr p) (tr_inv_tr_lemma p)

-
 end is_equiv

 open is_equiv
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@ -50,8 +50,6 @@ infixr  ∘'                 := dcompose
 infixl  on                 := on_fun
 infixr  $                  := app
 notation f `-[` op `]-` g  := combine f op g
-- Trick for using any binary function as infix operator
-notation a `⟨` f `⟩` b     :=  f a b

 end function

--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@ -127,7 +127,7 @@ namespace is_trunc
    A H
  --in the proof the type of H is given explicitly to make it available for class inference

-  definition is_trunc_of_leq (A : Type) (n m : trunc_index) (Hnm : n ≤ m)
+  definition is_trunc_of_leq.{l} (A : Type.{l}) {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
@ -149,11 +149,11 @@ namespace is_trunc

  definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
      : is_trunc (n.+1) A :=
-  is_trunc_of_leq A -1 (n.+1) star
+  is_trunc_of_leq A star

  definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
      : is_trunc (n.+2) A :=
-  is_trunc_of_leq A nat.zero (n.+2) star
+  is_trunc_of_leq A star

  /- hprops -/

@ -204,8 +204,12 @@ namespace is_trunc
  abbreviation hprop := -1-Type
  abbreviation hset := 0-Type

-  protected definition hprop.mk := @trunctype.mk -1
-  protected definition hset.mk := @trunctype.mk (-1.+1)
+  protected abbreviation hprop.mk := @trunctype.mk -1
+  protected abbreviation hset.mk := @trunctype.mk (-1.+1)
+
+  protected abbreviation trunctype.mk' [parsing-only] (n : trunc_index) (A : Type)
+    [H : is_trunc n A] : n-Type :=
+  trunctype.mk A H

  /- interaction with equivalences -/

@ -234,10 +238,18 @@ namespace is_trunc
      IH (f⁻¹ x = f⁻¹ y) _ (x = y) (ap f⁻¹)⁻¹ !is_equiv_inv))
    A HA B f H

+  definition is_trunc_is_equiv_closed_rev (n : trunc_index) (f : A → B) [H : is_equiv f]
+    [HA : is_trunc n B] : is_trunc n A :=
+  is_trunc_is_equiv_closed n f⁻¹
+
  definition is_trunc_equiv_closed (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A]
    : is_trunc n B :=
  is_trunc_is_equiv_closed n (to_fun f)

+  definition is_trunc_equiv_closed_rev (n : trunc_index) (f : A ≃ B) [HA : is_trunc n B]
+    : is_trunc n A :=
+  is_trunc_is_equiv_closed n (to_inv f)
+
  definition is_equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
    : is_equiv f :=
  is_equiv.mk f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim)
--- a/hott/types/default.hlean
+++ b/hott/types/default.hlean
@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.

 Module: types.default
 Authors: Floris van Doorn
-
-The core of the HoTT library
 -/

 import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@ -9,53 +9,47 @@ Ported from Coq HoTT
 Theorems about the types equiv and is_equiv
 -/

-import types.fiber types.arrow arity
+import .fiber .arrow arity .hprop_trunc

-open eq is_trunc sigma sigma.ops arrow pi
+open eq is_trunc sigma sigma.ops arrow pi fiber function equiv

 namespace is_equiv
-  open equiv function
-  section
-    open fiber
-    variables {A B : Type} (f : A → B) [H : is_equiv f]
-    include H
-    definition is_contr_fiber_of_is_equiv (b : B) : is_contr (fiber f b) :=
-    is_contr.mk
-      (fiber.mk (f⁻¹ b) (right_inv f b))
-      (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc
-        right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left
-             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p)       : by rewrite ap_con_eq_con
-             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p)    : by rewrite adj
-             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p      : by rewrite con.assoc
-             ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p     : by rewrite ap_compose
-             ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p       : by rewrite ap_inv
-             ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p            : by rewrite ap_con)))
-
-    definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) :=
-    begin
-      fapply is_trunc_equiv_closed,
-        {apply sigma_equiv_sigma_id, intro g, apply eq_equiv_homotopy},
-      fapply is_trunc_equiv_closed,
-        {apply fiber.sigma_char},
-      fapply is_contr_fiber_of_is_equiv,
-      apply (to_is_equiv (arrow_equiv_arrow_right (equiv.mk f H))),
-    end
-
-    definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ∼ id)
-      : is_contr (Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
-    begin
-      fapply is_trunc_equiv_closed,
-        {apply equiv.symm, apply sigma_pi_equiv_pi_sigma},
-      fapply is_trunc_equiv_closed,
-        {apply pi_equiv_pi_id, intro a,
-          apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp))},
-      fapply is_trunc_pi,
-      intro a, fapply @is_contr_eq,
-      apply is_contr_fiber_of_is_equiv
-    end
+  variables {A B : Type} (f : A → B) [H : is_equiv f]
+  include H
+  /- is_equiv f is a mere proposition -/
+  definition is_contr_fiber_of_is_equiv [instance] (b : B) : is_contr (fiber f b) :=
+  is_contr.mk
+    (fiber.mk (f⁻¹ b) (right_inv f b))
+    (λz, fiber.rec_on z (λa p, fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc
+      right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left
+           ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p)       : by rewrite ap_con_eq_con
+           ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p)    : by rewrite adj
+           ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p      : by rewrite con.assoc
+           ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p     : by rewrite ap_compose
+           ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p       : by rewrite ap_inv
+           ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p            : by rewrite ap_con)))

+  definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) :=
+  begin
+    fapply is_trunc_equiv_closed,
+      {apply sigma_equiv_sigma_id, intro g, apply eq_equiv_homotopy},
+    fapply is_trunc_equiv_closed,
+      {apply fiber.sigma_char},
+    fapply is_contr_fiber_of_is_equiv,
+    apply (to_is_equiv (arrow_equiv_arrow_right (equiv.mk f H))),
  end
-  variables {A B : Type} (f : A → B)
+
+  definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ∼ id)
+    : is_contr (Σ(η : u.1 ∘ f ∼ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
+  begin
+    fapply is_trunc_equiv_closed,
+      {apply equiv.symm, apply sigma_pi_equiv_pi_sigma},
+    fapply is_trunc_equiv_closed,
+      {apply pi_equiv_pi_id, intro a,
+        apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp))},
+  end
+
+  omit H

  protected definition sigma_char : (is_equiv f) ≃
  (Σ(g : B → A) (ε : f ∘ g ∼ id) (η : g ∘ f ∼ id), Π(a : A), ε (f a) = ap f (η a)) :=
@ -80,21 +74,32 @@ namespace is_equiv

  local attribute is_contr_right_inverse [instance] [priority 1600]
  local attribute is_contr_right_coherence [instance] [priority 1600]
+
  theorem is_hprop_is_equiv [instance] : is_hprop (is_equiv f) :=
  is_hprop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !sigma_char'))

-  /- contractible fibers -/ -- TODO: uncomment this (needs to import instance is_hprop_is_trunc)
-  -- definition is_contr_fun [reducible] {A B : Type} (f : A → B) := Π(b : B), is_contr (fiber f b)
+  /- contractible fibers -/
+  definition is_contr_fun [reducible] (f : A → B) := Π(b : B), is_contr (fiber f b)

-  -- definition is_hprop_is_contr_fun (f : A → B) : is_hprop (is_contr_fun f) := _
+  definition is_contr_fun_of_is_equiv [H : is_equiv f] : is_contr_fun f :=
+  is_contr_fiber_of_is_equiv f

-  -- definition is_equiv_of_is_contr_fun [instance] [H : is_contr_fun f] : is_equiv f :=
-  -- adjointify _ (λb, point (center (fiber f b)))
-  --              (λb, point_eq (center (fiber f b)))
-  --              (λa, ap point (contr (fiber.mk a idp)))
+  definition is_hprop_is_contr_fun (f : A → B) : is_hprop (is_contr_fun f) := _

-  -- definition is_equiv_of_imp_is_equiv (H : B → is_equiv f) : is_equiv f :=
-  -- @is_equiv_of_is_contr_fun _ _ f (is_contr_fun.mk (λb, @is_contr_fiber_of_is_equiv _ _ _ (H b) _))
+  /-
+    we cannot make the next theorem an instance, because it loops together with
+    is_contr_fiber_of_is_equiv
+  -/
+  definition is_equiv_of_is_contr_fun [H : is_contr_fun f] : is_equiv f :=
+  adjointify _ (λb, point (center (fiber f b)))
+               (λb, point_eq (center (fiber f b)))
+               (λa, ap point (center_eq (fiber.mk a idp)))
+
+  definition is_equiv_of_imp_is_equiv (H : B → is_equiv f) : is_equiv f :=
+  @is_equiv_of_is_contr_fun _ _ f (λb, @is_contr_fiber_of_is_equiv _ _ _ (H b) _)
+
+  definition is_equiv_equiv_is_contr_fun : is_equiv f ≃ is_contr_fun f :=
+  equiv_of_is_hprop _ (λH, !is_equiv_of_is_contr_fun)

 end is_equiv

@ -108,4 +113,32 @@ namespace equiv

  definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' :=
  by (cases f; cases f'; apply (equiv_mk_eq p))
+
+  protected definition equiv.sigma_char (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f :=
+  begin
+    fapply equiv.MK,
+      {intro F, exact ⟨to_fun F, to_is_equiv F⟩},
+      {intro p, cases p with [f, H], exact (equiv.mk f H)},
+      {intro p, cases p with [f, H], exact idp},
+      {intro F, cases F with [f, H], exact idp},
+  end
+
+  definition equiv_eq_char (f f' : A ≃ B) : (f = f') ≃ (to_fun f = to_fun f') :=
+  calc
+    (f = f') ≃ (to_fun !equiv.sigma_char f = to_fun !equiv.sigma_char f')
+                : eq_equiv_fn_eq (to_fun !equiv.sigma_char)
+         ... ≃ ((to_fun !equiv.sigma_char f).1 = (to_fun !equiv.sigma_char f').1 ) : equiv_subtype
+         ... ≃ (to_fun f = to_fun f') : equiv.refl
+
+  definition is_equiv_ap_to_fun (f f' : A ≃ B)
+    : is_equiv (ap to_fun : f = f' → to_fun f = to_fun f') :=
+  begin
+    fapply adjointify,
+      {intro p, cases f with [f, H], cases f' with [f', H'], cases p, apply (ap (mk f')), apply is_hprop.elim},
+      {intro p, cases f with [f, H], cases f' with [f', H'], cases p,
+        apply (@concat _ _ (ap to_fun (ap (equiv.mk f') (is_hprop.elim H H')))), {apply idp},
+        generalize (is_hprop.elim H H'), intro q, cases q, apply idp},
+      {intro p, cases p, cases f with [f, H], apply (ap (ap (equiv.mk f))), apply is_hset.elim}
+  end
+
 end equiv
--- a/hott/types/function.hlean
+++ b/hott/types/function.hlean
@ -0,0 +1,98 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: types.function
+Author: Floris van Doorn
+
+Ported from Coq HoTT
+Theorems about embeddings and surjections
+-/
+
+import hit.trunc .pi .fiber .equiv
+
+open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod
+
+variables {A B : Type} {f : A → B} {b : B}
+
+structure is_embedding [class] (f : A → B) :=
+(elim : Π(a a' : A), is_equiv (@ap A B f a a'))
+
+structure is_surjective [class] (f : A → B) :=
+(elim : Π(b : B), ∥ fiber f b ∥)
+
+structure is_split_surjective [class] (f : A → B) :=
+(elim : Π(b : B), fiber f b)
+
+structure is_retraction [class] (f : A → B) :=
+  (sect : B → A)
+  (right_inverse : Π(b : B), f (sect b) = b)
+
+namespace function
+
+  attribute is_embedding.elim [instance]
+
+  definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P]
+    (IH : fiber f b → P) : P :=
+  trunc.rec_on (is_surjective.elim f b) IH
+
+  definition is_surjective_of_is_split_surjective [instance] [H : is_split_surjective f]
+    : is_surjective f :=
+  is_surjective.mk (λb, tr (is_split_surjective.elim f b))
+
+  definition is_injective_of_is_embedding [reducible] [H : is_embedding f] {a a' : A}
+    : f a = f a' → a = a' :=
+  (ap f)⁻¹
+
+  definition is_embedding_of_is_injective [HA : is_hset A] [HB : is_hset B]
+    (H : Π(a a' : A), f a = f a' → a = a') : is_embedding f :=
+  begin
+  fapply is_embedding.mk,
+  intros [a, a'],
+  fapply adjointify,
+    {exact (H a a')},
+    {intro p, apply is_hset.elim},
+    {intro p, apply is_hset.elim}
+  end
+
+  definition is_hprop_is_embedding [instance] (f : A → B) : is_hprop (is_embedding f) :=
+  begin
+    have H : (Π(a a' : A), is_equiv (@ap A B f a a')) ≃ is_embedding f,
+    begin
+      fapply equiv.MK,
+        {exact is_embedding.mk},
+        {intro h, cases h, exact elim},
+        {intro h, cases h, apply idp},
+        {intro p, apply idp},
+    end,
+    apply is_trunc_equiv_closed,
+    exact H,
+  end
+
+  definition is_hprop_is_surjective [instance] (f : A → B) : is_hprop (is_surjective f) :=
+  begin
+    have H : (Π(b : B), merely (fiber f b)) ≃ is_surjective f,
+    begin
+      fapply equiv.MK,
+        {exact is_surjective.mk},
+        {intro h, cases h, exact elim},
+        {intro h, cases h, apply idp},
+        {intro p, apply idp},
+    end,
+    apply is_trunc_equiv_closed,
+    exact H,
+  end
+
+  definition is_embedding_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_embedding f :=
+  is_embedding.mk _
+
+  definition is_equiv_of_is_surjective_of_is_embedding (f : A → B)
+    [H : is_embedding f] [H' : is_surjective f] : is_equiv f :=
+  @is_equiv_of_is_contr_fun _ _ _
+    (λb, is_surjective_rec_on H' b
+      (λa, is_contr.mk a
+        (λa',
+          fiber_eq ((ap f)⁻¹ ((point_eq a) ⬝ (point_eq a')⁻¹))
+                   (by rewrite (right_inv (ap f)); rewrite inv_con_cancel_right))))
+
+end function
--- a/hott/types/hprop_trunc.hlean
+++ b/hott/types/hprop_trunc.hlean
@ -0,0 +1,63 @@
+/-
+Copyright (c) 2015 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: types.hprop_trunc
+Authors: Jakob von Raumer, Floris van Doorn
+
+Proof of the theorem that (is_trunc n A) is a mere proposition
+We prove this here to avoid circular dependency of files
+We want to use this in .equiv; .equiv is imported by .function and .function is imported by .trunc
+-/
+
+import .pi
+
+open equiv sigma sigma.ops eq function pi
+
+namespace is_trunc
+  definition is_contr.sigma_char (A : Type) :
+    (Σ (center : A), Π (a : A), center = a) ≃ (is_contr A) :=
+  begin
+    fapply equiv.MK,
+    { intro S, exact (is_contr.mk S.1 S.2)},
+    { intro H, cases H with [H'], cases H' with [ce, co], exact ⟨ce, co⟩},
+    { intro H, cases H with [H'], cases H' with [ce, co], exact idp},
+    { intro S, cases S, apply idp}
+  end
+
+  definition is_trunc.pi_char (n : trunc_index) (A : Type) :
+    (Π (x y : A), is_trunc n (x = y)) ≃ (is_trunc (n .+1) A) :=
+  begin
+    fapply equiv.MK,
+    { intro H, apply is_trunc_succ_intro},
+    { intros [H, x, y], apply is_trunc_eq},
+    { intro H, cases H, apply idp},
+    { intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b,
+      esimp [function.id,compose,is_trunc_succ_intro,is_trunc_eq],
+      generalize (P a b), intro H, cases H, apply idp},
+  end
+
+  definition is_hprop_is_trunc [instance] (n : trunc_index) :
+    Π (A : Type), is_hprop (is_trunc n A) :=
+  begin
+    apply (trunc_index.rec_on n),
+    { intro A,
+      apply is_trunc_is_equiv_closed,
+      { apply equiv.to_is_equiv, apply is_contr.sigma_char},
+      apply (@is_hprop.mk), intros,
+      fapply sigma_eq, {apply x.2},
+      apply (@is_hprop.elim),
+      apply is_trunc_pi, intro a,
+      apply is_hprop.mk, intros [w, z],
+      have H : is_hset A,
+      begin
+        apply is_trunc_succ, apply is_trunc_succ,
+        apply is_contr.mk, exact y.2
+      end,
+      fapply (@is_hset.elim A _ _ _ w z)},
+    { intros [n', IH, A],
+      apply is_trunc_is_equiv_closed,
+      apply equiv.to_is_equiv,
+      apply is_trunc.pi_char},
+  end
+end is_trunc
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@ -3,75 +3,99 @@ Copyright (c) 2015 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.

 Module: types.trunc
-Authors: Jakob von Raumer, Floris van Doorn
+Authors: Floris van Doorn

-Properties of is_trunc
+Properties of is_trunc and trunctype
 -/

-import types.pi types.eq
+--NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .hprop_trunc
+
+import types.pi types.eq types.equiv .function
+
+open eq sigma sigma.ops pi function equiv is_trunc.trunctype is_equiv prod

-open sigma sigma.ops pi function eq equiv eq funext
 namespace is_trunc
+  variables {A B : Type} {n : trunc_index}

-  definition is_contr.sigma_char (A : Type) :
-    (Σ (center : A), Π (a : A), center = a) ≃ (is_contr A) :=
-  begin
-    fapply equiv.mk,
-     {intro S, apply is_contr.mk, exact S.2},
-     {fapply is_equiv.adjointify,
-       {intro H, apply sigma.mk, exact (@center_eq A H)},
-       {intro H, apply (is_trunc.rec_on H), intro Hint,
-        apply (contr_internal.rec_on Hint), intros [H1, H2],
-        apply idp},
-       {intro S, cases S, apply idp}}
-  end
-
-  definition is_trunc.pi_char (n : trunc_index) (A : Type) :
-    (Π (x y : A), is_trunc n (x = y)) ≃ (is_trunc (n .+1) A) :=
-  begin
-    fapply equiv.MK,
-      {intro H, apply is_trunc_succ_intro},
-      {intros [H, x, y], apply is_trunc_eq},
-      {intro H, apply (is_trunc.rec_on H), intro Hint, apply idp},
-      {intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b,
-    esimp [function.id,compose,is_trunc_succ_intro,is_trunc_eq],
-    generalize (P a b), intro H, apply (is_trunc.rec_on H), intro H', apply idp},
-  end
-
-  definition is_hprop_is_trunc [instance] (n : trunc_index) :
-    Π (A : Type), is_hprop (is_trunc n A) :=
-  begin
-    apply (trunc_index.rec_on n),
-      {intro A,
-       apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv,
-       apply is_contr.sigma_char,
-       apply (@is_hprop.mk), intros,
-       fapply sigma_eq, apply x.2,
-       apply (@is_hprop.elim),
-       apply is_trunc_pi, intro a,
-       apply is_hprop.mk, intros [w, z],
-       have H : is_hset A,
-       begin
-         apply is_trunc_succ, apply is_trunc_succ,
-         apply is_contr.mk, exact y.2
-       end,
-       fapply (@is_hset.elim A _ _ _ w z)},
-     {intros [n', IH, A],
-      apply is_trunc_is_equiv_closed,
-        apply equiv.to_is_equiv,
-        apply is_trunc.pi_char},
-  end
-
-  definition is_trunc_succ_of_imp_is_trunc_succ {A : Type} {n : trunc_index} (H : A → is_trunc (n.+1) A)
-      : is_trunc (n.+1) A :=
+  definition is_trunc_succ_of_imp_is_trunc_succ (H : A → is_trunc (n.+1) A) : is_trunc (n.+1) A :=
  @is_trunc_succ_intro _ _ (λx y, @is_trunc_eq _ _ (H x) x y)

-  definition is_trunc_of_imp_is_trunc_of_leq {A : Type} {n : trunc_index} (Hn : -1 ≤ n)
-      (H : A → is_trunc n A) : is_trunc n A :=
+  definition is_trunc_of_imp_is_trunc_of_leq (Hn : -1 ≤ n) (H : A → is_trunc n A) : is_trunc n A :=
  trunc_index.rec_on n (λHn H, empty.rec _ Hn)
                       (λn IH Hn, is_trunc_succ_of_imp_is_trunc_succ)
                       Hn H

+  /- theorems about trunctype -/
+  protected definition trunctype.sigma_char.{l} (n : trunc_index) :
+    (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
+  begin
+    fapply equiv.MK,
+    { intro A, exact (⟨carrier A, struct A⟩)},
+    { intro S, exact (trunctype.mk S.1 S.2)},
+    { intro S, apply (sigma.rec_on S), intros [S1, S2], apply idp},
+    { intro A, apply (trunctype.rec_on A), intros [A1, A2], apply idp},
+  end
+
+  definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) :
+    (A = B) ≃ (carrier A = carrier B) :=
+  calc
+    (A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B)
+              : eq_equiv_fn_eq_of_equiv
+      ... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1)
+             : equiv.symm (!equiv_subtype)
+      ... ≃ (carrier A = carrier B) : equiv.refl
+
+  definition is_trunc_is_embedding_closed (f : A → B) [Hf : is_embedding f] [HB : is_trunc n B]
+    (Hn : -1 ≤ n) : is_trunc n A :=
+  begin
+    cases n with [n],
+      {exact (!empty.elim Hn)},
+      {apply is_trunc_succ_intro, intros [a, a'],
+         fapply (@is_trunc_is_equiv_closed_rev _ _ n (ap f))}
+  end
+
+  definition is_trunc_is_retraction_closed (f : A → B) [Hf : is_retraction f]
+    (n : trunc_index) [HA : is_trunc n A] : is_trunc n B :=
+  begin
+    reverts [A, B, f, Hf, HA],
+    apply (trunc_index.rec_on n),
+    { clear n, intros [A, B, f, Hf, HA], cases Hf with [g, ε], fapply is_contr.mk,
+      { exact (f (center A))},
+      { intro b, apply concat,
+        { apply (ap f), exact (center_eq (g b))},
+        { apply ε}}},
+    { clear n, intros [n, IH, A, B, f, Hf, HA], cases Hf with [g, ε],
+      apply is_trunc_succ_intro, intros [b, b'],
+      fapply (IH (g b = g b')),
+      { intro q, exact ((ε b)⁻¹ ⬝ ap f q ⬝ ε b')},
+      { apply (is_retraction.mk (ap g)),
+        { intro p, cases p, {rewrite [↑ap, con_idp, con.left_inv]}}},
+      { apply is_trunc_eq}}
+  end
+
+  definition is_embedding_to_fun (A B : Type) : is_embedding (@to_fun A B)  :=
+  is_embedding.mk (λf f', !is_equiv_ap_to_fun)
+
+  definition is_trunc_trunctype [instance] (n : trunc_index) : is_trunc n.+1 (n-Type) :=
+  begin
+    apply is_trunc_succ_intro, intros [X, Y],
+    fapply is_trunc_equiv_closed,
+      {apply equiv.symm, apply trunctype_eq_equiv},
+    fapply is_trunc_equiv_closed,
+      {apply equiv.symm, apply eq_equiv_equiv},
+    cases n,
+      {apply @is_contr_of_inhabited_hprop,
+        {apply is_trunc_is_embedding_closed,
+          {apply is_embedding_to_fun} ,
+          {exact unit.star}},
+        {apply equiv_of_is_contr_of_is_contr}},
+      {apply is_trunc_is_embedding_closed,
+        {apply is_embedding_to_fun},
+        {exact unit.star}}
+  end
+
+
+  /- theorems about decidable equality and axiom K -/
  definition is_hset_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_hset A :=
  is_hset.mk _ (λa b p q, eq.rec_on q K p)

@ -116,24 +140,62 @@ namespace is_trunc
    (K : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A :=
  @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_leq H (λp, eq.rec_on p !K))

-  open trunctype equiv equiv.ops
+end is_trunc open is_trunc

-  protected definition trunctype.sigma_char.{l} (n : trunc_index) :
-    (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
+namespace trunc
+  variable {A : Type}
+
+  definition trunc_eq_type (n : trunc_index) (aa aa' : trunc n.+1 A) : n-Type :=
+  trunc.rec_on aa (λa, trunc.rec_on aa' (λa', trunctype.mk' n (trunc n (a = a'))))
+
+  definition trunc_eq_equiv (n : trunc_index) (aa aa' : trunc n.+1 A)
+    : aa = aa' ≃ trunc_eq_type n aa aa' :=
  begin
    fapply equiv.MK,
-    /--/  intro A, exact (⟨carrier A, struct A⟩),
-    /--/  intro S, exact (trunctype.mk S.1 S.2),
-    /--/  intro S, apply (sigma.rec_on S), intros [S1, S2], apply idp,
-    intro A, apply (trunctype.rec_on A), intros [A1, A2], apply idp,
+    { intro p, cases p, apply (trunc.rec_on aa),
+      intro a, esimp [trunc_eq_type,trunc.rec_on], exact (tr idp)},
+    { apply (trunc.rec_on aa'), apply (trunc.rec_on aa),
+      intros [a, a', x], esimp [trunc_eq_type, trunc.rec_on] at x,
+      apply (trunc.rec_on x), intro p, exact (ap tr p)},
+    {
+      -- apply (trunc.rec_on aa'), apply (trunc.rec_on aa),
+      -- intros [a, a', x], esimp [trunc_eq_type, trunc.rec_on] at x,
+      -- apply (trunc.rec_on x), intro p,
+      -- cases p, esimp [trunc.rec_on,eq.cases_on,compose,id], -- apply idp --?
+      apply sorry},
+    { intro p, cases p, apply (trunc.rec_on aa), intro a, apply sorry},
  end

-  protected definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) :
-    (A = B) ≃ (carrier A = carrier B) :=
-  calc
-    (A = B) ≃ (trunctype.sigma_char n A = trunctype.sigma_char n B) : eq_equiv_fn_eq_of_equiv
-      ... ≃ ((trunctype.sigma_char n A).1 = (trunctype.sigma_char n B).1) : equiv.symm (!equiv_subtype)
-      ... ≃ (carrier A = carrier B) : equiv.refl
+  definition tr_eq_tr_equiv (n : trunc_index) (a a' : A)
+    : (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') :=
+  !trunc_eq_equiv

+  definition is_trunc_trunc_of_is_trunc [instance] [priority 500] (A : Type)
+    (n m : trunc_index) [H : is_trunc n A] : is_trunc n (trunc m A) :=
+  begin
+    reverts [A, m, H], apply (trunc_index.rec_on n),
+    { clear n, intros [A, m, H], apply is_contr_equiv_closed,
+      { apply equiv_trunc, apply (@is_trunc_of_leq _ -2), exact unit.star} },
+    { clear n, intros [n, IH, A, m, H], cases m with [m],
+      { apply (@is_trunc_of_leq _ -2), exact unit.star},
+      { apply is_trunc_succ_intro, intros [aa, aa'],
+        apply (@trunc.rec_on _ _ _ aa  (λy, !is_trunc_succ_of_is_hprop)),
+        apply (@trunc.rec_on _ _ _ aa' (λy, !is_trunc_succ_of_is_hprop)),
+        intros [a, a'], apply (is_trunc_equiv_closed_rev),
+        { apply tr_eq_tr_equiv},
+        { exact (IH _ _ _)}}}
+  end

-end is_trunc
+end trunc open trunc
+
+namespace function
+  variables {A B : Type}
+  definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f :=
+  is_surjective.mk (λb, !center)
+
+  definition is_equiv_equiv_is_embedding_times_is_surjective (f : A → B)
+    : is_equiv f ≃ (is_embedding f × is_surjective f) :=
+  equiv_of_is_hprop (λH, (_, _))
+                    (λP, prod.rec_on P (λH₁ H₂, !is_equiv_of_is_surjective_of_is_embedding))
+
+end function
--- a/hott/types/types.md
+++ b/hott/types/types.md
@ -3,13 +3,16 @@ hott.types

 Various datatypes.

+* [prod](prod.hlean)
+* [sigma](sigma.hlean)
 * [pi](pi.hlean)
 * [arrow](arrow.hlean)
 * [eq](eq.hlean)
-* [trunc](trunc.hlean)
-* [prod](prod.hlean)
-* [sigma](sigma.hlean)
 * [fiber](fiber.hlean)
+* [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [trunc](trunc.hlean) to avoid circularity in imports.
 * [equiv](equiv.hlean)
 * [pointed](pointed.hlean)
+
+* [trunc](trunc.hlean)
+
 * [W](W.hlean) (not loaded by default)