diff --git a/UniMath/CategoryTheory/Chains/OmegaContPolynomialFunctors.v b/UniMath/CategoryTheory/Chains/OmegaContPolynomialFunctors.v
new file mode 100644
index 0000000000..ac3363f51f
--- /dev/null
+++ b/UniMath/CategoryTheory/Chains/OmegaContPolynomialFunctors.v
@@ -0,0 +1,291 @@
+(** ** Polynomial Functors are omega-continuous
+
+    Author : Antoine Fisse (@AextraT), 2025
+*)
+
+Require Import UniMath.Foundations.PartD.
+Require Import UniMath.Foundations.Sets.
+Require Import UniMath.MoreFoundations.All.
+
+Require Import UniMath.Induction.FunctorCoalgebras_legacy.
+Require Import UniMath.Induction.PolynomialFunctors.
+Require Import UniMath.Induction.M.Core.
+Require Import UniMath.Induction.M.MWithSets.
+
+Require Import UniMath.CategoryTheory.Categories.Type.Core.
+Require Import UniMath.CategoryTheory.Core.Categories.
+Require Import UniMath.CategoryTheory.Core.Functors.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+Require Import UniMath.CategoryTheory.Chains.CoAdamek.
+Require Import UniMath.CategoryTheory.Chains.Chains.
+Require Import UniMath.CategoryTheory.Chains.Cochains.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.FunctorCoalgebras.
+
+Local Open Scope cat.
+Local Open Scope functions.
+
+Section OmegaContinuity.
+
+  Context {A : ob HSET} (B : pr1hSet A → ob HSET).
+
+  Definition F' := MWithSets.F' B.
+
+  Lemma comp_right_eq_hset
+    {X Y Z : UU}
+    {f g : X -> Y}
+    (h : Y -> Z)
+    (p : f = g)
+    : h ∘ f = h ∘ g.
+  Proof.
+    use funextfun.
+    apply homotfun.
+    induction p.
+    apply homotrefl.
+  Qed.
+
+  Lemma rev_proof {X : UU} {x y : X} (q : x = y) : y = x.
+  Proof.
+    symmetry. apply q.
+  Defined.
+
+
+  Lemma pullback_cone_edge
+    {X Y0 Y1 Y2: SET}
+    (x : pr1hSet X)
+    {f : SET ⟦ Y1, Y2 ⟧}
+    {g0 : SET ⟦ X, F' Y0 ⟧}
+    {g1 : SET ⟦ X, F' Y1 ⟧}
+    {g2 : SET ⟦ X, F' Y2 ⟧}
+    (p : (#F' f) ∘ g1 = g2)
+    (q1 : pr1 ∘ g0 = pr1 ∘ g1)
+    (q2 : pr1 ∘ g0 = pr1 ∘ g2)
+    : (λ b, f (pr2 (g1 x) (transportf (λ φ, pr1hSet (B (φ x))) q1 b))) = (λ b, pr2 (g2 x) (transportf (λ φ, pr1hSet (B (φ x))) q2 b)).
+  Proof.
+    induction p.
+    cbn.
+    assert (r : q1 = q2).
+    { apply (setproperty (SET ⟦ X, A ⟧,, isaset_forall_hSet (pr1hSet X) (λ _, A)) (pr1 ∘ g0) (pr1 ∘ g1)).
+    }
+    induction r.
+    apply idpath.
+  Defined.
+
+  Lemma pathtozero_cone
+    {c0 : SET}
+    {c : cochain SET}
+    (cc0 : Graphs.Limits.cone (Diagrams.mapdiagram F' c) c0)
+    (v : nat)
+    : pr1 ∘ (pr1 cc0 0) = pr1 ∘ (pr1 cc0 v).
+  Proof.
+    induction v.
+    - apply idpath.
+    - symmetry.
+      etrans.
+      + apply (comp_right_eq_hset (λ x : pr1hSet (F' (Diagrams.dob c v)), pr1 x) (pr2 cc0 (S v) v (idpath (S v)))).
+      + symmetry. apply IHv.
+  Defined.
+
+  Lemma pullback_cone
+    {c0 : SET}
+    (x : pr1hSet c0)
+    {c : cochain SET}
+    (cc0 : Graphs.Limits.cone (Diagrams.mapdiagram F' c) c0)
+    : Graphs.Limits.cone c (B (pr1 (pr1 cc0 0 x))).
+  Proof.
+    unfold Graphs.Limits.cone.
+    unfold Graphs.Limits.cone in cc0.
+    unfold Limits.forms_cone in cc0.
+    set (f := λ v : Diagrams.vertex conat_graph, (λ b, pr2 (pr1 cc0 v x) (transportf (λ φ, pr1hSet (B (φ x))) (pathtozero_cone cc0 v) b)) : SET ⟦ B (pr1 (pr1 cc0 0 x)), Diagrams.dob c v ⟧).
+    assert (p : Limits.forms_cone c f).
+    {
+      unfold Limits.forms_cone.
+      simpl.
+      intros u v e.
+      induction e.
+      set (p := pullback_cone_edge x (pr2 cc0 (S v) v (idpath (S v))) (pathtozero_cone cc0 (S v)) (pathtozero_cone cc0 v)).
+      apply p.
+    }
+    exact (f,, p).
+  Defined.
+
+  Lemma Exists_fun_mapdiagram
+    {c : cochain SET}
+    {L : SET}
+    {cc : Graphs.Limits.cone c L}
+    (c_limcone : Graphs.Limits.isLimCone c L cc)
+    (c0 : SET)
+    (cc0 : Graphs.Limits.cone (Diagrams.mapdiagram F' c) c0)
+    : SET ⟦ c0, F' L ⟧.
+  Proof.
+    intro x.
+    cbn.
+    unfold polynomial_functor_obj.
+    set (a := pr1 (pr1 cc0 0 x) : pr1hSet A).
+    set (cx := B a).
+    set (ccx := pullback_cone x cc0).
+    set (f2x := pr11 (c_limcone cx ccx)).
+    exact (a,, f2x).
+  Defined.
+
+  Lemma is_mor_mapdiagram2_point
+    {X Y c : UU}
+    (x : X)
+    {φ1 φ2 : X -> pr1hSet A}
+    {f : pr1hSet (B (φ1 x)) -> c}
+    {g : c -> Y}
+    {h : pr1hSet (B (φ2 x)) -> Y}
+    (q : φ1 = φ2)
+    (p : g ∘ f = λ b, h (transportf (λ ψ, pr1hSet (B (ψ x))) q b))
+    : transportf (λ a, pr1hSet (B a) -> Y) (toforallpaths _ _ _ q x) (g ∘ f) = h.
+  Proof.
+    induction q.
+    apply p.
+  Defined.
+
+  Lemma Exists_mor_mapdiagram
+    {c : cochain SET}
+    {L : SET}
+    {cc : Graphs.Limits.cone c L}
+    (c_limcone : Graphs.Limits.isLimCone c L cc)
+    (c0 : SET)
+    (cc0 : Graphs.Limits.cone (Diagrams.mapdiagram F' c) c0)
+    : ∑ f : SET ⟦ c0, F' L ⟧, Limits.is_cone_mor cc0 (Limits.mapcone F' c cc) f.
+  Proof.
+    set (f := Exists_fun_mapdiagram c_limcone c0 cc0).
+    assert (p : Limits.is_cone_mor cc0 (Limits.mapcone F' c cc) f).
+    {
+      unfold Limits.is_cone_mor.
+      intro v.
+      apply funextfun.
+      intro x.
+      use total2_paths_f.
+      - unfold Graphs.Limits.coneOut.
+        unfold Limits.mapcone.
+        cbn.
+        apply (toforallpaths _ _ _ (pathtozero_cone cc0 v) x).
+      - cbn.
+        unfold Graphs.Limits.coneOut.
+        set (a := pr1 (pr1 cc0 0 x) : pr1hSet A).
+        set (cx := B a).
+        set (ccx := pullback_cone x cc0).
+        set (p := pr2 (pr1 (c_limcone cx ccx)) v).
+        cbn in p.
+        unfold Graphs.Limits.coneOut in p.
+        apply (is_mor_mapdiagram2_point x (pathtozero_cone cc0 v) p).
+    }
+    exact (f,, p).
+  Defined.
+
+  Lemma move_proof
+    {X Y Z : SET}
+    {x : pr1hSet X}
+    (h1 h2 : SET⟦ X, A ⟧)
+    (f : SET ⟦ B (h2 x), Y ⟧)
+    (g : SET ⟦ Y, Z ⟧ )
+    (q : h1 = h2)
+    : g ∘ (transportf (λ a, SET ⟦ B a, Y ⟧) (rev_proof (toforallpaths _ _ _ q x)) f) = λ b, g (f (transportf (λ φ, pr1hSet (B (φ x))) q b)).
+  Proof.
+    induction q.
+    cbn.
+    apply idpath.
+  Defined.
+
+  Lemma proj_is_cone_mor_point
+    {X Y Z0 Z : SET}
+    (x : pr1hSet X)
+    {f : SET ⟦ X, F' Y ⟧}
+    {g : SET⟦ Y, Z ⟧}
+    (h0 : SET⟦ X, F' Z0 ⟧)
+    (h1 : SET⟦ X, F' Z ⟧)
+    (p : #F' g ∘ f = h1)
+    (q : pr1 (f x) = pr1 (h0 x))
+    (q' : pr1 ∘ h0 = pr1 ∘ h1)
+    : g ∘ (transportf _ q (pr2 (f x))) = λ b, (pr2 (h1 x)) (transportf (λ φ, pr1hSet (B (φ x))) q' b).
+  Proof.
+    induction p.
+    cbn.
+    set (q'x := toforallpaths _ _ _ q' x).
+    cbn in q'x.
+    set (q'x' := rev_proof q'x).
+    assert (r : q'x' = q) by apply (setproperty A).
+    induction r.
+    apply (move_proof (pr1 ∘ h0) (pr1 ∘ # F' g ∘ f) (pr2 (f x)) g q').
+  Defined.
+
+  Lemma proj_is_cone_mor
+    {c : cochain SET}
+    {c0 L : SET}
+    {x : pr1hSet c0}
+    {cc :  Graphs.Limits.cone c L}
+    {cc0 : Graphs.Limits.cone (Diagrams.mapdiagram F' c) c0}
+    (f : SET ⟦ c0, F' L ⟧)
+    {p : pr1 (f x) = pr1 (pr1 cc0 0 x)}
+    (pf : Limits.is_cone_mor cc0 (Limits.mapcone F' c cc) f)
+    : Limits.is_cone_mor (pullback_cone x cc0) cc (transportf _ p (pr2 (f x))).
+  Proof.
+    set (ccx := pullback_cone x cc0).
+    cbn.
+    unfold Limits.is_cone_mor.
+    intro v.
+    unfold Limits.is_cone_mor in pf.
+    unfold Graphs.Limits.coneOut in pf.
+    apply (proj_is_cone_mor_point x (pr1 cc0 0) (pr1 cc0 v) (pf v) p (pathtozero_cone cc0 v)).
+  Defined.
+
+  Lemma morph_unicity_pushout
+    {c : cochain SET}
+    {c0 L : SET}
+    {cc : Graphs.Limits.cone c L}
+    (c_limcone : Graphs.Limits.isLimCone c L cc)
+    (cc0 : Graphs.Limits.cone (Diagrams.mapdiagram F' c) c0)
+    {f' : SET⟦ c0, F' L ⟧}
+    (pf' : Limits.is_cone_mor cc0 (Limits.mapcone F' c cc) f')
+    : f' = pr1 (Exists_mor_mapdiagram c_limcone c0 cc0).
+  Proof.
+    set (f_pf := Exists_mor_mapdiagram c_limcone c0 cc0).
+    set (f := pr1 f_pf).
+    set (pf := pr2 f_pf).
+    apply funextfun.
+    intro x.
+    set (p := maponpaths (λ z, pr1 z) (toforallpaths _ _ _ (pf' 0) x)).
+    use total2_paths_f.
+    - unfold Limits.is_cone_mor in pf'.
+      unfold Limits.mapcone in pf'.
+      unfold Graphs.Limits.coneOut in pf'.
+      cbn in pf'.
+      apply p.
+    - cbn.
+      set (a := pr1 (pr1 cc0 0 x) : pr1hSet A).
+      set (cx := B a).
+      set (ccx := pullback_cone x cc0).
+      set (f'2 := transportf _ p (pr2 (f' x)) : SET ⟦ cx, L ⟧).
+      set (f'2_cone_mor := proj_is_cone_mor f' pf' : Limits.is_cone_mor ccx cc f'2).
+      apply (maponpaths (λ z, pr1 z) (pr2 (c_limcone cx ccx) (f'2,, f'2_cone_mor))).
+  Defined.
+
+  Lemma F'_omega_cont : is_omega_cont F'.
+  Proof.
+    unfold is_omega_cont.
+    unfold Limits.preserves_limit.
+    unfold Graphs.Limits.isLimCone.
+    intros c L cc c_limcone c0 cc0.
+    use tpair.
+    - exact (Exists_mor_mapdiagram c_limcone c0 cc0).
+    - set (f_pf := Exists_mor_mapdiagram c_limcone c0 cc0).
+      set (f := pr1 f_pf).
+      set (pf := pr2 f_pf).
+      intro t.
+      destruct t as [f' pf'].
+      use total2_paths_f.
+      + apply (morph_unicity_pushout c_limcone cc0 pf').
+      + set (p1 := morph_unicity_pushout c_limcone cc0 pf').
+        set (tpf' := transportf (Limits.is_cone_mor cc0 (Limits.mapcone F' c cc)) p1 pf').
+        unfold Limits.is_cone_mor in pf.
+        use funextsec.
+        intro v.
+        apply (isaset_forall_hSet (pr1hSet c0) (λ _, F' (Diagrams.dob c v))).
+  Defined.
+
+End OmegaContinuity.
diff --git a/UniMath/Induction/M/BinaryBooleanMTrees.v b/UniMath/Induction/M/BinaryBooleanMTrees.v
new file mode 100644
index 0000000000..6f990673f9
--- /dev/null
+++ b/UniMath/Induction/M/BinaryBooleanMTrees.v
@@ -0,0 +1,124 @@
+(** ** Exemple of construction of M Types using ComputationalMWithSets
+
+    Author : Antoine Fisse (@AextraT), 2025
+*)
+
+Require Import UniMath.Foundations.PartD.
+Require Import UniMath.Foundations.Sets.
+Require Import UniMath.MoreFoundations.All.
+
+Require Import UniMath.Combinatorics.Lists.
+Require Import UniMath.Combinatorics.StandardFiniteSets.
+
+Require Import UniMath.Induction.FunctorCoalgebras_legacy.
+Require Import UniMath.Induction.PolynomialFunctors.
+Require Import UniMath.Induction.M.Core.
+Require Import UniMath.Induction.M.ComputationalM.
+Require Import UniMath.Induction.M.ComputationalMWithSets.
+Require Import UniMath.Induction.M.MWithSets.
+Require Import UniMath.Induction.M.FinalCoalgebraHSET.
+
+Require Import UniMath.CategoryTheory.Categories.Type.Core.
+Require Import UniMath.CategoryTheory.Core.Categories.
+Require Import UniMath.CategoryTheory.Core.Functors.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Chains.OmegaContPolynomialFunctors.
+Require UniMath.CategoryTheory.FunctorCoalgebras.
+
+Local Open Scope cat.
+
+Local Definition A := setcoprod unitset boolset.
+Local Definition B : pr1hSet A -> SET :=
+  λ a, match a with
+       | ii1 _ => emptyset
+       | ii2 _ => setcoprod unitset unitset
+       end.
+
+Local Definition F := MWithSets.F B.
+Local Definition F' := MWithSets.F' B.
+
+(* The final coalgebra obtained corresponds to the type of possibly infinite binary trees labeled with booleands. *)
+Local Definition C' := pr1 (GetMType_HSET B).
+Local Definition C'_isfinal := pr2 (GetMType_HSET B).
+
+Local Definition C'1 := ComputationalMWithSets.C' B C' C'_isfinal.
+Local Definition C'1_isfinal : isTerminal (CoAlg_category F') C'1 := ComputationalMWithSets.finalC' B C' C'_isfinal.
+Local Definition corec_C1 := ComputationalMWithSets.corecC B C' C'_isfinal.
+Local Definition c1 := pr11 C'1.
+Local Definition destr_c1 := pr2 C'1.
+
+Lemma Get_list_at_depth (t : c1) (depth : nat) : list bool.
+Proof.
+  assert (l : list c1). (* List of subtrees at given depth *)
+  {
+    induction depth.
+    - exact (cons t nil).
+    - exact (list_ind
+               (λ _, list c1)
+               nil
+               (λ t0 _ acc, match destr_c1 t0 with
+                            | (ii1 _,, _) => acc
+                            | (ii2 _,, f) => cons (f (ii1 tt)) (cons (f (ii2 tt)) acc)
+                            end)
+               IHdepth).
+  }
+  exact (list_ind
+           (λ _, list bool)
+           nil
+           (λ t0 _ acc, match destr_c1 t0 with
+                        | (ii1 _,, _) => acc
+                        | (ii2 b,, _) => cons b acc
+                        end)
+           l).
+Defined.
+
+(* Full tree only labeled true *)
+Definition t0 : c1.
+Proof.
+  set (c := unit).
+  set (s_c := λ _ : c, (ii2 true,, λ _, tt) : F c).
+  exact (corec_C1 (c,, s_c) tt).
+Defined.
+
+Lemma only_true : Get_list_at_depth t0 4 = functionToList 16 (λ _, true).
+Proof.
+  apply idpath.
+Defined.
+
+(*       true
+        /    \
+     false   true
+    /       /    \
+  true   true   false
+*)
+Definition t1 : c1.
+Proof.
+  set (c := nat).
+  set (a0 := ii2 true : A).
+  set (a1 := ii2 false : A).
+  set (a2 := ii2 true : A).
+  set (s_c := λ x : c, match x with
+                       | 0 => (a0,, λ y : pr1hSet (B a0), match y with
+                                                         | ii1 _ => 1
+                                                         | ii2 _ => 2
+                                                         end : c)
+                       | 1 => (a1,, λ y : pr1hSet (B a1), match y with
+                                                         | ii1 _ => 3
+                                                         | ii2 _ => 5
+                                                         end : c)
+                       | 2 => (a2,, λ y : pr1hSet (B a2), match y with
+                                                        | ii1 _ => 3
+                                                        | ii2 _ => 4
+                                                        end : c)
+                       | 3 => (ii2 true,, λ _, 5)
+                       | 4 => (ii2 false,, λ _, 5)
+                       | _ => (ii1 tt,, λ _, 5)
+                       end : F c).
+  exact (corec_C1 (c,, s_c) 0).
+Defined.
+
+Lemma row2 : Get_list_at_depth t1 2 = cons true (cons true (cons false nil)).
+Proof.
+  apply idpath.
+Defined.
diff --git a/UniMath/Induction/M/ComputationalMWithSets.v b/UniMath/Induction/M/ComputationalMWithSets.v
new file mode 100644
index 0000000000..647642e44f
--- /dev/null
+++ b/UniMath/Induction/M/ComputationalMWithSets.v
@@ -0,0 +1,62 @@
+(** ** Refinement of M-Types in the case of sets
+
+    Author : Antoine Fisse (@AextraT), 2025
+
+ *)
+
+Require Import UniMath.Foundations.PartD.
+Require Import UniMath.Foundations.Sets.
+Require Import UniMath.MoreFoundations.All.
+
+Require Import UniMath.Induction.FunctorCoalgebras_legacy.
+Require Import UniMath.Induction.PolynomialFunctors.
+Require Import UniMath.Induction.M.Core.
+Require Import UniMath.Induction.M.ComputationalM.
+Require Import UniMath.Induction.M.MWithSets.
+
+Require Import UniMath.CategoryTheory.Categories.Type.Core.
+Require Import UniMath.CategoryTheory.Core.Categories.
+Require Import UniMath.CategoryTheory.Core.Functors.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require UniMath.CategoryTheory.FunctorCoalgebras.
+
+Local Open Scope cat.
+
+Section Upstream.
+
+  Context {A : ob HSET} (B : pr1hSet A → ob HSET).
+
+  Local Definition F := MWithSets.F B.
+  Local Definition F' := MWithSets.F' B.
+
+  Context (C0' : UniMath.CategoryTheory.FunctorCoalgebras.coalgebra_ob F') (C0'_is_final : isTerminal (UniMath.CategoryTheory.FunctorCoalgebras.CoAlg_category F') C0').
+
+  Local Definition c0' : hSet :=  UniMath.CategoryTheory.FunctorCoalgebras.coalg_carrier F' C0'.
+
+  Local Definition C0 : coalgebra F := MWithSets.C0 B C0'.
+  Local Definition finalC0 : is_final C0 := MWithSets.C0_is_final B C0' C0'_is_final.
+
+  Local Definition C : coalgebra F := ComputationalM.M (pr1 A) (λ a, pr1 (B a)) C0 finalC0.
+  Local Definition finalC : is_final C := finalM (pr1 A) (λ a, pr1 (B a)) C0 finalC0.
+  Local Definition c : type_precat := coalgebra_ob F C.
+  Local Definition s_c := coalgebra_mor F C.
+
+  Lemma c_isaset : isaset c.
+  Proof.
+    cbn.
+    unfold carrierM.
+    apply (isaset_total2_hSet c0' (λ m0, hProp_to_hSet (∃ (C : coalgebra F) (c : coalgebra_ob F C), (pr11 (finalC0 C)) c = m0))).
+  Defined.
+
+  Local Definition C' := MWithSets.C0' B C c_isaset.
+  Local Definition finalC' := MWithSets.C0'_is_final B C c_isaset finalC.
+
+  Local Definition corecC := ComputationalM.corecM (pr1 A) (λ a, pr1 (B a)) C0 finalC0.
+
+  Lemma corec_computation_set C1 c1 : s_c (corecC C1 c1) = # F (corecC C1) (pr2 C1 c1).
+  Proof.
+    apply idpath.
+  Defined.
+
+End Upstream.
diff --git a/UniMath/Induction/M/FinalCoalgebraHSET.v b/UniMath/Induction/M/FinalCoalgebraHSET.v
new file mode 100644
index 0000000000..5b0add4c44
--- /dev/null
+++ b/UniMath/Induction/M/FinalCoalgebraHSET.v
@@ -0,0 +1,72 @@
+(** ** A final coalgebra of a polynomial functor defined by sets is a set.
+
+    Author : Antoine Fisse (@AextraT), 2025
+ *)
+
+Require Import UniMath.Foundations.PartD.
+Require Import UniMath.Foundations.Sets.
+Require Import UniMath.MoreFoundations.All.
+
+Require Import UniMath.Induction.FunctorCoalgebras_legacy.
+Require Import UniMath.Induction.PolynomialFunctors.
+Require Import UniMath.Induction.M.Core.
+Require Import UniMath.Induction.M.MWithSets.
+Require Import UniMath.Induction.M.Uniqueness.
+
+Require Import UniMath.CategoryTheory.Categories.Type.Core.
+Require Import UniMath.CategoryTheory.Core.Categories.
+Require Import UniMath.CategoryTheory.Core.Functors.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+Require Import UniMath.CategoryTheory.Chains.CoAdamek.
+Require Import UniMath.CategoryTheory.Chains.Chains.
+Require Import UniMath.CategoryTheory.Chains.Cochains.
+Require Import UniMath.CategoryTheory.Chains.OmegaContPolynomialFunctors.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.FunctorCoalgebras.
+
+Local Open Scope cat.
+Local Open Scope functions.
+
+Section MTypesAreSets.
+
+  Context {A : ob HSET} (B : pr1hSet A → ob HSET).
+
+  Local Definition F := MWithSets.F B.
+
+  Lemma SET_terminal : Terminal SET.
+  Proof.
+    unfold Terminal.
+    assert (p : isTerminal SET unitHSET).
+    {
+      unfold isTerminal.
+      cbn.
+      intro a.
+      use tpair.
+      - exact (λ _, tt).
+      - intro t.
+        apply funextfun.
+        intro x.
+        apply isapropunit.
+    }
+    exact (unitHSET,, p).
+  Defined.
+
+  Lemma GetMType_HSET : Terminal (CoAlg_category (OmegaContPolynomialFunctors.F' B)).
+  Proof.
+    exact (limCoAlgTerminal SET_terminal (F'_omega_cont B) (LimConeHSET _ (termCochain SET_terminal (OmegaContPolynomialFunctors.F' B)))).
+  Defined.
+
+  Lemma F'CoalgAreSets (C : coalgebra F) (C_isfinal : is_final C) : isaset (pr1 C).
+  Proof.
+    set (C1'_t := GetMType_HSET).
+    unfold Terminal in C1'_t.
+    destruct C1'_t as [C1' C1'_isterm].
+    set (C1 := MWithSets.C0 B C1').
+    set (C1_isfinal := C0_is_final B C1' C1'_isterm : is_final C1).
+    set (p := M_carriers_eq (pr1hSet A) (λ a, pr1hSet (B a)) (C1,, C1_isfinal) (C,, C_isfinal) : pr1 C1 = pr1 C).
+    set (C1_isaset := pr21 C1' : isaset (pr1 C1)).
+    apply (transportf (λ c, isaset c) p C1_isaset).
+  Defined.
+
+End MTypesAreSets.
diff --git a/UniMath/Induction/M/MWithSets.v b/UniMath/Induction/M/MWithSets.v
new file mode 100644
index 0000000000..940322ea4b
--- /dev/null
+++ b/UniMath/Induction/M/MWithSets.v
@@ -0,0 +1,215 @@
+(** ** Equivalence between being a final coalgebra in UU and in HSET
+
+    Authors : Antoine Fisse (@AextraT), Ralph Matthes (@rmatthes), 2025
+
+ *)
+
+Require Import UniMath.Foundations.PartD.
+Require Import UniMath.Foundations.Sets.
+Require Import UniMath.MoreFoundations.All.
+
+Require Import UniMath.Induction.FunctorCoalgebras_legacy.
+Require Import UniMath.Induction.PolynomialFunctors.
+Require Import UniMath.Induction.SetBasedPolynomialFunctors.
+Require Import UniMath.Induction.M.Core.
+
+Require Import UniMath.CategoryTheory.Categories.Type.Core.
+Require Import UniMath.CategoryTheory.Core.Categories.
+Require Import UniMath.CategoryTheory.Core.Functors.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require UniMath.CategoryTheory.FunctorCoalgebras.
+
+Local Open Scope cat.
+
+Section M.
+  Context {A : ob HSET} (B : pr1hSet A → ob HSET).
+
+  Local Definition F : type_precat ⟶ type_precat := polynomial_functor (pr1hSet A) (fun a => pr1hSet (B a)).
+
+  Local Definition F' : functor HSET HSET := polynomial_functor_HSET A B.
+
+  Definition FromCoalgInHSET (C' : FunctorCoalgebras.CoAlg_category F') : coalgebra F.
+  Proof.
+    use tpair.
+    - exact (pr1hSet (FunctorCoalgebras.coalg_carrier F' C')).
+    - exact (FunctorCoalgebras.coalg_map F' C').
+  Defined.
+
+  Definition ToCoalgInHSET (C : coalgebra F) : isaset (coalgebra_ob F C) -> FunctorCoalgebras.CoAlg_category F'.
+  Proof.
+    intro Hyp.
+    use tpair.
+    - exact (coalgebra_ob F C ,, Hyp).
+    - exact (coalgebra_mor F C).
+  Defined.
+
+  Section ToFinalInHSET.
+
+  Context (C0 : coalgebra F).
+
+  Local Definition c0 : type_precat := coalgebra_ob F C0.
+
+  Context (c0_isaset : isaset c0).
+
+  Definition C0' : FunctorCoalgebras.coalgebra_ob F'.
+  Proof.
+    exact (ToCoalgInHSET C0 c0_isaset).
+  Defined.
+
+  Context (C0_is_final : is_final C0).
+
+  Lemma C0'_is_final : isTerminal (FunctorCoalgebras.CoAlg_category F') C0'.
+  Proof.
+    intro C'.
+    destruct (C0_is_final (FromCoalgInHSET C')) as [[φ p2] isunique].
+    cbn in φ.
+    use tpair.
+    - use tpair.
+      + exact φ.
+      + change (pr2 C' -->[φ] pr2 C0').
+        exact p2.
+    - intro ψ.
+      apply isunique.
+  Defined.
+
+  End ToFinalInHSET.
+
+  Section IngredientsOfAnAdjunction.
+
+  Local Definition out_set_trunc (C : coalgebra F) : coalgebra_ob F C → pr1hSet (F' (settrunc (coalgebra_ob F C))).
+  Proof.
+    intro x.
+    destruct C as [c s_c].
+    cbn -[settrunc].
+    unfold polynomial_functor_obj.
+    use tpair.
+    - exact (pr1(s_c(x))).
+    - intro b.
+      exact (settruncin c (pr2(s_c(x))(b))).
+  Defined.
+
+  Definition coalg_set_trunc (C : coalgebra F) : FunctorCoalgebras.CoAlg_category F'.
+  Proof.
+    exists (settrunc (coalgebra_ob F C)).
+    exact (settrunc_rec _ (out_set_trunc C)).
+  Defined.
+
+  Lemma is_coalgebra_homo_comp_with_settruncin (C : coalgebra F) (C0' : FunctorCoalgebras.coalgebra_ob F') (f : FunctorCoalgebras.CoAlg_category F' ⟦coalg_set_trunc C, C0'⟧)
+    : is_coalgebra_homo F (X:=C) (Y:=FromCoalgInHSET C0') (λ x, pr1 f (settruncin ((coalgebra_ob F C)) x)).
+  Proof.
+    destruct f as [φ p1].
+    set (s0' := FunctorCoalgebras.coalg_map F' C0').
+    destruct C as [c s_c].
+    cbn in c.
+    cbn in s_c.
+    unfold polynomial_functor_obj in s_c.
+    set (c' := settrunc c).
+    set (C' := coalg_set_trunc (c,, s_c) : FunctorCoalgebras.coalgebra_ob F').
+    set (s_c' := FunctorCoalgebras.coalg_map _ C' : c' → pr1hSet (F' c')).
+    cbn -[settrunc] in φ.
+    set (ψ := λ x, φ(settruncin c x) : pr1 (FunctorCoalgebras.coalg_carrier F' C0')).
+    change (is_coalgebra_homo F (X:=(c,,s_c)) (Y:=FromCoalgInHSET C0') ψ).
+    unfold is_coalgebra_homo.
+    apply funextfun.
+    intro x.
+    cbn in x.
+    symmetry.
+    assert (p21 : (s0'(ψ(x)) = s0'(φ(settruncin c x)))).
+    { unfold ψ. apply idpath. }
+    assert (p22 : s0'(ψ(x)) = (#F φ)(s_c'(settruncin c x))).
+    {
+      etrans.
+      - apply p21.
+      - set (f1 := λ y : c', s0'(φ(y))).
+        set (f2 := λ y : c', (#F φ)(s_c'(y))).
+        set (x' := settruncin c x : c').
+        assert (p221 : f1 = f2).
+        { cbn -[settrunc] in p1. unfold f1, f2. cbn -[settrunc]. unfold s0'. symmetry. apply p1. }
+        assert (p222 : f1 x' = f2 x').
+        { apply (toforallpaths _ f1 f2 p221). }
+        apply p222.
+    }
+    assert (p23 : s0'(ψ(x)) = (#F ψ)(s_c(x))).
+    {
+      etrans.
+      - apply p22.
+      - apply idpath.
+    }
+    apply p23.
+  Qed.
+
+  Lemma is_homo_of_coalgebras_settrunc_rec (C : coalgebra F) (C0' : FunctorCoalgebras.coalgebra_ob F') (f' : coalgebra_homo F _ (FromCoalgInHSET C0'))
+    : pr2 (coalg_set_trunc C) -->[settrunc_rec _ (pr1 f')] pr2 (FromCoalgInHSET C0').
+  Proof.
+    destruct f' as [ψ' p'].
+    cbn in ψ'.
+    set (φ' := settrunc_rec _ ψ').
+    destruct C as [c s_c].
+    set (s0' := FunctorCoalgebras.coalg_map F' C0').
+    set (C' := coalg_set_trunc (c,, s_c) : FunctorCoalgebras.coalgebra_ob F').
+    set (s_c' := FunctorCoalgebras.coalg_map _ C').
+    assert (p11' : (s0' ∘ φ' ∘ (settruncin c))%functions = ((#F φ') ∘ s_c' ∘ (settruncin c))%functions).
+    {
+      unfold is_coalgebra_homo in p'.
+      cbn in p'.
+      symmetry.
+      apply p'.
+    }
+    apply settrunc_rec_unique.
+    intro x.
+    apply pathsinv0.
+    apply (toforallpaths _ _ _ p11').
+  Qed.
+
+  End IngredientsOfAnAdjunction.
+
+  Section FromFinalInHSET.
+
+    Context (C0' : FunctorCoalgebras.coalgebra_ob F').
+    Context (C0'_is_final : isTerminal (FunctorCoalgebras.CoAlg_category F') C0').
+
+    Definition C0 : coalgebra F := FromCoalgInHSET C0'.
+
+  Lemma C0_is_final : is_final C0.
+  Proof.
+    set (s0' := FunctorCoalgebras.coalg_map F' C0').
+    intros [c s_c].
+    cbn in c.
+    cbn in s_c.
+    unfold polynomial_functor_obj in s_c.
+    set (c' := settrunc c).
+    set (C' := coalg_set_trunc (c,, s_c) : FunctorCoalgebras.coalgebra_ob F').
+    set (s_c' := FunctorCoalgebras.coalg_map _ C' : c' → pr1hSet (F' c')).
+    destruct (C0'_is_final C') as [f isunique].
+    use tpair.
+    - use tpair.
+      2: { apply (is_coalgebra_homo_comp_with_settruncin _ _ f). }
+    - intro f'.
+      set (φ' := settrunc_rec _ (pr1 f')).
+      set (p1' := is_homo_of_coalgebras_settrunc_rec _ _ f').
+      assert (p41 : (φ',, p1') = f).
+      {
+        apply (isunique (φ',, p1')).
+      }
+      assert (p411 := maponpaths (λ x, pr1 x) p41 : (φ' = pr1 f)).
+      clear p41.
+      use total2_paths_f.
+      + apply funextfun.
+        intro x.
+        etrans.
+        * assert (p421 : pr1 f' x = φ' (settruncin c x)).
+          {
+            apply idpath.
+          }
+          apply p421.
+        * apply (toforallpaths _ φ' (pr1 f) p411).
+      + (* show_id_type.
+           unfold is_coalgebra_homo in TYPE. *)
+        set (is_set := isaset_forall_hSet c (λ _, F' (pr1 C0'))).
+        apply is_set.
+  Defined.
+
+  End FromFinalInHSET.
+End M.
diff --git a/UniMath/Induction/SetBasedPolynomialFunctors.v b/UniMath/Induction/SetBasedPolynomialFunctors.v
new file mode 100644
index 0000000000..07043a7008
--- /dev/null
+++ b/UniMath/Induction/SetBasedPolynomialFunctors.v
@@ -0,0 +1,56 @@
+(** ** Set Based Polynomial Functors
+
+    Author : Ralph Matthes (@rmatthes), 2025
+
+*)
+
+Require Import UniMath.Induction.PolynomialFunctors.
+Require Import UniMath.Induction.M.Core.
+Require Import UniMath.CategoryTheory.Categories.Type.Core.
+Require Import UniMath.Foundations.Sets.
+Require Import UniMath.CategoryTheory.Core.Categories.
+Require Import UniMath.CategoryTheory.Core.Functors.
+Require Import UniMath.CategoryTheory.DisplayedCats.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+
+Local Open Scope cat.
+
+Section SetBasedPolynomialFunctors.
+
+  Context (A : hSet).
+  Context (B : A -> hSet).
+
+  Definition polynomial_functor_HSET_obj (X : hSet) : hSet.
+  Proof.
+    exists (polynomial_functor_obj (pr1hSet A) (fun a => pr1hSet (B a)) X).
+    unfold polynomial_functor_obj.
+    transparent assert (f : (pr1hSet A -> hSet)).
+    { intro a.
+      use tpair.
+      - exact (pr1hSet (B a) -> pr1hSet X).
+      - apply isaset_forall_hSet.
+    }
+    exact (isaset_total2_hSet _ f).
+  Defined.
+
+  Definition polynomial_functor_HSET_data : functor_data HSET HSET.
+  Proof.
+    use make_functor_data.
+    - exact polynomial_functor_HSET_obj.
+    - intros X Y.
+      simpl.
+      apply (polynomial_functor_arr (pr1hSet A) (fun a => pr1hSet (B a))).
+  Defined.
+
+  Lemma polynomial_functor_HSET_is_functor : is_functor polynomial_functor_HSET_data.
+  Proof.
+    split.
+    - intro.
+      apply idpath.
+    - intros ? ? ? ? ?.
+      apply idpath.
+  Qed.
+
+  Definition polynomial_functor_HSET : functor HSET HSET := _ ,, polynomial_functor_HSET_is_functor.
+
+End SetBasedPolynomialFunctors.
diff --git a/UniMath/MoreFoundations/Sets.v b/UniMath/MoreFoundations/Sets.v
index 5ad3989281..a9e4b165bd 100644
--- a/UniMath/MoreFoundations/Sets.v
+++ b/UniMath/MoreFoundations/Sets.v
@@ -12,6 +12,7 @@ Require Export UniMath.Foundations.Sets.
   - The equivalence relation of being in the same fiber
   - Subsets
   - Binary relations
+  - Set truncation
  *)
 
 Local Open Scope logic.
@@ -497,3 +498,98 @@ Proof.
   rewrite hSet_univalence_map_univalence_hSet.
   apply idpath.
 Qed.
+
+(** ** Set truncation
+    Based on a post by Niels van der Weide on June 13, 2023
+ *)
+
+Local Close Scope logic.
+
+Definition path_eqrel
+           (X : UU)
+  : eqrel X.
+Proof.
+  use make_eqrel.
+  - exact (λ x₁ x₂, ∥ x₁ = x₂ ∥ : hProp).
+  - repeat split.
+    + intros x₁ x₂ x₃.
+      use factor_through_squash.
+      {
+        apply impred ; intro.
+        apply propproperty.
+      }
+      intro p.
+      use factor_through_squash.
+      {
+        apply propproperty.
+      }
+      intro q.
+      apply hinhpr.
+      exact (p @ q).
+    + intros x.
+      exact (hinhpr (idpath _)).
+    + intros x₁ x₂.
+      use factor_through_squash.
+      {
+        apply propproperty.
+      }
+      intro p.
+      apply hinhpr.
+      exact (!p).
+Defined.
+
+Definition settrunc
+           (X : UU)
+  : hSet
+  := setquotinset (path_eqrel X).
+
+Definition settruncin
+           (X : UU)
+  : X → settrunc X
+  := setquotpr (path_eqrel X).
+
+
+Definition settrunc_rec
+           (X : UU)
+           {Y : hSet}
+           (i : X → Y)
+  : settrunc X → Y.
+Proof.
+  use setquotuniv.
+  - exact i.
+  - intros x₁ x₂.
+    use factor_through_squash.
+    {
+      apply setproperty.
+    }
+    intro p.
+    exact (maponpaths i p).
+Defined.
+
+Definition settrunc_rec_eq
+           (X : UU)
+           {Y : hSet}
+           (i : X → Y)
+           (x : X)
+  : settrunc_rec X i (settruncin X x) = i x.
+Proof.
+  apply idpath.
+Qed.
+
+Definition settrunc_rec_unique
+           (X : UU)
+           {Y : hSet}
+           (f g : settrunc X → Y)
+           (p : ∏ (x : X), f (settruncin X x) = g (settruncin X x))
+  : f = g.
+Proof.
+  use funextsec.
+  use setquotunivprop'.
+  {
+    intro.
+    apply setproperty.
+  }
+  intro x.
+  cbn.
+  exact (p x).
+Qed.