diff --git a/theories/Colimits/SpanPushout.v b/theories/Colimits/SpanPushout.v
index cda85420c4c..23ce41a20ef 100644
--- a/theories/Colimits/SpanPushout.v
+++ b/theories/Colimits/SpanPushout.v
@@ -1,5 +1,5 @@
 Require Import HoTT.Basics HoTT.Colimits.Pushout.
-Require Import Types.Paths.
+Require Import Types.Paths Types.Sigma Types.Prod HFiber Limits.Pullback.
 
 (** * Pushouts of "dependent spans". *)
 
@@ -121,3 +121,19 @@ Proof.
     2: apply spushout_rec_beta_spglue.
     apply H.
 Defined.
+
+(** Any pushout is equivalent to a span pushout. *)
+Definition equiv_pushout_spushout {X Y Z : Type} (f : X -> Y) (g : X -> Z)
+  : Pushout f g
+    <~> SPushout (fun (y : Y) (z : Z) => {x : X & f x = y /\ g x = z}).
+Proof.
+  snrapply equiv_pushout.
+  { nrefine (equiv_sigma_prod _ oE _).
+    apply equiv_double_fibration_replacement. }
+  1-4: reflexivity.
+Defined.
+
+(** There is a natural map from the total space of [Q] to the pushout product of [Q]. *)
+Definition spushout_sjoin_map {X Y : Type} (Q : X -> Y -> Type)
+  : {x : X & {y : Y & Q x y}} -> Pullback (spushl Q) (spushr Q)
+  := functor_sigma idmap (fun _ => functor_sigma idmap (fun _ => spglue Q)).
diff --git a/theories/HFiber.v b/theories/HFiber.v
index 0a1f4ae787d..663312a3e8f 100644
--- a/theories/HFiber.v
+++ b/theories/HFiber.v
@@ -142,29 +142,21 @@ Defined.
 Definition equiv_fibration_replacement  {B C} (f:C ->B)
   : C <~> {y:B & hfiber f y}.
 Proof.
-  snrefine (Build_Equiv _ _ _ (
-    Build_IsEquiv C {y:B & {x:C & f x = y}}
-      (fun c => (f c; (c; idpath)))
-      (fun c => c.2.1)
-      _
-      (fun c => idpath)
-       _)).
-  - intros [? [? []]]; reflexivity.
-  - reflexivity.
+  make_equiv_contr_basedpaths.
+Defined.
+
+(** This is a useful variant for taking a "double fiber" of two maps. *)
+Definition equiv_double_fibration_replacement
+  {X Y Z : Type} (f : X -> Y) (g : X -> Z)
+  : X <~> {y : Y & {z : Z & {x : X & f x = y /\ g x = z}}}.
+Proof.
+  make_equiv_contr_basedpaths.
 Defined.
 
 Definition hfiber_fibration {X} (x : X) (P:X->Type)
   : P x <~> @hfiber (sig P) X pr1 x.
 Proof.
-  snrefine (Build_Equiv _ _ _
-    (Build_IsEquiv (P x) { z : sig P & z.1 = x }
-      (fun Px => ((x; Px); idpath))
-      (fun Px => transport P Px.2 Px.1.2)
-      _
-      (fun Px => idpath)
-      _)).
-  - intros [[] []]; reflexivity.
-  - reflexivity.
+  make_equiv_contr_basedpaths.
 Defined.
 
 (** ** Exercise 4.4: The unstable octahedral axiom. *)
diff --git a/theories/HoTT.v b/theories/HoTT.v
index 840964f27e4..faad9332df8 100644
--- a/theories/HoTT.v
+++ b/theories/HoTT.v
@@ -151,7 +151,6 @@ Require Export HoTT.Homotopy.HomotopyGroup.
 Require Export HoTT.Homotopy.PinSn.
 Require Export HoTT.Homotopy.WhiteheadsPrinciple.
 Require Export HoTT.Homotopy.BlakersMassey.
-Require Export HoTT.Homotopy.Freudenthal.
 Require Export HoTT.Homotopy.Suspension.
 Require Export HoTT.Homotopy.Smash.
 Require Export HoTT.Homotopy.Wedge.
diff --git a/theories/Homotopy/BlakersMassey.v b/theories/Homotopy/BlakersMassey.v
index 0322aa91d30..558544119f7 100644
--- a/theories/Homotopy/BlakersMassey.v
+++ b/theories/Homotopy/BlakersMassey.v
@@ -1,6 +1,8 @@
-Require Import HoTT.Basics HoTT.Types.
+Require Import HoTT.Basics HoTT.Types HFiber.
 Require Import Colimits.Pushout.
 Require Import Colimits.SpanPushout.
