diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean
index 5c7891518..36e20800c 100644
--- a/hott/homotopy/cofiber.hlean
+++ b/hott/homotopy/cofiber.hlean
@@ -9,60 +9,51 @@ import hit.pushout function .susp types.unit
 
 open eq pushout unit pointed is_trunc is_equiv susp unit equiv
 
-definition cofiber {A B : Type} (f : A → B) := pushout (λ (a : A), ⋆) f
+definition cofiber {A B : Type} (f : A → B) := pushout f (λ (a : A), ⋆)
 
 namespace cofiber
   section
   parameters {A B : Type} (f : A → B)
 
-  protected definition base : cofiber f := inl ⋆
-
-  protected definition cod : B → cofiber f := inr
+  definition cod : B → cofiber f := inl
+  definition base : cofiber f := inr ⋆
 
   parameter {f}
-  protected definition glue (a : A) : cofiber.base f = cofiber.cod f (f a) :=
+  protected definition glue (a : A) : cofiber.cod f (f a) = cofiber.base f :=
   pushout.glue a
 
-  parameter (f)
-  protected definition contr_of_equiv [H : is_equiv f] : is_contr (cofiber f) :=
-  begin
-    fapply is_contr.mk, exact base,
-    intro a, induction a with [u, b],
-    { cases u, reflexivity },
-    { exact !glue ⬝ ap inr (right_inv f b) },
-    { apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !ap_constant ⬝ph _,
-      apply move_bot_of_left, refine !idp_con ⬝ph _, apply transpose, esimp,
-      refine _ ⬝hp (ap (ap inr) !adj⁻¹), refine _ ⬝hp !ap_compose, apply square_Flr_idp_ap },
-  end
-
-  parameter {f}
-  protected definition rec {P : cofiber f → Type}
-    (Pbase : P base) (Pcod : Π (b : B), P (cod b))
-    (Pglue : Π (a : A), pathover P Pbase (glue a) (Pcod (f a))) :
+  protected definition rec {P : cofiber f → Type} (Pcod : Π (b : B), P (cod b)) (Pbase : P base)
+    (Pglue : Π (a : A), pathover P (Pcod (f a)) (glue a) Pbase) :
     (Π y, P y) :=
   begin
-    intro y, induction y, induction x, exact Pbase, exact Pcod x, esimp, exact Pglue x,
+    intro y, induction y, exact Pcod x, induction x, exact Pbase, exact Pglue x
   end
 
   protected definition rec_on {P : cofiber f → Type} (y : cofiber f)
-    (Pbase : P base) (Pcod : Π (b : B), P (cod b))
-    (Pglue : Π (a : A), pathover P Pbase (glue a) (Pcod (f a))) : P y :=
-  cofiber.rec Pbase Pcod Pglue y
+    (Pcod : Π (b : B), P (cod b)) (Pbase : P base)
+    (Pglue : Π (a : A), pathover P (Pcod (f a)) (glue a) Pbase) : P y :=
+  cofiber.rec Pcod Pbase Pglue y
 
-  protected definition elim {P : Type} (Pbase : P) (Pcod : B → P)
-    (Pglue : Π (x : A), Pbase = Pcod (f x)) (y : cofiber f) : P :=
-  pushout.elim (λu, Pbase) Pcod Pglue y
+  protected theorem rec_glue {P : cofiber f → Type} (Pcod : Π (b : B), P (cod b)) (Pbase : P base)
+    (Pglue : Π (a : A), pathover P (Pcod (f a)) (glue a) Pbase) (a : A)
+    : apd (cofiber.rec Pcod Pbase Pglue) (cofiber.glue a) = Pglue a :=
+  !pushout.rec_glue
 
-  protected definition elim_on {P : Type} (y : cofiber f) (Pbase : P) (Pcod : B → P)
-    (Pglue : Π (x : A), Pbase = Pcod (f x)) : P :=
-  cofiber.elim Pbase Pcod Pglue y
+  protected definition elim {P : Type} (Pcod : B → P) (Pbase : P)
+    (Pglue : Π (x : A), Pcod (f x) = Pbase) (y : cofiber f) : P :=
+  pushout.elim Pcod (λu, Pbase) Pglue y
 
-  protected theorem elim_glue {P : Type} (y : cofiber f) (Pbase : P) (Pcod : B → P)
-    (Pglue : Π (x : A), Pbase = Pcod (f x)) (a : A)
-    : ap (elim Pbase Pcod Pglue) (glue a) = Pglue a :=
+  protected definition elim_on {P : Type} (y : cofiber f) (Pcod : B → P) (Pbase : P)
+    (Pglue : Π (x : A), Pcod (f x) = Pbase) : P :=
+  cofiber.elim Pcod Pbase Pglue y
+
+  protected theorem elim_glue {P : Type} (Pcod : B → P) (Pbase : P)
+    (Pglue : Π (x : A), Pcod (f x) = Pbase) (a : A)
+    : ap (cofiber.elim Pcod Pbase Pglue) (cofiber.glue a) = Pglue a :=
   !pushout.elim_glue
 
   end
+
 end cofiber
 
 attribute cofiber.base cofiber.cod [constructor]
@@ -78,21 +69,42 @@ notation `ℂ` := pcofiber
 
 namespace cofiber
 
-  variables (A : Type*)
+  variables {A B : Type*} (f : A →* B)
 
-  definition cofiber_unit : pcofiber (pconst A punit) ≃* psusp A :=
+  definition is_contr_cofiber_of_equiv [H : is_equiv f] : is_contr (cofiber f) :=
+  begin
+    fapply is_contr.mk, exact cofiber.base f,
+    intro a, induction a with b a,
+    { exact !glue⁻¹ ⬝ ap inl (right_inv f b) },
+    { reflexivity },
+    { apply eq_pathover_constant_left_id_right, apply move_top_of_left,
+      refine _ ⬝pv natural_square_tr cofiber.glue (left_inv f a) ⬝vp !ap_constant,
+      refine ap02 inl _ ⬝ !ap_compose⁻¹, exact adj f a },
+  end
+
+  definition pcod [constructor] (f : A →* B) : B →* pcofiber f :=
+  pmap.mk (cofiber.cod f) (ap inl (respect_pt f)⁻¹ ⬝ cofiber.glue pt)
+
+  definition pcod_pcompose [constructor] (f : A →* B) : pcod f ∘* f ~* pconst A (ℂ f) :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, exact cofiber.glue a },
+    { exact !con_inv_cancel_left⁻¹ ⬝ idp ◾ (!ap_inv⁻¹ ◾ idp) }
+  end
+
+  definition pcofiber_punit (A : Type*) : pcofiber (pconst A punit) ≃* psusp A :=
   begin
     fapply pequiv_of_pmap,
     { fconstructor, intro x, induction x, exact north, exact south, exact merid x,
-      reflexivity },
+      exact (merid pt)⁻¹ },
     { esimp, fapply adjointify,
       { intro s, induction s, exact inl ⋆, exact inr ⋆, apply glue a },
       { intro s, induction s, do 2 reflexivity, esimp,
         apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, apply hdeg_square,
         refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
         refine ap _ !elim_merid ⬝ _, apply elim_glue },
-      { intro c, induction c with s, reflexivity,
-        induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square,
+      { intro c, induction c with u, induction u, reflexivity,
+        reflexivity, esimp, apply eq_pathover, apply hdeg_square,
         refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
         refine ap02 _ !elim_glue ⬝ _, apply elim_merid }},
   end