diff --git a/hott/hit/red_susp.hlean b/hott/hit/red_susp.hlean
new file mode 100644
index 000000000..c8cc7238f
--- /dev/null
+++ b/hott/hit/red_susp.hlean
@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+Declaration of the reduced suspension
+-/
+
+import .two_quotient types.pointed algebra.e_closure
+
+open simple_two_quotient eq unit pointed e_closure
+
+namespace red_susp
+section
+
+  parameter {A : Pointed}
+
+  inductive red_susp_R : unit → unit → Type :=
+  | Rmk : Π(a : A), red_susp_R star star
+  open red_susp_R
+  inductive red_susp_Q : Π⦃x : unit⦄, e_closure red_susp_R x x → Type :=
+  | Qmk : red_susp_Q [Rmk pt]
+  open red_susp_Q
+  local abbreviation R := red_susp_R
+  local abbreviation Q := red_susp_Q
+
+  definition red_susp : Type := simple_two_quotient R Q -- TODO: define this in root namespace
+
+  definition base : red_susp :=
+  incl0 R Q star
+
+  definition merid (a : A) : base = base :=
+  incl1 R Q (Rmk a)
+
+  definition merid_pt : merid pt = idp :=
+  incl2 R Q Qmk
+
+  -- protected definition rec {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
+  --   (Pe : Pm pt =[merid_pt] idpo) (x : red_susp) : P x :=
+  -- begin
+  --   induction x,
+  -- end
+
+  -- protected definition rec_on [reducible] {P : red_susp → Type} (x : red_susp) (Pb : P base)
+  --   (Pm : Π(a : A), Pb =[merid a] Pb) (Pe : Pm pt =[merid_pt] idpo) : P x :=
+  -- rec Pb Pm Pe x
+
+  -- definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
+  --   (Pe : Pm pt =[merid_pt] idpo) (a : A)
+  --   : apdo (rec Pb Pm Pe) (merid a) = Pm a :=
+  -- !rec_incl1
+
+  -- theorem elim_merid_pt {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
+  --   (Pe : Pm pt =[merid_pt] idpo)
+  --   : square (ap02 (rec Pb Pm Pe) merid_pt) Pe (rec_merid Pe pt) idp :=
+  -- !rec_incl2
+
+  protected definition elim {P : Type} (Pb : P) (Pm : Π(a : A), Pb = Pb)
+    (Pe : Pm pt = idp) (x : red_susp) : P :=
+  begin
+    induction x,
+      exact Pb,
+      induction s, exact Pm a,
+      induction q, exact Pe
+  end
+
+  protected definition elim_on [reducible] {P : Type} (x : red_susp) (Pb : P)
+    (Pm : Π(a : A), Pb = Pb) (Pe : Pm pt = idp) : P :=
+  elim Pb Pm Pe x
+
+  definition elim_merid {P : Type} {Pb : P} {Pm : Π(a : A), Pb = Pb}
+    (Pe : Pm pt = idp) (a : A)
+    : ap (elim Pb Pm Pe) (merid a) = Pm a :=
+  !elim_incl1
+
+  theorem elim_merid_pt {P : Type} (Pb : P) (Pm : Π(a : A), Pb = Pb)
+    (Pe : Pm pt = idp) : square (ap02 (elim Pb Pm Pe) merid_pt) Pe (elim_merid Pe pt) idp :=
+  !elim_incl2
+
+end
+end red_susp
+
+attribute red_susp.base [constructor]
+attribute /-red_susp.rec-/ red_susp.elim [unfold-c 6] [recursor 6]
+--attribute red_susp.elim_type [unfold-c 9]
+attribute /-red_susp.rec_on-/ red_susp.elim_on [unfold-c 3]
+--attribute red_susp.elim_type_on [unfold-c 6]
diff --git a/hott/hit/refl_quotient.hlean b/hott/hit/refl_quotient.hlean
new file mode 100644
index 000000000..6ba1ed1df
--- /dev/null
+++ b/hott/hit/refl_quotient.hlean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Floris van Doorn
+
+Quotient of a reflexive relation
+-/
+
+import hit.circle types.cubical.squareover .two_quotient
+
+open eq simple_two_quotient e_closure
+
+namespace refl_quotient
+section
+
+  parameters {A : Type} (R : A → A → Type) (ρ : Πa, R a a)
+  inductive refl_quotient_Q : Π⦃a : A⦄, e_closure R a a → Type :=
+  | Qmk {} : Π(a : A), refl_quotient_Q [ρ a]
+  open refl_quotient_Q
+  local abbreviation Q := refl_quotient_Q
+
+  definition refl_quotient : Type := simple_two_quotient R Q -- TODO: define this in root namespace
+
+  definition rclass_of (a : A) : refl_quotient := incl0 R Q a
+  definition req_of_rel ⦃a a' : A⦄ (r : R a a') : rclass_of a = rclass_of a' :=
+  incl1 R Q r
+
+  definition pρ (a : A) : req_of_rel (ρ a) = idp :=
+  incl2 R Q (Qmk a)
+
+  -- protected definition rec {P : refl_quotient → Type}
+  --   (Pc : Π(a : A), P (rclass_of a))
+  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
+  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo)
+  --   (x : refl_quotient) : P x :=
+  -- sorry
+
+  -- protected definition rec_on [reducible] {P : refl_quotient → Type}
+  --   (Pc : Π(a : A), P (rclass_of a))
+  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
+  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo) : P y :=
+  -- rec Pinl Pinr Pglue y
+
+  -- definition rec_req_of_rel {P : Type} {P : refl_quotient → Type}
+  --   (Pc : Π(a : A), P (rclass_of a))
+  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
+  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo)
+  --   ⦃a a' : A⦄ (r : R a a') : apdo (rec Pc Pp Pr) (req_of_rel r) = Pp r :=
+  -- !rec_incl1
+
+  -- theorem rec_pρ {P : Type} {P : refl_quotient → Type}
+  --   (Pc : Π(a : A), P (rclass_of a))
+  --   (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
+  --   (Pr : Π(a : A), Pp (ρ a) =[pρ a] idpo) (a : A)
+  --    : square (ap02 (rec Pc Pp Pr) (pρ a)) (Pr a) (elim_req_of_rel Pr (ρ a)) idp :=
+  -- !rec_incl2
+
+  protected definition elim {P : Type} (Pc : Π(a : A), P)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (Pr : Π(a : A), Pp (ρ a) = idp)
+    (x : refl_quotient) : P :=
+  begin
+    induction x,
+      exact Pc a,
+      exact Pp s,
+      induction q, apply Pr
+  end
+
+  protected definition elim_on [reducible] {P : Type} (x : refl_quotient) (Pc : Π(a : A), P)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (Pr : Π(a : A), Pp (ρ a) = idp) : P :=
+  elim Pc Pp Pr x
+
+  definition elim_req_of_rel {P : Type} {Pc : Π(a : A), P}
+    {Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a'} (Pr : Π(a : A), Pp (ρ a) = idp)
+    ⦃a a' : A⦄ (r : R a a') : ap (elim Pc Pp Pr) (req_of_rel r) = Pp r :=
+  !elim_incl1
+
+  theorem elim_pρ {P : Type} (Pc : Π(a : A), P)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (Pr : Π(a : A), Pp (ρ a) = idp) (a : A)
+     : square (ap02 (elim Pc Pp Pr) (pρ a)) (Pr a) (elim_req_of_rel Pr (ρ a)) idp :=
+  !elim_incl2
+
+end
+end refl_quotient
+
+attribute refl_quotient.rclass_of [constructor]
+attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold-c 8] [recursor 8]
+--attribute refl_quotient.elim_type [unfold-c 9]
+attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold-c 5]
+--attribute refl_quotient.elim_type_on [unfold-c 6]
diff --git a/hott/hit/torus.hlean b/hott/hit/torus.hlean
new file mode 100644
index 000000000..ba7932e99
--- /dev/null
+++ b/hott/hit/torus.hlean
@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Floris van Doorn
+
+Declaration of the torus
+-/
+
+import .two_quotient
+
+open two_quotient eq bool unit relation
+
+namespace torus
+
+  definition torus_R (x y : unit) := bool
+  local infix `⬝r`:75 := @e_closure.trans unit torus_R star star star
+  local postfix `⁻¹ʳ`:(max+10) := @e_closure.symm unit torus_R star star
+  local notation `[`:max a `]`:0 := @e_closure.of_rel unit torus_R star star a
+
+  inductive torus_Q : Π⦃x y : unit⦄, e_closure torus_R x y → e_closure torus_R x y → Type :=
+  | Qmk : torus_Q ([ff] ⬝r [tt]) ([tt] ⬝r [ff])
+
+  definition torus := two_quotient torus_R torus_Q
+  definition base  : torus := incl0 _ _ star
+  definition loop1 : base = base := incl1 _ _ ff
+  definition loop2 : base = base := incl1 _ _ tt
+  definition surf  : loop1 ⬝ loop2 = loop2 ⬝ loop1 :=
+  incl2 _ _ torus_Q.Qmk
+
+  -- protected definition rec {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
+  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
+  --   (x : torus) : P x :=
+  -- sorry
+
+  -- example {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb) (Pl2 : Pb =[loop2] Pb)
+  --         (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2) : torus.rec Pb Pl1 Pl2 Pf base = Pb := idp
+
+  -- definition rec_loop1 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
+  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
+  --   : apdo (torus.rec Pb Pl1 Pl2 Pf) loop1 = Pl1 :=
+  -- sorry
+
+  -- definition rec_loop2 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
+  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
+  --   : apdo (torus.rec Pb Pl1 Pl2 Pf) loop2 = Pl2 :=
+  -- sorry
+
+  -- definition rec_surf {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
+  --   (Pl2 : Pb =[loop2] Pb) (Pf : squareover P fill Pl1 Pl1 Pl2 Pl2)
+  --   : cubeover P rfl1 (apds (torus.rec Pb Pl1 Pl2 Pf) fill) Pf
+  --              (vdeg_squareover !rec_loop2) (vdeg_squareover !rec_loop2)
+  --              (vdeg_squareover !rec_loop1) (vdeg_squareover !rec_loop1) :=
+  -- sorry
+
+  protected definition elim {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
+    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) (x : torus) : P :=
+  begin
+    induction x,
+    { exact Pb},
+    { induction s,
+      { exact Pl1},
+      { exact Pl2}},
+    { induction q, exact Ps},
+  end
+
+  protected definition elim_on [reducible] {P : Type} (x : torus) (Pb : P)
+    (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : P :=
+  torus.elim Pb Pl1 Pl2 Ps x
+
+  definition elim_loop1 {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
+    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop1 = Pl1 :=
+  !elim_incl1
+
+  definition elim_loop2 {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
+    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
+  !elim_incl1
+
+  definition elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
+    (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1)
+  : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf)
+           Ps
+           (!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2))
+           (!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) :=
+  !elim_incl2
+
+end torus
+
+attribute torus.base [constructor]
+attribute /-torus.rec-/ torus.elim [unfold-c 6] [recursor 6]
+--attribute torus.elim_type [unfold-c 9]
+attribute /-torus.rec_on-/ torus.elim_on [unfold-c 2]
+--attribute torus.elim_type_on [unfold-c 6]
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
new file mode 100644
index 000000000..3452230bf
--- /dev/null
+++ b/hott/hit/two_quotient.hlean
@@ -0,0 +1,320 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Floris van Doorn
+-/
+
+import hit.circle types.eq2 algebra.e_closure
+
+open quotient eq circle sum sigma equiv function relation
+
+namespace simple_two_quotient
+
+  section
+  parameters {A : Type}
+             (R : A → A → Type)
+  local abbreviation T := e_closure R -- the (type-valued) equivalence closure of R
+  parameter  (Q : Π⦃a⦄, T a a → Type)
+  variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
+
+
+  local abbreviation B := A ⊎ Σ(a : A) (r : T a a), Q r
+
+  inductive pre_simple_two_quotient_rel : B → B → Type :=
+  | pre_Rmk {} : Π⦃a a'⦄ (r : R a a'), pre_simple_two_quotient_rel (inl a) (inl a')
+  --BUG: if {} not provided, the alias for pre_Rmk is wrong
+
+  definition pre_simple_two_quotient := quotient pre_simple_two_quotient_rel
+
+  open pre_simple_two_quotient_rel
+  local abbreviation C := quotient pre_simple_two_quotient_rel
+  protected definition j [constructor] (a : A) : C := class_of pre_simple_two_quotient_rel (inl a)
+  protected definition pre_aux [constructor] (q : Q r) : C :=
+  class_of pre_simple_two_quotient_rel (inr ⟨a, r, q⟩)
+  protected definition e (s : R a a') : j a = j a' := eq_of_rel _ (pre_Rmk s)
+  protected definition et (t : T a a') : j a = j a' := e_closure.elim e t
+  protected definition f [unfold-c 7] (q : Q r) : S¹ → C :=
+  circle.elim (j a) (et r)
+
+  protected definition pre_rec [unfold-c 8] {P : C → Type}
+    (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q))
+    (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') (x : C) : P x :=
+  begin
+    induction x with p,
+    { induction p,
+      { apply Pj},
+      { induction a with a1 a2, induction a2, apply Pa}},
+    { induction H, esimp, apply Pe},
+  end
+
+  protected definition pre_elim [unfold-c 8] {P : Type} (Pj : A → P)
+    (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') (x : C)
+    : P :=
+  pre_rec Pj Pa (λa a' s, pathover_of_eq (Pe s)) x
+
+  protected theorem rec_e {P : C → Type}
+    (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q))
+    (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') ⦃a a' : A⦄ (s : R a a')
+    : apdo (pre_rec Pj Pa Pe) (e s) = Pe s :=
+  !rec_eq_of_rel
+
+  protected theorem elim_e {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P)
+    (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') ⦃a a' : A⦄ (s : R a a')
+    : ap (pre_elim Pj Pa Pe) (e s) = Pe s :=
+  begin
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (e s)),
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pre_elim,rec_e],
+  end
+
+  protected definition elim_et {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P)
+    (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') ⦃a a' : A⦄ (t : T a a')
+    : ap (pre_elim Pj Pa Pe) (et t) = e_closure.elim Pe t :=
+  ap_e_closure_elim_h e (elim_e Pj Pa Pe) t
+
+  inductive simple_two_quotient_rel : C → C → Type :=
+  | Rmk {} : Π{a : A} {r : T a a} (q : Q r) (x : circle), simple_two_quotient_rel (f q x) (pre_aux q)
+
+  open simple_two_quotient_rel
+  definition simple_two_quotient := quotient simple_two_quotient_rel
+  local abbreviation D := simple_two_quotient
+  local abbreviation i := class_of simple_two_quotient_rel
+  definition incl0 (a : A) : D := i (j a)
+  protected definition aux (q : Q r) : D := i (pre_aux q)
+  definition incl1 (s : R a a') : incl0 a = incl0 a' := ap i (e s)
+  definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t
+  -- "wrong" version inclt, which is ap i (p ⬝ q) instead of ap i p ⬝ ap i q
+  -- it is used in the proof, because inclt is easier to work with
+  protected definition incltw (t : T a a') : incl0 a = incl0 a' := ap i (et t)
+
+  protected definition inclt_eq_incltw (t : T a a') : inclt t = incltw t :=
+  (ap_e_closure_elim i e t)⁻¹
+
+  definition incl2' (q : Q r) (x : S¹) : i (f q x) = aux q :=
+  eq_of_rel simple_two_quotient_rel (Rmk q x)
+
+  protected definition incl2w (q : Q r) : incltw r = idp :=
+  (ap02 i (elim_loop (j a) (et r))⁻¹) ⬝
+  (ap_compose i (f q) loop)⁻¹ ⬝
+  ap_weakly_constant (incl2' q) loop ⬝
+  !con.right_inv
+
+  definition incl2 (q : Q r) : inclt r = idp :=
+  inclt_eq_incltw r ⬝ incl2w q
+
+  local attribute simple_two_quotient f i incl0 aux incl1 incl2' inclt [reducible]
+  local attribute i aux incl0 [constructor]
+  protected definition elim {P : Type} (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    (x : D) : P :=
+  begin
+    induction x,
+    { refine (pre_elim _ _ _ a),
+      { exact P0},
+      { intro a r q, exact P0 a},
+      { exact P1}},
+    { exact abstract begin induction H, induction x,
+      { exact idpath (P0 a)},
+      { unfold f, apply pathover_eq, apply hdeg_square,
+        exact abstract ap_compose (pre_elim P0 _ P1) (f q) loop ⬝
+              ap _ !elim_loop ⬝
+              !elim_et ⬝
+              P2 q ⬝
+              !ap_constant⁻¹ end
+} end end},
+  end
+  local attribute elim [unfold-c 8]
+
+  protected definition elim_on {P : Type} (x : D) (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+     : P :=
+  elim P0 P1 P2 x
+
+  definition elim_incl1 {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    ⦃a a' : A⦄ (s : R a a') : ap (elim P0 P1 P2) (incl1 s) = P1 s :=
+  (ap_compose (elim P0 P1 P2) i (e s))⁻¹ ⬝ !elim_e
+
+  definition elim_inclt {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t :=
+  ap_e_closure_elim_h incl1 (elim_incl1 P2) t
+
+  protected definition elim_incltw {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (incltw t) = e_closure.elim P1 t :=
+  (ap_compose (elim P0 P1 P2) i (et t))⁻¹ ⬝ !elim_et
+
+  protected theorem elim_inclt_eq_elim_incltw {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    ⦃a a' : A⦄ (t : T a a')
+    : elim_inclt P2 t = ap (ap (elim P0 P1 P2)) (inclt_eq_incltw t) ⬝ elim_incltw P2 t :=
+  begin
+    unfold [elim_inclt,elim_incltw,inclt_eq_incltw,et],
+    refine !ap_e_closure_elim_h_eq ⬝ _,
+    rewrite [ap_inv,-con.assoc],
+    xrewrite [eq_of_square (ap_ap_e_closure_elim i (elim P0 P1 P2) e t)⁻¹ʰ],
+    rewrite [↓incl1,con.assoc], apply whisker_left,
+    rewrite [↑[elim_et,elim_incl1],+ap_e_closure_elim_h_eq,con_inv,↑[i,function.compose]],
+    rewrite [-con.assoc (_ ⬝ _),con.assoc _⁻¹,con.left_inv,▸*,-ap_inv,-ap_con],
+    apply ap (ap _),
+    krewrite [-eq_of_homotopy3_inv,-eq_of_homotopy3_con]
+  end
+
+  definition elim_incl2'_incl0 {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) :=
+  !elim_eq_of_rel
+
+  -- set_option pp.implicit true
+  protected theorem elim_incl2w {P : Type} (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r)
+    : square (ap02 (elim P0 P1 P2) (incl2w q)) (P2 q) (elim_incltw P2 r) idp :=
+  begin
+    esimp [incl2w,ap02],
+    rewrite [+ap_con (ap _),▸*],
+    xrewrite [-ap_compose (ap _) (ap i)],
+    rewrite [+ap_inv],
+    xrewrite [eq_top_of_square
+               ((ap_compose_natural (elim P0 P1 P2) i (elim_loop (j a) (et r)))⁻¹ʰ⁻¹ᵛ ⬝h
+               (ap_ap_compose (elim P0 P1 P2) i (f q) loop)⁻¹ʰ⁻¹ᵛ ⬝h
+               ap_ap_weakly_constant (elim P0 P1 P2) (incl2' q) loop ⬝h
+               ap_con_right_inv_sq (elim P0 P1 P2) (incl2' q base)),
+               ↑[elim_incltw]],
+    apply whisker_tl,
+    rewrite [ap_weakly_constant_eq],
+    xrewrite [naturality_apdo_eq (λx, !elim_eq_of_rel) loop],
+    rewrite [↑elim_2,rec_loop,square_of_pathover_concato_eq,square_of_pathover_eq_concato,
+            eq_of_square_vconcat_eq,eq_of_square_eq_vconcat],
+    apply eq_vconcat,
+    { apply ap (λx, _ ⬝ eq_con_inv_of_con_eq ((_ ⬝ x ⬝ _)⁻¹ ⬝ _) ⬝ _),
+      transitivity _, apply ap eq_of_square,
+        apply to_right_inv !pathover_eq_equiv_square (hdeg_square (elim_1 P A R Q P0 P1 a r q P2)),
+      transitivity _, apply eq_of_square_hdeg_square,
+      unfold elim_1, reflexivity},
+    rewrite [+con_inv,whisker_left_inv,+inv_inv,-whisker_right_inv,
+             con.assoc (whisker_left _ _),con.assoc _ (whisker_right _ _),▸*,
+             whisker_right_con_whisker_left _ !ap_constant],
+    xrewrite [-con.assoc _ _ (whisker_right _ _)],
+    rewrite [con.assoc _ _ (whisker_left _ _),idp_con_whisker_left,▸*,
+             con.assoc _ !ap_constant⁻¹,con.left_inv],
+    xrewrite [eq_con_inv_of_con_eq_whisker_left,▸*],
+    rewrite [+con.assoc _ _ !con.right_inv,
+             right_inv_eq_idp (
+               (λ(x : ap (elim P0 P1 P2) (incl2' q base) = idpath
+               (elim P0 P1 P2 (class_of simple_two_quotient_rel (f q base)))), x)
+                (elim_incl2'_incl0 P2 q)),
+             ↑[whisker_left]],
+    xrewrite [con2_con_con2],
+    rewrite [idp_con,↑elim_incl2'_incl0,con.left_inv,whisker_right_inv,↑whisker_right],
+    xrewrite [con.assoc _ _ (_ ◾ _)],
+    rewrite [con.left_inv,▸*,-+con.assoc,con.assoc _⁻¹,↑[elim,function.compose],con.left_inv,
+             ▸*,↑j,con.left_inv,idp_con],
+    apply square_of_eq, reflexivity
+  end
+
+  theorem elim_incl2 {P : Type} (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
+    ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r)
+    : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 r) idp :=
+  begin
+    rewrite [↑incl2,↑ap02,ap_con,elim_inclt_eq_elim_incltw],
+    apply whisker_tl,
+    apply elim_incl2w
+  end
+
+end
+end simple_two_quotient
+
+--attribute simple_two_quotient.j [constructor] --TODO
+attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold-c 8] [recursor 8]
+--attribute simple_two_quotient.elim_type [unfold-c 9]
+attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold-c 5]
+--attribute simple_two_quotient.elim_type_on [unfold-c 6]
+
+namespace two_quotient
+  open e_closure simple_two_quotient
+  section
+  parameters {A : Type}
+             (R : A → A → Type)
+  local abbreviation T := e_closure R -- the (type-valued) equivalence closure of R
+  parameter  (Q : Π⦃a a'⦄, T a a' → T a a' → Type)
+  variables ⦃a a' : A⦄ {s : R a a'} {t t' : T a a'}
+
+
+  inductive two_quotient_Q : Π⦃a : A⦄, e_closure R a a → Type :=
+  | Qmk : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄, Q t t' → two_quotient_Q (t ⬝r t'⁻¹ʳ)
+  open two_quotient_Q
+  local abbreviation Q2 := two_quotient_Q
+
+  definition two_quotient := simple_two_quotient R Q2
+  definition incl0 (a : A) : two_quotient := incl0 _ _ a
+  definition incl1 (s : R a a') : incl0 a = incl0 a' := incl1 _ _ s
+  definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t
+  definition incl2 (q : Q t t') : inclt t = inclt t' :=
+  eq_of_con_inv_eq_idp (incl2 _ _ (Qmk R q))
+
+  protected definition elim {P : Type} (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    (x : two_quotient) : P :=
+  begin
+    induction x,
+    { exact P0 a},
+    { exact P1 s},
+    { exact abstract [unfold-c 10] begin induction q with a a' t t' q,
+      rewrite [↑e_closure.elim,↓e_closure.elim P1 t,↓e_closure.elim P1 t'],
+      apply con_inv_eq_idp, exact P2 q end end},
+  end
+  local attribute elim [unfold-c 8]
+
+  protected definition elim_on {P : Type} (x : two_quotient) (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+     : P :=
+  elim P0 P1 P2 x
+
+  definition elim_incl1 {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (s : R a a') : ap (elim P0 P1 P2) (incl1 s) = P1 s :=
+  !elim_incl1
+
+  definition elim_inclt {P : Type} {P0 : A → P}
+    {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t :=
+  !elim_inclt --ap_e_closure_elim_h incl1 (elim_incl1 P2) t
+
+  --print elim
+  theorem elim_incl2 {P : Type} (P0 : A → P)
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
+    ⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t')
+    : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') :=
+  begin
+    -- let H := elim_incl2 R Q2 P0 P1 (two_quotient_Q.rec (λ (a a' : A) (t t' : T a a') (q : Q t t'), con_inv_eq_idp (P2 q))) (Qmk R q),
+    -- esimp at H,
+    rewrite [↑[incl2,elim],ap_eq_of_con_inv_eq_idp],
+    xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q)),▸*],
+    exact sorry
+  end
+
+end
+end two_quotient
+
+--attribute two_quotient.j [constructor] --TODO
+attribute /-two_quotient.rec-/ two_quotient.elim [unfold-c 8] [recursor 8]
+--attribute two_quotient.elim_type [unfold-c 9]
+attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold-c 5]
+--attribute two_quotient.elim_type_on [unfold-c 6]