+Require Import Homotopy.Suspension.
+Require Import Limits.Pullback.
 Require Import Homotopy.Join.Core.
 Require Import Truncations.
 
@@ -527,10 +529,10 @@ End GBM.
 (** ** The classical Blakers-Massey Theorem *)
 
 Global Instance blakers_massey `{Univalence} (m n : trunc_index)
-           {X Y : Type} (Q : X -> Y -> Type)
-           `{forall y, IsConnected m.+1 { x : X & Q x y } }
-           `{forall x, IsConnected n.+1 { y : Y & Q x y } }
-           (x : X) (y : Y)
+  {X Y : Type} (Q : X -> Y -> Type)
+  `{forall y, IsConnected m.+1 { x : X & Q x y } }
+  `{forall x, IsConnected n.+1 { y : Y & Q x y } }
+  (x : X) (y : Y)
   : IsConnMap (m +2+ n) (@spglue X Y Q x y).
 Proof.
   intros r.
@@ -539,3 +541,54 @@ Proof.
   1: intros; apply isconnected_join.
   all: exact _.
 Defined.
+
+(** A sigma functor is connected if its fibers are, so we have the following. *)
+Definition blakers_massey_total_map `{Univalence} (m n : trunc_index)
+  {X Y : Type} (Q : X -> Y -> Type)
+  `{forall y, IsConnected m.+1 { x : X & Q x y } }
+  `{forall x, IsConnected n.+1 { y : Y & Q x y } }
+  : IsConnMap (Tr (m +2+ n)) (spushout_sjoin_map Q)
+  := _.
+
+Definition blakers_massey_po `{Univalence} (m n : trunc_index)
+  {X Y Z : Type} (f : X -> Y) (g : X -> Z)
+  `{H1 : !IsConnMap n.+1 f} `{H2 : !IsConnMap m.+1 g}
+  : IsConnMap (m +2+ n) (pullback_corec (pglue (f:=f) (g:=g))).
+Proof.
+  (** We postcompose our map with an equivalence from the the pullback of the pushout of [f] and [g] to the pullback of an equivalent [SPushout] over a family [Q]. *)
+  pose (Q := fun y z => {x : X & f x = y /\ g x = z}).
+  snrapply cancelL_equiv_conn_map.
+  1: exact (Pullback (spushl Q) (spushr Q)).
+  1: by snrapply (equiv_pullback (equiv_pushout_spushout _ _)).
+  (** Next we precompose with the equivalence from the total space of [Q] to [X]. *)
+  rapply (cancelR_conn_map _ (equiv_double_fibration_replacement f g)^-1%equiv).
+  (** Next we prove that this composition is homotopic to [spushout_sjoin_map Q]. *)
+  snrapply (conn_map_homotopic _ (spushout_sjoin_map Q)).
+  { intros [y [z [x [[] []]]]].
+    snrapply (path_sigma' _ 1 (path_sigma' _ 1 _)); simpl; symmetry.
+    lhs nrapply concat_1p.
+    lhs nrapply concat_p1.
+    lhs nrapply functor_coeq_beta_cglue.
+    lhs nrapply concat_p1.
+    nrapply concat_1p. }
+  rapply blakers_massey_total_map.
+  (** What's left is to check that the partial total spaces of [Q] are connected, which we get since [f] and [g] are connected maps. We just have to strip off the irrelevant parts of [Q] to get the hfiber in each case. *)
+  - intros z.
+    nrefine (isconnected_equiv' _ _ _ (H2 z)).
+    make_equiv_contr_basedpaths.
+  - intros y.
+    nrefine (isconnected_equiv' _ _ _ (H1 y)).
+    make_equiv_contr_basedpaths.
+Defined.
+
+(** ** The Freudenthal Suspension Theorem *)
+
+(** The Freudenthal suspension theorem is a fairly trivial corollary of the Blakers-Massey theorem.  It says that [merid : X -> North = South] is highly connected. *)
+Global Instance freudenthal `{Univalence} (n : trunc_index)
+           (X : Type@{u}) `{IsConnected n.+1 X}
+  : IsConnMap (n +2+ n) (@merid X).
+Proof.
+  (* If we post-compose [merid : X -> North = South] with an equivalence [North = South <~> P], where [P] is the pullback of the inclusions [Unit -> Susp X] hitting [North] and [South], we get the canonical comparison map [X -> P] whose connectivity follows from the Blakers-Massey theorem. *)
+  rapply (cancelL_equiv_conn_map _ _ (equiv_pullback_unit_unit_paths _ _)^-1%equiv).
+  rapply blakers_massey_po.
+Defined.
diff --git a/theories/Homotopy/Cofiber.v b/theories/Homotopy/Cofiber.v
new file mode 100644
index 00000000000..c04ae028fea
--- /dev/null
+++ b/theories/Homotopy/Cofiber.v
@@ -0,0 +1,150 @@
+Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Basics.Equivalences.
+Require Import Types.Unit Types.Paths Types.Universe Types.Sigma.
+Require Import Truncations.Core Truncations.Connectedness.
+Require Import Colimits.Pushout Homotopy.Suspension.
+Require Import Homotopy.NullHomotopy.
+Require Import HFiber Limits.Pullback BlakersMassey.
+
+Set Universe Minimization ToSet.
+
+(** * Homotopy Cofibers *)
+
+(** ** Definition *)
+
+(** Homotopy cofibers or mapping cones are spaces constructed from a map [f : X -> Y] by contracting the image of [f] inside [Y] to a point. They can be thought of as a kind of coimage or quotient. *)
+
+Definition Cofiber {X Y : Type} (f : X -> Y)
+  := Pushout f (const_tt X).
+
+(** *** Constructors *)
+
+(** Any element of [Y] can be included in the cofiber. *)
+Definition cofib {X Y : Type} (f : X -> Y) : Y -> Cofiber f
+  := pushl.
+
+(** We have a distinguised point in the cofiber, where the image of [f] is contracted to. *)
+Definition cf_apex {X Y : Type} (f : X -> Y) : Cofiber f
+  := pushr tt.
+
+(** Given an element [x : X], we have the path [cfglue f x] from the [f x] to the [cf_apex]. *)
+Definition cfglue {X Y : Type} (f : X -> Y) (x : X) : cofib f (f x) = cf_apex f
+  := pglue _.
+
+(** *** Induction and recursion principles *)
+
+(** The recursion principle for the cofiber of [f : X -> Y] requires a function [g : Y -> Z] such that [g o f] is null homotopic, i.e. constant. *)
+Definition cofiber_rec {X Y Z : Type} (f : X -> Y) (g : Y -> Z)
+  (null : NullHomotopy (g o f))
+  : Cofiber f -> Z.
+Proof.
+  snrapply Pushout_rec.
+  - exact g.
+  - intros; exact null.1.
+  - intros a.
+    exact (null.2 a).
+Defined.
+
+(** The induction principle is similar, although requries a dependent form of null homotopy. *)
+Definition cofiber_ind {X Y : Type} (f : X -> Y) (P : Cofiber f -> Type)
+  (g : forall y, P (cofib f y))
+  (null : exists b, forall x, transport P (cfglue f x) (g (f x)) = b)
+  : forall x, P x.
+Proof.
+  snrapply Pushout_ind.
+  - intros y; apply g.
+  - intros []; exact null.1.
+  - exact null.2.
+Defined.
+
+(** ** Functoriality *)
+
+Local Close Scope trunc_scope.
+
+(** The homotopy cofiber can be thought of as a functor from the category of arrows in [Type] to [Type]. *)
+
+(** 1-functorial action. *)
+Definition functor_cofiber {X Y X' Y' : Type} {f : X -> Y} {f' : X' -> Y'}
+  (g : X -> X') (h : Y -> Y') (p : h o f == f' o g)
+  : Cofiber f -> Cofiber f'
+  := functor_pushout g h idmap p (fun _ => idpath).
+
+(** 2-functorial action. *)
+Definition functor_cofiber_homotopy {X Y X' Y' : Type} {f : X -> Y} {f' : X' -> Y'}
+  {g g' : X -> X'} {h h' : Y -> Y'} {p : h o f == f' o g} {p' : h' o f == f' o g'}
+  (u : g == g') (v : h == h') 
+  (r : forall x, p x @ ap f' (u x) = v (f x) @ p' x)
+  : functor_cofiber g h p == functor_cofiber g' h' p'.
+Proof.
+  snrapply (functor_pushout_homotopic u v (fun _ => 1) r).
+  intro x; exact (concat_1p _ @ ap_const _ _).
+Defined.
+
+(** The cofiber functor preserves the identity map. *) 
+Definition functor_cofiber_idmap {X Y : Type} (f : X -> Y)
+  : functor_cofiber (f:=f) idmap idmap (fun _ => 1) == idmap
+  := functor_pushout_idmap.
+
+(** The cofiber functor preserves composition of squares. (When mapping parallel edges). *)
+Definition functor_cofiber_compose {X Y X' Y' X'' Y'' : Type}
+  {f : X -> Y} {f' : X' -> Y'} {f'' : X'' -> Y''}
+  {g : X -> X'} {g' : X' -> X''} {h : Y -> Y'} {h' : Y' -> Y''}
+  (p : h o f == f' o g) (p' : h' o f' == f'' o g')
+  : functor_cofiber (g' o g) (h' o h) (fun x => ap h' (p x) @ p' (g x))
+    == functor_cofiber g' h' p' o functor_cofiber g h p
+  := functor_pushout_compose g h idmap g' h' idmap p (fun _ => 1) p' (fun _ => 1).
+
+Local Open Scope trunc_scope.
+
+(** ** Connectivity of cofibers *)
+
+(** The cofiber of an [n]-conencted map is [n.+1]-connected. *)
+Definition isconnnected_cofiber (n : trunc_index) {X Y : Type} (f : X -> Y)
+  {fc : IsConnMap n f}
+  : IsConnected n.+1 (Cofiber f).
+Proof.
+  apply isconnected_from_elim.
+  intros C H' g.
+  exists (g (cf_apex _)).
+  snrapply cofiber_ind.
+  - rapply (conn_map_elim n f).
+    intros x.
+    exact (ap g (cfglue f x)).
+  - exists idpath.
+    intros x.
+    lhs snrapply transport_paths_Fl.
+    apply moveR_Vp.
+    rhs nrapply concat_p1.
+    nrapply conn_map_comp.
+Defined.
+
+(** ** Comparison of fibers and cofibers *)
+
+Definition fiber_to_path_cofiber {X Y : Type} (f : X -> Y) (y : Y)
+  : hfiber f y -> cofib f y = cf_apex f.
+Proof.
+  intros [x p].
+  lhs_V nrapply (ap (cofib f) p).
+  apply cfglue.
+Defined.
+
+(** Blakers-Massey implies that the comparison map is highly connected. *)
+Definition isconnected_fiber_to_cofiber `{Univalence}
+  (n m : trunc_index) {X Y : Type} {ac : IsConnected m.+1 X}
+  (f : X -> Y) {fc : IsConnMap n.+1 f} (y : Y)
+  : IsConnMap (m +2+ n) (fiber_to_path_cofiber f y).
+Proof.
+  (* It's enough to check the connectivity of [functor_sigma idmap (fiber_to_path_cofiber f)]. *)
+  revert y; snrapply conn_map_fiber.
+  (* We precompose with the equivalence [X <~> { y : Y & hfiber f y }]. *)
+  rapply (cancelR_conn_map _ (equiv_fibration_replacement _)).
+  (* The Sigma-type [{ y : Y & cofib f y = cf_apex f}] in the codomain is the fiber of the map [cofib f], and so it is equivalent to the pullback of the cospan in the pushout square defining [Cofiber f].  We postcompose with this equivalence. *)
+  snrapply (cancelL_equiv_conn_map _ _ (equiv_pullback_unit_hfiber _ _)^-1%equiv).
+  (* The composite is homotopic to the map from [blakers_massey_po], with the only difference being an extra [1 @ _]. *)
+  snrapply conn_map_homotopic.
+  3: rapply blakers_massey_po.
+  (* Use [compute.] to see the details of the goal. *)
+  intros x.
+  apply (ap (fun z => (f x; tt; z))).
+  unfold fiber_to_path_cofiber; simpl.
+  symmetry; apply concat_1p.
+Defined.
diff --git a/theories/Homotopy/Freudenthal.v b/theories/Homotopy/Freudenthal.v
deleted file mode 100644
index 9fdcaa8173a..00000000000
--- a/theories/Homotopy/Freudenthal.v
+++ /dev/null
@@ -1,33 +0,0 @@
-Require Import Basics.
-Require Import Types.
-Require Import Colimits.Pushout.
-Require Import Colimits.SpanPushout.
-Require Import HoTT.Truncations.
-Require Import Homotopy.Suspension.
-Require Import Homotopy.BlakersMassey.
-
-(** * The Freudenthal Suspension Theorem *)
-
-(** The Freudenthal suspension theorem is a fairly trivial corollary of the Blakers-Massey theorem.  The only real work is to relate the span-pushout that we used for Blakers-Massey to the naive pushout that we used to define suspension. *)
-Local Definition freudenthal' `{Univalence} (n : trunc_index)
-           (X : Type) `{IsConnected n.+1 X}
-  : IsConnMap (n +2+ n) (@merid X).
-Proof.
-  snrapply cancelL_equiv_conn_map.
-  2: { refine (equiv_ap' (B:=SPushout (fun (u v : Unit) => X)) _ North South).
-       exact (equiv_pushout (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
-                            (equiv_idmap Unit) (equiv_idmap Unit)
-                            (fun x : X => idpath) (fun x : X => idpath)). }
-  refine (conn_map_homotopic _ _ _ _
-                             (blakers_massey n n (fun (u v:Unit) => X) tt tt)).
-  intros x.
-  refine (_ @ (equiv_pushout_pglue
-                 (equiv_contr_sigma (fun _ : Unit * Unit => X))^-1
-                 (equiv_idmap Unit) (equiv_idmap Unit)
-                 (fun x : X => idpath) (fun x : X => idpath) x)^).
-  exact ((concat_p1 _ @ concat_1p _)^).
-Defined.
-
-Definition freudenthal@{u v | u < v} := Eval unfold freudenthal' in @freudenthal'@{u u u u u v u u u u u}.
-
-Global Existing Instance freudenthal.
diff --git a/theories/Limits/Pullback.v b/theories/Limits/Pullback.v
index 5269280dad7..4e60bf2383d 100644
--- a/theories/Limits/Pullback.v
+++ b/theories/Limits/Pullback.v
@@ -91,14 +91,30 @@ Defined.
 Definition equiv_pullback_unit_prod (A B : Type)
 : Pullback (const_tt A) (const_tt B) <~> A * B.
 Proof.
-  simple refine (equiv_adjointify _ _ _ _).
-  - intros [a [b _]]; exact (a , b).
-  - intros [a b]; exact (a ; b ; 1).
-  - intros [a b]; exact 1.
-  - intros [a [b p]]; simpl.
-    apply (path_sigma' _ 1); simpl.
-    apply (path_sigma' _ 1); simpl.
-    apply path_contr.
+  refine (equiv_sigma_prod0 A B oE _).
+  snrapply equiv_functor_sigma_id; intro a; cbn.
+  rapply equiv_sigma_contr.
+Defined.
+
+(** Pullback of [Unit] is equivalent to [hfiber]. *)
+Definition equiv_pullback_unit_hfiber {A B : Type} (f : A -> B) (g : Unit -> B)
+  : Pullback f g <~> hfiber f (g tt).
+Proof.
+  snrapply equiv_functor_sigma_id; intro a; cbn.
+  exact (equiv_contr_sigma (fun c => _ = g c)).
+Defined.
+
+(** The same for the symmetrical pullback. *)
+Definition equiv_pullback_unit_hfiber' {A B : Type} (f : Unit -> B) (g : A -> B)
+  : Pullback f g <~> hfiber g (f tt)
+  := equiv_pullback_unit_hfiber _ _ oE equiv_pullback_symm _ _.
+
+(** When both corners are [Unit] you get the path type. *)
+Definition equiv_pullback_unit_unit_paths {B : Type} (f g : Unit -> B)
+  : Pullback f g <~> (f tt = g tt).
+Proof.
+  refine (_ oE equiv_contr_sigma _).
+  exact (equiv_contr_sigma (fun c => _ = g c)).
 Defined.
 
 (** The property of a given commutative square being a pullback *)
diff --git a/theories/Pointed/pSusp.v b/theories/Pointed/pSusp.v
index b1d302e691c..bf5dc6e16ca 100644
--- a/theories/Pointed/pSusp.v
+++ b/theories/Pointed/pSusp.v
@@ -5,7 +5,7 @@ Require Import Pointed.Loops.
 Require Import Pointed.pTrunc.
 Require Import Pointed.pEquiv.
 Require Import Homotopy.Suspension.
-Require Import Homotopy.Freudenthal.
+Require Import Homotopy.BlakersMassey.
 Require Import Truncations.
 Require Import WildCat.