diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean
index 44e2a7c43..f055789a7 100644
--- a/hott/algebra/category/category.hlean
+++ b/hott/algebra/category/category.hlean
@@ -37,6 +37,15 @@ namespace category
   definition eq_of_iso [reducible] {a b : ob} : a ≅ b → a = b :=
   iso_of_eq⁻¹ᶠ
 
+  definition iso_of_eq_eq_of_iso {a b : ob} (p : a ≅ b) : iso_of_eq (eq_of_iso p) = p :=
+  right_inv iso_of_eq p
+
+  definition hom_of_eq_eq_of_iso {a b : ob} (p : a ≅ b) : hom_of_eq (eq_of_iso p) = to_hom p :=
+  ap to_hom !iso_of_eq_eq_of_iso
+
+  definition inv_of_eq_eq_of_iso {a b : ob} (p : a ≅ b) : inv_of_eq (eq_of_iso p) = to_inv p :=
+  ap to_inv !iso_of_eq_eq_of_iso
+
   definition is_trunc_1_ob : is_trunc 1 ob :=
   begin
     apply is_trunc_succ_intro, intro a b,
diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean
index f73e1f35d..cbdbf6fa3 100644
--- a/hott/algebra/category/constructions/comma.hlean
+++ b/hott/algebra/category/constructions/comma.hlean
@@ -8,7 +8,7 @@ Comma category
 
 import ..functor cubical.pathover ..strict ..category
 
-open core eq functor equiv sigma sigma.ops is_trunc cubical iso
+open eq functor equiv sigma sigma.ops is_trunc cubical iso is_equiv
 
 namespace category
 
@@ -16,9 +16,9 @@ namespace category
     (a : A)
     (b : B)
     (f : S a ⟶ T b)
-  abbreviation ob1 := @comma_object.a
-  abbreviation ob2 := @comma_object.b
-  abbreviation mor := @comma_object.f
+  abbreviation ob1 [unfold-c 6] := @comma_object.a
+  abbreviation ob2 [unfold-c 6] := @comma_object.b
+  abbreviation mor [unfold-c 6] := @comma_object.f
 
   variables {A B C : Precategory} (S : A ⇒ C) (T : B ⇒ C)
 
@@ -40,19 +40,27 @@ namespace category
     (r : mor x =[ap011 (@hom C C) (ap (to_fun_ob S) p) (ap (to_fun_ob T) q)] mor y) : x = y :=
   begin
     cases x with a b f, cases y with a' b' f', cases p, cases q,
-    esimp [ap011,congr,core.ap,subst] at r,
+    esimp [ap011,congr,ap,subst] at r,
     eapply (idp_rec_on r), reflexivity
   end
 
