diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index c1ad224f3..5a01c4ba7 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -22,6 +22,7 @@ namespace e_closure
   infix ` ⬝r `:75 := e_closure.trans
   postfix `⁻¹ʳ`:(max+10) := e_closure.symm
   notation `[`:max a `]`:0 := e_closure.of_rel a
+  notation `<`:max p `>`:0 := e_closure.of_path _ p
   abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
 end e_closure
 open e_closure
@@ -57,21 +58,6 @@ section
       exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (IH₁ ◾ IH₂)
   end
 
-/-  definition ap_e_closure_elim_h_inv [unfold_full] {B C : Type} {f : A → B} {g : B → C}
-    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
-    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
-    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
-    : ap_e_closure_elim_h e p t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim_h e p t)⁻² :=
-  by reflexivity
-
-  definition ap_e_closure_elim_h_con [unfold_full] {B C : Type} {f : A → B} {g : B → C}
-    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
-    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
-    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') (t' : T a' a'')
-    : ap_e_closure_elim_h e p (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝
-        (ap_e_closure_elim_h e p t ◾ ap_e_closure_elim_h e p t') :=
-  by reflexivity-/
-
   definition ap_e_closure_elim [unfold 10] {B C : Type} {f : A → B} (g : B → C)
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
     : ap g (e_closure.elim e t) = e_closure.elim (λa a' r, ap g (e r)) t :=
@@ -141,6 +127,7 @@ section
       intro a a' a'' t t', exact t ⬝r t',
   end
 
+/-
   definition e_closure.transport_left {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
     (t : e_closure R a a') (p : a = a'')
     : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t :=
@@ -155,6 +142,7 @@ section
     (t : e_closure R a a) (p : a = a')
     : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) :=
   by induction p; esimp; exact !idp_con⁻¹
+-/
 
   /- dependent elimination -/
 
diff --git a/hott/hit/hit.md b/hott/hit/hit.md
index 38caac3e7..c73e0dbd5 100644
--- a/hott/hit/hit.md
+++ b/hott/hit/hit.md
@@ -14,9 +14,13 @@ hits related to homotopy theory are defined in
 
 Files in this folder:
 
-* [quotient](quotient.hlean) (quotients, primitive)
-* [trunc](trunc.hlean) (truncation, primitive)
-* [colimit](colimit.hlean) (Colimits of arbitrary diagrams and sequential colimits, defined using quotients)
-* [pushout](pushout.hlean) (Pushouts, defined using quotients)
-* [coeq](coeq.hlean) (Co-equalizers, defined using quotients)
-* [set_quotient](set_quotient.hlean) (Set-quotients, defined using quotients and set-truncation)
+* [quotient](quotient.hlean): quotients, primitive
+* [trunc](trunc.hlean): truncation, primitive
+* [colimit](colimit.hlean): Colimits of arbitrary diagrams and sequential colimits, defined using quotients
+* [pushout](pushout.hlean): Pushouts, defined using quotients
+* [coeq](coeq.hlean): Co-equalizers, defined using quotients
+* [set_quotient](set_quotient.hlean): Set-quotients, defined using quotients and set-truncation
+
+The following hits have also 2-constructors. They are defined only using quotients.
+* [two_quotient](two_quotient.hlean): Quotients where you can also specify 2-paths. These are used for all hits which have 2-constructors, and they are almost fully general for such hits, as long as they are nonrecursive
+* [refl_quotient](refl_quotient.hlean): Quotients where you can also specify 2-paths
\ No newline at end of file
diff --git a/hott/hit/refl_quotient.hlean b/hott/hit/refl_quotient.hlean
index bc4e46784..3f5cc05e1 100644
--- a/hott/hit/refl_quotient.hlean
+++ b/hott/hit/refl_quotient.hlean
@@ -20,7 +20,7 @@ section
   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 refl_quotient : Type := simple_two_quotient R Q
 
   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' :=
@@ -29,32 +29,26 @@ section
   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 {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), change_path (pρ a) (Pp (ρ a)) = idpo) (x : refl_quotient) : P x :=
+  begin
+    induction x,
+      exact Pc a,
+      exact Pp s,
+      induction q, apply Pr
+  end
 
-  -- 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
+  protected definition rec_on [reducible] {P : refl_quotient → Type} (x : refl_quotient)
+    (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), change_path (pρ a) (Pp (ρ a)) = idpo) : P x :=
+  rec Pc Pp Pr x
 
-  -- 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
+  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), change_path (pρ a) (Pp (ρ a)) = idpo) ⦃a a' : A⦄ (r : R a a')
+    : apdo (rec Pc Pp Pr) (req_of_rel r) = Pp r :=
+  !rec_incl1
 
   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)
