diff --git a/theories/Constant.v b/theories/Constant.v
index 56661d475c6..10cbc450f2a 100644
--- a/theories/Constant.v
+++ b/theories/Constant.v
@@ -180,3 +180,33 @@ Proof.
     + cbn. funext x y.
       pose (Ys x); apply path_ishprop.
 Defined.
+
+(** We can use the above to give a funext-free approach to defining a map by factoring through a surjection. *)
+
+Section SurjectiveFactor.
+  Context {A B C : Type} `{IsHSet C} (f : A -> C) (g : A -> B)
+    (resp : forall x y, g x = g y -> f x = f y).
+
+  (** The assumption [resp] tells us that [f o pr1] is weakly constant on each fiber of [g], so it factors through the propositional truncation. *)
+  Definition surjective_factor_aux (b : B) : merely (hfiber g b) -> C.
+  Proof.
+    rapply (merely_rec_hset (f o pr1)).
+    intros [x p] [y q]; cbn.
+    exact (resp x y (p @ q^)).
+  Defined.
+
+  (** When [g] is surjective, those propositional truncations are contractible, giving us a way to get an element of [C]. *)
+  Definition surjective_factor `{IsSurjection g} : B -> C.
+  Proof.
+    intro b.
+    exact (surjective_factor_aux b (center _)).
+  Defined.
+
+  Definition surjective_factor_factors `{IsSurjection g}
+    : surjective_factor o g == f.
+  Proof.
+    intros a; unfold surjective_factor.
+    exact (ap (surjective_factor_aux (g a)) (contr (tr (a; idpath)))).
+  Defined.
+
+End SurjectiveFactor.
diff --git a/theories/HIT/surjective_factor.v b/theories/HIT/surjective_factor.v
deleted file mode 100644
index d3b0d5c46cd..00000000000
--- a/theories/HIT/surjective_factor.v
+++ /dev/null
@@ -1,36 +0,0 @@
-Require Import
-        HoTT.Basics
-        HoTT.Truncations.Core Modalities.Modality.
-
-(** Definition by factoring through a surjection. *)
-
-Section surjective_factor.
-  Context `{Funext}.
-  Context {A B C} `{IsHSet C} `(f : A -> C) `(g : A -> B) {Esurj : IsSurjection g}.
-  Variable (Eg : forall x y, g x = g y -> f x = f y).
-
-  Lemma ishprop_surjective_factor_aux : forall b, IsHProp (exists c : C, forall a, g a = b -> f a = c).
-  Proof.
-    intros. apply Sigma.ishprop_sigma_disjoint.
-    intros c1 c2 E1 E2.
-    generalize (@center _ (Esurj b)); apply (Trunc_ind _).
-    intros [a p];destruct p.
-    path_via (f a).
-  Qed.
-
-  Definition surjective_factor_aux :=
-    @conn_map_elim
-      _ _ _ _ Esurj (fun b => exists c : C, forall a, g a = b -> f a = c)
-      ishprop_surjective_factor_aux
-      (fun a => exist (fun c => forall a, _ -> _ = c) (f a) (fun a' => Eg a' a)).
-
-  Definition surjective_factor : B -> C
-    := fun b => (surjective_factor_aux b).1.
-
-  Lemma surjective_factor_pr : f == compose surjective_factor g.
-  Proof.
-    intros a.
-    apply (surjective_factor_aux (g a)).2. trivial.
-  Qed.
-
-End surjective_factor.
diff --git a/theories/HoTT.v b/theories/HoTT.v
index faad9332df8..fd8eea3db9f 100644
--- a/theories/HoTT.v
+++ b/theories/HoTT.v
@@ -52,7 +52,6 @@ Require Export HoTT.HIT.epi.
 Require Export HoTT.HIT.unique_choice.
 Require Export HoTT.HIT.iso.
 Require Export HoTT.HIT.quotient.
-Require Export HoTT.HIT.surjective_factor.
 Require Export HoTT.HIT.V.
 
 Require Export HoTT.Diagrams.Graph.