-  -- definition comma_object_eq {x y : comma_object S T} (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
-  --   (r : T (hom_of_eq q) ∘ mor x ∘ S (inv_of_eq p) = mor y) : x = y :=
-  -- begin
-  --   fapply comma_object_eq' p q,
-  --   --cases x with a b f, cases y with a' b' f', cases p, cases q,
-  --   --esimp [ap011,congr,core.ap,subst] at r,
-  --   --eapply (idp_rec_on r), reflexivity
-  -- end
+  --TODO: remove. This is a different version where Hq is not in square brackets
+  definition eq_comp_inverse_of_comp_eq' {ob : Type} {C : precategory ob} {d c b : ob} {r : hom c d}
+    {q : hom b c} {x : hom b d} {Hq : is_iso q} (p : r ∘ q = x) : r = x ∘ q⁻¹ʰ :=
+  sorry --eq_inverse_comp_of_comp_eq p
 
+  definition comma_object_eq {x y : comma_object S T} (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
+    (r : T (hom_of_eq q) ∘ mor x ∘ S (inv_of_eq p) = mor y) : x = y :=
+  begin
+    cases x with a b f, cases y with a' b' f', cases p, cases q,
+    have r' : f = f',
+    begin
+      rewrite [▸* at r, -r, respect_id, id_left, respect_inv'],
+      apply eq_comp_inverse_of_comp_eq',
+      rewrite [respect_id,id_right]
+    end,
+    rewrite r'
+  end
 
   definition ap_ob1_comma_object_eq' (x y : comma_object S T) (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
     (r : mor x =[ap011 (@hom C C) (ap (to_fun_ob S) p) (ap (to_fun_ob T) q)] mor y)
@@ -149,19 +157,20 @@ namespace category
     strict_precategory (comma_object S T) :=
   strict_precategory.mk (comma_category S T) !is_trunc_comma_object
 
-  -- definition is_univalent_comma (HA : is_univalent A) (HB : is_univalent B)
-  --   : is_univalent (comma_category S T) :=
-  -- begin
-  --   intros c d,
-  --   fapply adjointify,
-  --   { intro i, cases i with f s, cases s with g l r, cases f with fA fB fp, cases g with gA gB gp,
-  --     esimp at *, fapply comma_object_eq', unfold is_univalent at (HA, HB),
-  --       {apply iso_of_eq⁻¹ᶠ, exact (iso.MK fA gA (ap mor1 l) (ap mor1 r))},
-  --       {apply iso_of_eq⁻¹ᶠ, exact (iso.MK fB gB (ap mor2 l) (ap mor2 r))},
-  --       { apply sorry}},
-  --   { apply sorry},
-  --   { apply sorry},
-  -- end
+  --set_option pp.notation false
+  definition is_univalent_comma (HA : is_univalent A) (HB : is_univalent B)
+    : is_univalent (comma_category S T) :=
+  begin
+    intros c d,
+    fapply adjointify,
+    { intro i, cases i with f s, cases s with g l r, cases f with fA fB fp, cases g with gA gB gp,
+      esimp at *, fapply comma_object_eq,
+        {apply iso_of_eq⁻¹ᶠ, exact (iso.MK fA gA (ap mor1 l) (ap mor1 r))},
+        {apply iso_of_eq⁻¹ᶠ, exact (iso.MK fB gB (ap mor2 l) (ap mor2 r))},
+        { apply sorry /-rewrite hom_of_eq_eq_of_iso,-/ }},
+    { apply sorry},
+    { apply sorry},
+  end
 
 
 end category
diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index ae6861c34..5f05943b4 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -86,9 +86,7 @@ namespace functor
       apply (respect_id F) ),
   end
 
-  attribute functor.preserve_iso [instance]
-
-  protected definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b)
+  definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b)
     [H : is_iso f] [H' : is_iso (F f)] :
     F (f⁻¹) = (F f)⁻¹ :=
   begin
@@ -101,6 +99,11 @@ namespace functor
       apply right_inverse
   end
 
+  attribute functor.preserve_iso [instance]
+
+  definition respect_inv' (F : C ⇒ D) {a b : C} (f : hom a b) {H : is_iso f} : F (f⁻¹) = (F f)⁻¹ :=
+  respect_inv F f
+
   protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
       H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
   !functor_mk_eq_constant (λa b f, idp)
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 434960c97..c833ac96a 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -24,13 +24,13 @@ namespace iso
 
   attribute is_iso [multiple-instances]
   open split_mono split_epi is_iso
-  definition retraction_of [reducible] := @split_mono.retraction_of
-  definition retraction_comp [reducible] := @split_mono.retraction_comp
-  definition section_of [reducible] := @split_epi.section_of
-  definition comp_section [reducible] := @split_epi.comp_section
-  definition inverse [reducible] := @is_iso.inverse
-  definition left_inverse [reducible] := @is_iso.left_inverse
-  definition right_inverse [reducible] := @is_iso.right_inverse
+  abbreviation retraction_of [unfold-c 6] := @split_mono.retraction_of
+  abbreviation retraction_comp [unfold-c 6] := @split_mono.retraction_comp
+  abbreviation section_of [unfold-c 6] := @split_epi.section_of
+  abbreviation comp_section [unfold-c 6] := @split_epi.comp_section
+  abbreviation inverse [unfold-c 6] := @is_iso.inverse
+  abbreviation left_inverse [unfold-c 6] := @is_iso.left_inverse
+  abbreviation right_inverse [unfold-c 6] := @is_iso.right_inverse
   postfix `⁻¹` := inverse
   --a second notation for the inverse, which is not overloaded
   postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
@@ -84,6 +84,10 @@ namespace iso
     : (f⁻¹)⁻¹ = f :=
   inverse_eq_right !left_inverse
 
+  definition inverse_eq_inverse {f g : a ⟶ b} [H : is_iso f] [H : is_iso g] (p : f = g)
+    : f⁻¹ = g⁻¹ :=
+  by cases p;apply inverse_unique
+
   definition retraction_id (a : ob) : retraction_of (ID a) = id :=
   retraction_eq !id_comp
 
@@ -141,10 +145,10 @@ namespace iso
     (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
   @mk _ _ _ _ f (is_iso.mk H1 H2)
 
-  definition to_inv (f : a ≅ b) : b ⟶ a :=
+  definition to_inv [unfold-c 5] (f : a ≅ b) : b ⟶ a :=
   (to_hom f)⁻¹
 
-  protected definition refl (a : ob) : a ≅ a :=
+  protected definition refl [constructor] (a : ob) : a ≅ a :=
   mk (ID a)
 
   protected definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
@@ -178,13 +182,13 @@ namespace iso
       apply equiv.to_is_equiv (!iso.sigma_char),
   end
 
-  definition iso_of_eq (p : a = b) : a ≅ b :=
+  definition iso_of_eq [unfold-c 5] (p : a = b) : a ≅ b :=
   eq.rec_on p (iso.refl a)
 
-  definition hom_of_eq [reducible] (p : a = b) : a ⟶ b :=
+  definition hom_of_eq [reducible] [unfold-c 5] (p : a = b) : a ⟶ b :=
   iso.to_hom (iso_of_eq p)
 
-  definition inv_of_eq [reducible] (p : a = b) : b ⟶ a :=
+  definition inv_of_eq [reducible] [unfold-c 5] (p : a = b) : b ⟶ a :=
   iso.to_inv (iso_of_eq p)
 
   definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) :=
diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean
index d6b4f9f2a..959bbd492 100644
--- a/hott/algebra/hott.hlean
+++ b/hott/algebra/hott.hlean
@@ -44,7 +44,7 @@ namespace algebra
   definition group_pathover {G : group A} {H : group B} (f : A ≃ B) : (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H :=
   begin
     revert H,
-    eapply (rec_on_ua3 f),
+    eapply (rec_on_ua_idp' f),
     intros H resp_mul,
     esimp [equiv.refl] at resp_mul, esimp,
     apply pathover_idp_of_eq, apply group_eq,
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 7884e74a5..0dfadab67 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -249,7 +249,7 @@ namespace equiv
   definition to_right_inv [reducible] [unfold-c 3] (f : A ≃ B) : f ∘ f⁻¹ ∼ id := right_inv f
   definition to_left_inv [reducible] [unfold-c 3] (f : A ≃ B) : f⁻¹ ∘ f ∼ id := left_inv f
 
-  protected definition refl [refl] : A ≃ A :=
+  protected definition refl [refl] [constructor] : A ≃ A :=
   equiv.mk id !is_equiv_id
 
   protected definition symm [symm] (f : A ≃ B) : B ≃ A :=
@@ -281,6 +281,6 @@ namespace equiv
     infixl `⬝e`:75 := equiv.trans
     postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
     postfix `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded
-    abbreviation erfl := @equiv.refl
+    abbreviation erfl [constructor] := @equiv.refl
   end ops
 end equiv
diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean
index 24a418c3a..95d8bd362 100644
--- a/hott/init/ua.hlean
+++ b/hott/init/ua.hlean
@@ -60,14 +60,19 @@ namespace equiv
     (f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f :=
   right_inv equiv_of_eq f ▸ H (ua f)
 
+  -- a variant where we immediately recurse on the equality in the new goal
+  definition rec_on_ua_idp [recursor] {A : Type} {P : Π{B}, A ≃ B → Type} {B : Type}
+    (f : A ≃ B) (H : P equiv.refl) : P f :=
+  rec_on_ua f (λq, eq.rec_on q H)
+
   -- a variant where (equiv_of_eq (ua f)) will be replaced by f in the new goal
-  definition rec_on_ua2 {A B : Type} {P : A ≃ B → A = B → Type}
+  definition rec_on_ua' {A B : Type} {P : A ≃ B → A = B → Type}
     (f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q) q) : P f (ua f) :=
   right_inv equiv_of_eq f ▸ H (ua f)
 
-  -- a variant where we immediately recurse on the equality in the new goal
-  definition rec_on_ua3 {A : Type} {P : Π{B}, A ≃ B → A = B → Type} {B : Type}
+  -- a variant where we do both
+  definition rec_on_ua_idp' {A : Type} {P : Π{B}, A ≃ B → A = B → Type} {B : Type}
     (f : A ≃ B) (H : P equiv.refl idp) : P f (ua f) :=
-  rec_on_ua2 f (λq, eq.rec_on q H)
+  rec_on_ua' f (λq, eq.rec_on q H)
 
 end equiv