@@ -84,7 +78,7 @@ end
 end refl_quotient
 
 attribute refl_quotient.rclass_of [constructor]
-attribute /-refl_quotient.rec-/ refl_quotient.elim [unfold 8] [recursor 8]
+attribute refl_quotient.rec refl_quotient.elim [unfold 8] [recursor 8]
 --attribute refl_quotient.elim_type [unfold 9]
-attribute /-refl_quotient.rec_on-/ refl_quotient.elim_on [unfold 5]
+attribute refl_quotient.rec_on refl_quotient.elim_on [unfold 5]
 --attribute refl_quotient.elim_type_on [unfold 6]
diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean
index 89a7eb9df..b86eb8adc 100644
--- a/hott/hit/set_quotient.hlean
+++ b/hott/hit/set_quotient.hlean
@@ -34,7 +34,7 @@ section
     { intro x', apply Pt},
     { intro y, fapply (quotient.rec_on y),
       { exact Pc},
-      { intros, apply equiv.to_inv !(pathover_compose _ tr), apply Pp}}
+      { intros, exact pathover_of_pathover_ap P tr (Pp H)}}
   end
 
   protected definition rec_on [reducible] {P : set_quotient → Type} (x : set_quotient)
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index d8fa7d12e..fd76c80b7 100644
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@@ -133,6 +133,7 @@ namespace simple_two_quotient
   local attribute simple_two_quotient f i D incl0 aux incl1 incl2' inclt [reducible]
   local attribute i aux incl0 [constructor]
 
+  parameters {R Q}
   protected definition rec {P : D → Type} (P0 : Π(a : A), P (incl0 a))
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
     (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
@@ -358,6 +359,7 @@ namespace two_quotient
   definition incl2 (q : Q t t') : inclt t = inclt t' :=
   eq_of_con_inv_eq_idp (incl2 _ _ (Qmk R q))
 
+  parameters {R Q}
   protected definition rec {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
@@ -389,14 +391,14 @@ namespace two_quotient
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
       change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
     ⦃a a' : A⦄ (s : R a a') : apdo (rec P0 P1 P2) (incl1 s) = P1 s :=
-  rec_incl1 _ _ _ _ _ s
+  rec_incl1 _ _ _ s
 
   theorem rec_inclt {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
       change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
     ⦃a a' : A⦄ (t : T a a') : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
-  rec_inclt _ _ _ _ _ t
+  rec_inclt _ _ _ t
 
   protected definition elim {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
@@ -437,15 +439,15 @@ namespace two_quotient
     : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') :=
   begin
     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))],
-    xrewrite [{simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2)
+    xrewrite [eq_top_of_square (elim_incl2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q))],
+    xrewrite [{simple_two_quotient.elim_inclt (elim_1 A R Q P P0 P1 P2)
            (t ⬝r t'⁻¹ʳ)}
-      idpath (ap_con (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2))
+      idpath (ap_con (simple_two_quotient.elim P0 P1 (elim_1 A R Q P P0 P1 P2))
                      (inclt t) (inclt t')⁻¹ ⬝
-             (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t ◾
-             (ap_inv (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2))
+             (simple_two_quotient.elim_inclt (elim_1 A R Q P P0 P1 P2) t ◾
+             (ap_inv (simple_two_quotient.elim P0 P1 (elim_1 A R Q P P0 P1 P2))
                      (inclt t') ⬝
-             inverse2 (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t')))),▸*],
+             inverse2 (simple_two_quotient.elim_inclt (elim_1 A R Q P P0 P1 P2) t')))),▸*],
     rewrite [-con.assoc _ _ (con_inv_eq_idp _),-con.assoc _ _ (_ ◾ _),con.assoc _ _ (ap_con _ _ _),
              con.left_inv,↑whisker_left,con2_con_con2,-con.assoc (ap_inv _ _)⁻¹,
              con.left_inv,+idp_con,eq_of_con_inv_eq_idp_con2],