diff --git a/Mathlib.lean b/Mathlib.lean
index a096d1453b48ea..fdffa5948cc9e1 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2314,6 +2314,7 @@ import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
 import Mathlib.CategoryTheory.Functor.KanExtension.Basic
+import Mathlib.CategoryTheory.Functor.KanExtension.Dense
 import Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
 import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
 import Mathlib.CategoryTheory.Functor.KanExtension.Preserves
@@ -2340,6 +2341,7 @@ import Mathlib.CategoryTheory.Generator.Indization
 import Mathlib.CategoryTheory.Generator.Preadditive
 import Mathlib.CategoryTheory.Generator.Presheaf
 import Mathlib.CategoryTheory.Generator.Sheaf
+import Mathlib.CategoryTheory.Generator.StrongGenerator
 import Mathlib.CategoryTheory.GlueData
 import Mathlib.CategoryTheory.GradedObject
 import Mathlib.CategoryTheory.GradedObject.Associator
@@ -2711,11 +2713,13 @@ import Mathlib.CategoryTheory.Noetherian
 import Mathlib.CategoryTheory.ObjectProperty.Basic
 import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 import Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
+import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
 import Mathlib.CategoryTheory.ObjectProperty.ContainsZero
 import Mathlib.CategoryTheory.ObjectProperty.EpiMono
 import Mathlib.CategoryTheory.ObjectProperty.Extensions
 import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
 import Mathlib.CategoryTheory.ObjectProperty.Ind
+import Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
 import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
 import Mathlib.CategoryTheory.ObjectProperty.Local
 import Mathlib.CategoryTheory.ObjectProperty.Opposite
@@ -2759,8 +2763,10 @@ import Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
 import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
 import Mathlib.CategoryTheory.Presentable.Basic
+import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
 import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
 import Mathlib.CategoryTheory.Presentable.ColimitPresentation
+import Mathlib.CategoryTheory.Presentable.Directed
 import Mathlib.CategoryTheory.Presentable.Finite
 import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
 import Mathlib.CategoryTheory.Presentable.Limits
@@ -5113,6 +5119,7 @@ import Mathlib.Order.Category.LinOrd
 import Mathlib.Order.Category.NonemptyFinLinOrd
 import Mathlib.Order.Category.OmegaCompletePartialOrder
 import Mathlib.Order.Category.PartOrd
+import Mathlib.Order.Category.PartOrdEmb
 import Mathlib.Order.Category.Preord
 import Mathlib.Order.Category.Semilat
 import Mathlib.Order.Chain
diff --git a/Mathlib/CategoryTheory/Comma/Arrow.lean b/Mathlib/CategoryTheory/Comma/Arrow.lean
index a2f3c8ff964c71..c3628882e84eaf 100644
--- a/Mathlib/CategoryTheory/Comma/Arrow.lean
+++ b/Mathlib/CategoryTheory/Comma/Arrow.lean
@@ -72,6 +72,10 @@ theorem mk_eq (f : Arrow T) : Arrow.mk f.hom = f := by
   cases f
   rfl
 
+lemma mk_surjective (f : Arrow T) :
+    ∃ (X Y : T) (g : X ⟶ Y), f = Arrow.mk g :=
+  ⟨_, _, f.hom, rfl⟩
+
 theorem mk_injective (A B : T) :
     Function.Injective (Arrow.mk : (A ⟶ B) → Arrow T) := fun f g h => by
   cases h
diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean
index ea569695d60868..92e7574cea778f 100644
--- a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean
+++ b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean
@@ -17,7 +17,7 @@ be used in the proof of the Special Adjoint Functor Theorem.
 namespace CategoryTheory
 
 -- morphism levels before object levels. See note [category theory universes].
-universe v₁ v₂ u₁ u₂
+universe w v₁ v₂ u₁ u₂
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
@@ -25,6 +25,12 @@ namespace StructuredArrow
 
 variable {S : D} {T : C ⥤ D}
 
+instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (StructuredArrow S T) :=
+  small_of_surjective (f := fun (f : Σ (X : C), S ⟶ T.obj X) ↦ StructuredArrow.mk f.2)
+    (fun f ↦ by
+      obtain ⟨X, f, rfl⟩ := f.mk_surjective
+      exact ⟨⟨X, f⟩, rfl⟩)
+
 instance small_inverseImage_proj_of_locallySmall
     {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] :
     ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by
@@ -45,6 +51,12 @@ namespace CostructuredArrow
 
 variable {S : C ⥤ D} {T : D}
 
+instance [Small.{w} C] [LocallySmall.{w} D] : Small.{w} (CostructuredArrow S T) :=
+  small_of_surjective (f := fun (f : Σ (X : C), S.obj X ⟶ T) ↦ CostructuredArrow.mk f.2)
+    (fun f ↦ by
+      obtain ⟨X, f, rfl⟩ := f.mk_surjective
+      exact ⟨⟨X, f⟩, rfl⟩)
+
 instance small_inverseImage_proj_of_locallySmall
     {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] :
     ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by
diff --git a/Mathlib/CategoryTheory/Filtered/Final.lean b/Mathlib/CategoryTheory/Filtered/Final.lean
index dc754515c96869..82c0cedb435753 100644
--- a/Mathlib/CategoryTheory/Filtered/Final.lean
+++ b/Mathlib/CategoryTheory/Filtered/Final.lean
@@ -436,24 +436,22 @@ end Pi
 
 section Prod
 
-open IsFiltered in
-instance final_fst [IsFilteredOrEmpty C] [IsFiltered D] : (Prod.fst C D).Final := by
-  apply Functor.final_of_exists_of_isFiltered
-  · exact fun c => ⟨(c, nonempty.some), ⟨𝟙 c⟩⟩
-  · intro c ⟨c', d'⟩ f g
-    exact ⟨(coeq f g, d'), (coeqHom f g, 𝟙 d'), coeq_condition _ _⟩
+instance final_fst [IsFiltered D] : (Prod.fst C D).Final := by
+  let F : D ⥤ Discrete PUnit.{1} := (Functor.const _).obj (Discrete.mk .unit)
+  have hF : F.Final := Functor.final_of_isFiltered_of_pUnit _
+  change (Functor.prod (𝟭 C) F ⋙ (prod.rightUnitorEquivalence.{0} C).functor).Final
+  infer_instance
 
-instance final_snd [IsFiltered C] [IsFilteredOrEmpty D] : (Prod.snd C D).Final :=
+instance final_snd [IsFiltered C] : (Prod.snd C D).Final :=
   inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Final
 
-open IsCofiltered in
-instance initial_fst [IsCofilteredOrEmpty C] [IsCofiltered D] : (Prod.fst C D).Initial := by
-  apply Functor.initial_of_exists_of_isCofiltered
-  · exact fun c => ⟨(c, nonempty.some), ⟨𝟙 c⟩⟩
-  · intro c ⟨c', d'⟩ f g
-    exact ⟨(eq f g, d'), (eqHom f g, 𝟙 d'), eq_condition _ _⟩
+instance initial_fst [IsCofiltered D] : (Prod.fst C D).Initial := by
+  let F : D ⥤ Discrete PUnit.{1} := (Functor.const _).obj (Discrete.mk .unit)
+  have hF : F.Initial := Functor.initial_of_isCofiltered_pUnit _
+  change (Functor.prod (𝟭 C) F ⋙ (prod.rightUnitorEquivalence.{0} C).functor).Initial
+  infer_instance
 
-instance initial_snd [IsCofiltered C] [IsCofilteredOrEmpty D] : (Prod.snd C D).Initial :=
+instance initial_snd [IsCofiltered C] : (Prod.snd C D).Initial :=
   inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Initial
 
 end Prod
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean
new file mode 100644
index 00000000000000..060a9ebb99fcc6
--- /dev/null
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean
@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
+import Mathlib.CategoryTheory.Limits.Presheaf
+import Mathlib.CategoryTheory.Generator.StrongGenerator
+
+/-!
+# Dense functors
+
+A functor `F : C ⥤ D` is dense (`F.IsDense`) if `𝟭 D` is a pointwise
+left Kan extension of `F` along itself, i.e. any `Y : D` is the
+colimit of all `F.obj X` for all morphisms `F.obj X ⟶ Y` (which
+is the condition `F.DenseAt Y`).
+When `F` is full, we show that this
+is equivalent to saying that the restricted Yoneda functor
+`D ⥤ Cᵒᵖ ⥤ Type _` is fully faithful (see the lemma
+`Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda`).
+
+We also show that the range of a dense functor is a strong
+generator (see `Functor.isStrongGenerator_of_isDense`).
+
+## References
+
+* https://ncatlab.org/nlab/show/dense+subcategory
+
+-/
+
+universe w v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+open Limits Opposite Presheaf
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
+
+namespace Functor
+
+/-- A functor `F : C ⥤ D` is dense if any `Y : D` is a canonical colimit
+relatively to `F`. -/
+class IsDense (F : C ⥤ D) : Prop where
+  isDenseAt (F) (Y : D) : F.isDenseAt Y
+
+/-- This is a choice of structure `F.DenseAt Y` when `F : C ⥤ D`
+is dense, and `Y : D`. -/
+noncomputable def denseAt (F : C ⥤ D) [F.IsDense] (Y : D) : F.DenseAt Y :=
+  (IsDense.isDenseAt F Y).some
+
+lemma isDense_iff_nonempty_isPointwiseLeftKanExtension (F : C ⥤ D) :
+    F.IsDense ↔
+      Nonempty ((LeftExtension.mk _ (rightUnitor F).inv).IsPointwiseLeftKanExtension) :=
+  ⟨fun _ ↦ ⟨fun _ ↦ F.denseAt _⟩, fun ⟨h⟩ ↦ ⟨fun _ ↦ ⟨h _⟩⟩⟩
+
+variable (F : C ⥤ D)
+
+instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Faithful where
+  map_injective h :=
+    (F.denseAt _).hom_ext' (fun X p ↦ by
+      simpa using ULift.up_injective (congr_fun (NatTrans.congr_app h (op X)) (ULift.up p)))
+
+instance [F.IsDense] : (restrictedULiftYoneda.{w} F).Full where
+  map_surjective {Y Z} f := by
+    let c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
+      { pt := Z
+        ι :=
+          { app g := ((f.app (op g.left)) (ULift.up g.hom)).down
+            naturality g₁ g₂ φ := by
+              simpa [uliftFunctor, uliftYoneda,
+                restrictedULiftYoneda, ← ULift.down_inj] using
+                (congr_fun (f.naturality φ.left.op) (ULift.up g₂.hom)).symm }}
+    refine ⟨(F.denseAt Y).desc c, ?_⟩
+    ext ⟨X⟩ ⟨x⟩
+    have := (F.denseAt Y).fac c (.mk x)
+    dsimp [c] at this
+    simpa using ULift.down_injective this
+
+variable {F} in
+lemma IsDense.of_fullyFaithful_restrictedULiftYoneda [F.Full]
+    (h : (restrictedULiftYoneda.{w} F).FullyFaithful) :
+    F.IsDense where
+  isDenseAt Y := by
+    let φ (s : Cocone (CostructuredArrow.proj F Y ⋙ F)) :
+        (restrictedULiftYoneda.{w} F).obj Y ⟶ (restrictedULiftYoneda F).obj s.pt :=
+      { app := fun ⟨X⟩ ⟨x⟩ ↦ ULift.up (s.ι.app (.mk x))
+        naturality := by
+          rintro ⟨X₁⟩ ⟨X₂⟩ ⟨f⟩
+          ext ⟨x⟩
+          let α : CostructuredArrow.mk (F.map f ≫ x) ⟶ CostructuredArrow.mk x :=
+            CostructuredArrow.homMk f
+          simp [uliftYoneda, ← s.w α, α] }
+    have hφ (s) (j) : (restrictedULiftYoneda F).map j.hom ≫ φ s =
+        (restrictedULiftYoneda F).map (s.ι.app j) := by
+      ext ⟨X⟩ ⟨x⟩
+      let α : .mk (x ≫ j.hom) ⟶ j := CostructuredArrow.homMk (F.preimage x)
+      have := s.w α
+      dsimp [uliftYoneda, φ, α] at this ⊢
+      rw [← this, map_preimage]
+    exact
+      ⟨{desc s := (h.preimage (φ s))
+        fac s j := h.map_injective (by simp [hφ])
+        uniq s m hm := h.map_injective (by
+          ext ⟨X⟩ ⟨x⟩
+          simp [uliftYoneda, φ, ← hm])}⟩
+
+lemma isDense_iff_fullyFaithful_restrictedULiftYoneda [F.Full] :
+    F.IsDense ↔ Nonempty (restrictedULiftYoneda.{w} F).FullyFaithful :=
+  ⟨fun _ ↦ ⟨FullyFaithful.ofFullyFaithful _⟩,
+    fun ⟨h⟩ ↦ IsDense.of_fullyFaithful_restrictedULiftYoneda h⟩
+
+open ObjectProperty in
+lemma isStrongGenerator_of_isDense [F.IsDense] :
+    IsStrongGenerator (.ofObj F.obj) :=
+  (IsStrongGenerator.mk_of_exists_colimitsOfShape.{max u₁ u₂ v₁ v₂} (fun Y ↦ ⟨_, _, ⟨{
+    ι := _
+    diag := _
+    isColimit := (IsColimit.whiskerEquivalence (F.denseAt Y)
+      ((ShrinkHoms.equivalence _).symm.trans ((Shrink.equivalence _)).symm))
+    prop_diag_obj := by simp }⟩⟩))
+
+end Functor
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Generator/Basic.lean b/Mathlib/CategoryTheory/Generator/Basic.lean
index c2d90981ea0cde..3fa05bf3af7a59 100644
--- a/Mathlib/CategoryTheory/Generator/Basic.lean
+++ b/Mathlib/CategoryTheory/Generator/Basic.lean
@@ -7,6 +7,9 @@ import Mathlib.CategoryTheory.Limits.EssentiallySmall
 import Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
 import Mathlib.CategoryTheory.Subobject.Lattice
 import Mathlib.CategoryTheory.ObjectProperty.Small
+import Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
+import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
+import Mathlib.CategoryTheory.Comma.StructuredArrow.Small
 
 /-!
 # Separating and detecting sets
@@ -287,31 +290,117 @@ lemma isCodetecting_bot_of_isGroupoid [IsGroupoid C] :
 
 end Empty
 
+lemma IsSeparating.mk_of_exists_epi
+    (hP : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Cofan s) (_ : IsColimit c)
+      (p : c.pt ⟶ X), Epi p) :
+    P.IsSeparating := by
+  intro X Y f g h
+  obtain ⟨ι, s, hs, c, hc, p, _⟩ := hP X
+  rw [← cancel_epi p]
+  exact Cofan.IsColimit.hom_ext hc _ _
+    (fun i ↦ by simpa using h _ (hs i) (c.inj i ≫ p))
+
+lemma IsCoseparating.mk_of_exists_mono
+    (hP : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Fan s) (_ : IsLimit c)
+      (j : X ⟶ c.pt), Mono j) :
+    P.IsCoseparating := by
+  intro X Y f g h
+  obtain ⟨ι, s, hs, c, hc, j, _⟩ := hP Y
+  rw [← cancel_mono j]
+  exact Fan.IsLimit.hom_ext hc _ _
+    (fun i ↦ by simpa using h _ (hs i) (j ≫ c.proj i))
+
+lemma IsSeparating.mk_of_exists_colimitsOfShape
+    (hP : ∀ (X : C), ∃ (J : Type w) (_ : SmallCategory J), Nonempty (P.ColimitOfShape J X)) :
+    P.IsSeparating := by
+  intro X Y f g h
+  obtain ⟨J, _, ⟨p⟩⟩ := hP X
+  exact p.isColimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)
+
+lemma IsCoseparating.mk_of_exists_limitsOfShape
+    (hP : ∀ (X : C), ∃ (J : Type w) (_ : SmallCategory J), Nonempty (P.LimitOfShape J X)) :
+    P.IsCoseparating := by
+  intro X Y f g h
+  obtain ⟨J, _, ⟨p⟩⟩ := hP Y
+  exact p.isLimit.hom_ext (fun j ↦ h _ (p.prop_diag_obj _) _)
+
 variable (P)
 
+section
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the map which
+sends `i : CostructuredArrow P.ι X` to `i.left.obj : C`. The coproduct
+of this family is the source of the morphism `P.coproductFrom X`. -/
+abbrev coproductFromFamily (X : C) (i : CostructuredArrow P.ι X) : C := i.left.obj
+
+variable (X : C)
+
+variable [HasCoproduct (P.coproductFromFamily X)]
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the coproduct of
+all the morphisms `Y ⟶ X` such that `P Y` holds. -/
+noncomputable abbrev coproductFrom : ∐ (P.coproductFromFamily X) ⟶ X :=
+  Sigma.desc (fun i ↦ i.hom)
+
+variable {X} in
+/-- The inclusion morphisms to `∐ (P.coproductFromFamily X)`. -/
+noncomputable abbrev ιCoproductFrom {Y : C} (f : Y ⟶ X) (hY : P Y) :
+    Y ⟶ ∐ (P.coproductFromFamily X) := by
+  exact Sigma.ι (P.coproductFromFamily X) (CostructuredArrow.mk (Y := ⟨Y, hY⟩) (by exact f))
+
+end
+
+variable {P} in
+lemma IsSeparating.epi_coproductFrom (hP : P.IsSeparating)
+    (X : C) [HasCoproduct (P.coproductFromFamily X)] :
+    Epi (P.coproductFrom X) where
+  left_cancellation u v huv :=
+    hP _ _ (fun G hG h ↦ by simpa using P.ιCoproductFrom h hG ≫= huv)
+
 theorem isSeparating_iff_epi
-    [∀ A : C, HasCoproduct fun f : Σ G : Subtype P, G.1 ⟶ A ↦ f.1.1] :
-    IsSeparating P ↔
-      ∀ A : C, Epi (Sigma.desc (Sigma.snd (β := fun (G : Subtype P) ↦ G.1 ⟶ A))) := by
-  let β (A : C) (G : Subtype P) := G.1 ⟶ A
-  let b (A : C) (x : Σ G, β A G) := x.1.1
-  refine ⟨fun h A ↦ ⟨fun u v huv ↦ h _ _ fun G hG f ↦ ?_⟩, fun h X Y f g hh ↦ ?_⟩
-  · simpa [β, b] using Sigma.ι (b A) ⟨⟨G, hG⟩, f⟩ ≫= huv
-  · rw [← cancel_epi (Sigma.desc (Sigma.snd (β := β X)))]
-    ext ⟨⟨_, hG⟩, _⟩
-    simpa using hh _ hG _
+    [∀ (X : C), HasCoproduct (P.coproductFromFamily X)] :
+    IsSeparating P ↔ ∀ X : C, Epi (P.coproductFrom X) :=
+  ⟨fun hP X ↦ hP.epi_coproductFrom X,
+    fun hP ↦ IsSeparating.mk_of_exists_epi (fun X ↦ ⟨_, P.coproductFromFamily X,
+      fun i ↦ i.left.2, _, colimit.isColimit _, _, hP X⟩)⟩
+
+section
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the map which
+sends `i : StructuredArrow P.ι X` to `i.right.obj : C`. The product
+of this family is the target of the morphism `P.productTo X`. -/
+abbrev productToFamily (X : C) (i : StructuredArrow X P.ι) : C := i.right.obj
+
+variable (X : C)
+
+variable [HasProduct (P.productToFamily X)]
+
+/-- Given `P : ObjectProperty C` and `X : C`, this is the product of
+all the morphisms `X ⟶ Y` such that `P Y` holds. -/
+noncomputable abbrev productTo : X ⟶ ∏ᶜ (P.productToFamily X) :=
+  Pi.lift (fun i ↦ i.hom)
+
+variable {X} in
+/-- The projection morphisms from `∏ᶜ (P.productToFamily X)`. -/
+noncomputable abbrev πProductTo {Y : C} (f : X ⟶ Y) (hY : P Y) :
+    ∏ᶜ (P.productToFamily X) ⟶ Y := by
+  exact Pi.π (P.productToFamily X) (StructuredArrow.mk (Y := ⟨Y, hY⟩) (by exact f))
+
+end
+
+variable {P} in
+lemma IsCoseparating.mono_productTo (hP : P.IsCoseparating)
+    (X : C) [HasProduct (P.productToFamily X)] :
+    Mono (P.productTo X) where
+  right_cancellation u v huv :=
+    hP _ _ (fun G hG h ↦ by simpa using huv =≫ P.πProductTo h hG)
 
 theorem isCoseparating_iff_mono
-    [∀ A : C, HasProduct fun f : Σ G : Subtype P, A ⟶ G.1 ↦ f.1.1] :
-    IsCoseparating P ↔
-      ∀ A : C, Mono (Pi.lift (Sigma.snd (β := fun (G : Subtype P) ↦ A ⟶ G.1))) := by
-  let β (A : C) (G : Subtype P) := A ⟶ G.1
-  let b (A : C) (x : Σ G, β A G) := x.1.1
-  refine ⟨fun h A ↦ ⟨fun u v huv ↦ h _ _ fun G hG f ↦ ?_⟩, fun h X Y f g hh ↦ ?_⟩
-  · simpa [β, b] using huv =≫ Pi.π (b A) ⟨⟨G, hG⟩, f⟩
-  · rw [← cancel_mono (Pi.lift (Sigma.snd (β := β Y)))]
-    ext ⟨⟨_, hG⟩, _⟩
-    simpa using hh _ hG _
+    [∀ (X : C), HasProduct (P.productToFamily X)] :
+    IsCoseparating P ↔ ∀ X : C, Mono (P.productTo X) :=
+  ⟨fun hP X ↦ hP.mono_productTo X,
+    fun hP ↦ IsCoseparating.mk_of_exists_mono (fun X ↦ ⟨_, P.productToFamily X,
+      fun i ↦ i.right.2, _, limit.isLimit _, _, hP X⟩)⟩
 
 end ObjectProperty
 
@@ -324,16 +413,17 @@ theorem hasInitial_of_isCoseparating [LocallySmall.{w} C] [WellPowered.{w} C]
     [HasLimitsOfSize.{w, w} C] {P : ObjectProperty C} [ObjectProperty.Small.{w} P]
     (hP : P.IsCoseparating) : HasInitial C := by
   have := hasFiniteLimits_of_hasLimitsOfSize C
-  haveI : HasProductsOfShape (Subtype P) C := hasProductsOfShape_of_small C (Subtype P)
-  haveI := fun A => hasProductsOfShape_of_small.{w} C (Σ G : Subtype P, A ⟶ (G : C))
+  haveI := hasProductsOfShape_of_small C (Subtype P)
+  haveI := fun A => hasProductsOfShape_of_small.{w} C (StructuredArrow A P.ι)
   letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : Subtype P → C)))
   suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by
     exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C)
+  have := hP.mono_productTo
   refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
-  · let s := Pi.lift fun f : Σ G : Subtype P, A ⟶ (G : C) => Pi.π (Subtype.val : Subtype P → C) f.1
-    let t := Pi.lift (@Sigma.snd (Subtype P) fun G => A ⟶ (G : C))
-    haveI : Mono t := P.isCoseparating_iff_mono.1 hP A
-    exact Subobject.ofLEMk _ (pullback.fst _ _ : pullback s t ⟶ _) bot_le ≫ pullback.snd _ _
+  · let s : ∏ᶜ (Subtype.val (p := P)) ⟶ ∏ᶜ P.productToFamily A :=
+      Pi.lift (fun f ↦ Pi.π Subtype.val ⟨f.right.obj, f.right.property⟩)
+    exact Subobject.ofLEMk _
+      (pullback.fst _ _ : pullback s (P.productTo A) ⟶ _) bot_le ≫ pullback.snd _ _
   · suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
       apply this
     intro g
diff --git a/Mathlib/CategoryTheory/Generator/StrongGenerator.lean b/Mathlib/CategoryTheory/Generator/StrongGenerator.lean
new file mode 100644
index 00000000000000..ea67d6a0d4994d
--- /dev/null
+++ b/Mathlib/CategoryTheory/Generator/StrongGenerator.lean
@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.ExtremalEpi
+import Mathlib.CategoryTheory.Generator.Basic
+import Mathlib.CategoryTheory.Limits.Presentation
+
+/-!
+# Strong generators
+
+If `P : ObjectProperty C`, we say that `P` is a strong generator if it is a
+generator (in the sense that `IsSeparating P` holds) such that for any
+proper subobject `A ⊂ X`, there exists a morphism `G ⟶ X` which does not factor
+through `A` from an object satisfying `P`.
+
+The main result is the lemma `isStrongGenerator_iff_exists_extremalEpi` which
+says that if `P` is `w`-small, `C` is locally `w`-small and
+has coproducts of size `w`, then `P` is a strong generator iff any
+object of `C` is the target of an extremal epimorphism from a coproduct of
+objects satisfying `P`.
+
+We also show that if any object in `C` is a colimit of objects in `S`,
+then `S` is a strong generator.
+
+## References
+* [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994]
+
+-/
+
+universe w v u
+
+namespace CategoryTheory
+
+open Limits
+
+
+namespace ObjectProperty
+
+variable {C : Type u} [Category.{v} C] (P : ObjectProperty C)
+
+/-- A property `P : ObjectProperty C` is a strong generator
+if it is separating and for any proper subobject `A ⊂ X`, there exists
+a morphism `G ⟶ X` which does not factor through `A` from an object
+such that `P G` holds. -/
+def IsStrongGenerator : Prop :=
+  P.IsSeparating ∧ ∀ ⦃X : C⦄ (A : Subobject X),
+    (∀ (G : C) (_ : P G) (f : G ⟶ X), Subobject.Factors A f) → A = ⊤
+
+variable {P}
+
+lemma isStrongGenerator_iff :
+    P.IsStrongGenerator ↔ P.IsSeparating ∧
+      ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
+        (∀ (G : C) (_ : P G), Function.Surjective (fun (f : G ⟶ X) ↦ f ≫ i)) → IsIso i := by
+  refine ⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
+    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩
+  · rw [Subobject.isIso_iff_mk_eq_top]
+    refine hS₂ _ (fun G hG g ↦ ?_)
+    rw [Subobject.mk_factors_iff]
+    exact h G hG g
+  · rw [← Subobject.isIso_arrow_iff_eq_top]
+    exact hS₂ A.arrow (fun G hG g ↦ ⟨_, Subobject.factorThru_arrow _ _ (hA G hG g)⟩)
+
+namespace IsStrongGenerator
+
+section
+
+variable (hP : P.IsStrongGenerator)
+
+include hP
+
+lemma isSeparating : P.IsSeparating := hP.1
+
+lemma subobject_eq_top {X : C} {A : Subobject X}
+    (hA : ∀ (G : C) (_ : P G) (f : G ⟶ X), Subobject.Factors A f) :
+    A = ⊤ :=
+  hP.2 _ hA
+
+lemma isIso_of_mono ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i]
+    (hi : ∀ (G : C) (_ : P G), Function.Surjective (fun (f : G ⟶ X) ↦ f ≫ i)) : IsIso i :=
+  (isStrongGenerator_iff.1 hP).2 i hi
+
+lemma exists_of_subobject_ne_top {X : C} {A : Subobject X} (hA : A ≠ ⊤) :
+    ∃ (G : C) (_ : P G) (f : G ⟶ X), ¬ Subobject.Factors A f := by
+  by_contra!
+  exact hA (hP.subobject_eq_top this)
+
+lemma exists_of_mono_not_isIso {X Y : C} (i : X ⟶ Y) [Mono i] (hi : ¬ IsIso i) :
+    ∃ (G : C) (_ : P G) (g : G ⟶ Y), ∀ (f : G ⟶ X), f ≫ i ≠ g := by
+  by_contra!
+  exact hi (hP.isIso_of_mono i this)
+
+end
+
+end IsStrongGenerator
+
+namespace IsStrongGenerator
+
+lemma mk_of_exists_extremalEpi
+    (hS : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Cofan s) (_ : IsColimit c)
+      (p : c.pt ⟶ X), ExtremalEpi p) :
+    P.IsStrongGenerator := by
+  rw [isStrongGenerator_iff]
+  refine ⟨IsSeparating.mk_of_exists_epi.{w} (fun X ↦ ?_), fun X Y i _ hi ↦ ?_⟩
+  · obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS X
+    exact ⟨ι, s, hs, c, hc, p, inferInstance⟩
+  · obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS Y
+    replace hi (j : ι) := hi (s j) (hs j) (c.inj j ≫ p)
+    choose φ hφ using hi
+    exact ExtremalEpi.isIso p (Cofan.IsColimit.desc hc φ) _
+      (Cofan.IsColimit.hom_ext hc _ _ (by simp [hφ]))
+
+lemma extremalEpi_coproductFrom
+    (hP : IsStrongGenerator P) (X : C) [HasCoproduct (P.coproductFromFamily X)] :
+    ExtremalEpi (P.coproductFrom X) where
+  toEpi := hP.isSeparating.epi_coproductFrom X
+  isIso p i fac _ := hP.isIso_of_mono _ (fun G hG f ↦ ⟨P.ιCoproductFrom f hG ≫ p, by simp [fac]⟩)
+
+end IsStrongGenerator
+
+lemma isStrongGenerator_iff_exists_extremalEpi
+    [HasCoproducts.{w} C] [LocallySmall.{w} C] [ObjectProperty.Small.{w} P] :
+    P.IsStrongGenerator ↔
+      ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ i, P (s i)) (c : Cofan s) (_ : IsColimit c)
+        (p : c.pt ⟶ X), ExtremalEpi p := by
+  refine ⟨fun hP X ↦ ?_, fun hP ↦ .mk_of_exists_extremalEpi hP⟩
+  have := hasCoproductsOfShape_of_small.{w} C (CostructuredArrow P.ι X)
+  have := (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
+    (Discrete.equivalence (equivShrink.{w} _)).symm
+  refine ⟨_, fun j ↦ ((equivShrink.{w} (CostructuredArrow P.ι X)).symm j).left.1,
+    fun j ↦ ((equivShrink.{w} _).symm j).1.2, _,
+    (coproductIsCoproduct (P.coproductFromFamily X)).whiskerEquivalence
+    (Discrete.equivalence (equivShrink.{w} _)).symm, _, hP.extremalEpi_coproductFrom X⟩
+
+lemma IsStrongGenerator.mk_of_exists_colimitsOfShape
+    (hP : ∀ (X : C), ∃ (J : Type w) (_ : SmallCategory J), Nonempty (P.ColimitOfShape J X)) :
+    P.IsStrongGenerator := by
+  rw [isStrongGenerator_iff]
+  refine ⟨IsSeparating.mk_of_exists_colimitsOfShape hP,
+    fun X Y i _ hi ↦ ?_⟩
+  suffices ∃ (r : Y ⟶ X), r ≫ i = 𝟙 Y by
+    obtain ⟨r, fac⟩ := this
+    exact ⟨r, by simp [← cancel_mono i, fac], fac⟩
+  obtain ⟨J, _, ⟨p⟩⟩ := hP Y
+  choose φ hφ using fun j ↦ hi _ (p.prop_diag_obj j) (p.ι.app j)
+  dsimp at hφ
+  let c : Cocone p.diag := Cocone.mk _
+    { app := φ
+      naturality j₁ j₂ f := by simp [← cancel_mono i, hφ] }
+  refine ⟨p.isColimit.desc c, p.isColimit.hom_ext (fun j ↦ ?_)⟩
+  dsimp
+  rw [p.isColimit.fac_assoc, hφ, Category.comp_id]
+
+end ObjectProperty
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean
index ce26bbffd1d56b..77f3fe1f7c3fbd 100644
--- a/Mathlib/CategoryTheory/Limits/Final.lean
+++ b/Mathlib/CategoryTheory/Limits/Final.lean
@@ -1111,6 +1111,9 @@ variable (F : C ⥤ D) (G : C' ⥤ D')
 instance [F.Final] [G.Final] : (F.prod G).Final where
   out := fun ⟨d, d'⟩ => isConnected_of_equivalent (StructuredArrow.prodEquivalence d d' F G).symm
 
+instance [F.Initial] [G.Initial] : (F.prod G).Initial where
+  out := fun ⟨d, d'⟩ => isConnected_of_equivalent (CostructuredArrow.prodEquivalence F G d d').symm
+
 end Prod
 
 namespace ObjectProperty
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
index 9603cb981d8367..f46a16aa46cfe9 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
@@ -184,6 +184,31 @@ lemma Hom.id_eq_id (X : WalkingMultispan J) : Hom.id X = 𝟙 X := rfl
 lemma Hom.comp_eq_comp {X Y Z : WalkingMultispan J}
     (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.comp f g = f ≫ g := rfl
 
+variable (J) in
+/-- The bijection `WalkingMultispan J ≃ J.L ⊕ J.R`. -/
+def equiv : WalkingMultispan J ≃ J.L ⊕ J.R where
+  toFun x := match x with
+    | left a => Sum.inl a
+    | right b => Sum.inr b
+  invFun := Sum.elim left right
+  left_inv := by rintro (_ | _) <;> rfl
+  right_inv := by rintro (_ | _) <;> rfl
+
+variable (J) in
+/-- The bijection `Arrow (WalkingMultispan J) ≃ WalkingMultispan J ⊕ J.R ⊕ J.R`. -/
+def arrowEquiv :
+    Arrow (WalkingMultispan J) ≃ WalkingMultispan J ⊕ J.L ⊕ J.L where
+  toFun f := match f.hom with
+    | .id x => Sum.inl x
+    | .fst a => Sum.inr (Sum.inl a)
+    | .snd a => Sum.inr (Sum.inr a)
+  invFun :=
+    Sum.elim (fun X ↦ Arrow.mk (𝟙 X))
+      (Sum.elim (fun a ↦ Arrow.mk (Hom.fst a : left _ ⟶ right _))
+        (fun a ↦ Arrow.mk (Hom.snd a : left _ ⟶ right _)))
+  left_inv := by rintro ⟨_, _, (_ | _ | _)⟩ <;> rfl
+  right_inv := by rintro (_ | _ | _) <;> rfl
+
 end WalkingMultispan
 
 /-- This is a structure encapsulating the data necessary to define a `Multicospan`. -/
diff --git a/Mathlib/CategoryTheory/Limits/Types/Filtered.lean b/Mathlib/CategoryTheory/Limits/Types/Filtered.lean
index aeabaeef779d3b..0b9b47cf1cafdc 100644
--- a/Mathlib/CategoryTheory/Limits/Types/Filtered.lean
+++ b/Mathlib/CategoryTheory/Limits/Types/Filtered.lean
@@ -152,4 +152,14 @@ theorem colimit_eq_iff [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} :
       ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj :=
   isColimit_eq_iff _ (colimit.isColimit F)
 
+open IsFiltered in
+variable {F} in
+lemma jointly_surjective_of_isColimit₂
+    {t : Cocone F} (ht : IsColimit t) (x₁ x₂ : t.pt) :
+    ∃ (j : J) (x₁' x₂' : F.obj j), t.ι.app j x₁' = x₁ ∧ t.ι.app j x₂' = x₂ := by
+  obtain ⟨j₁, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₁
+  obtain ⟨j₂, x₂, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₂
+  exact ⟨max j₁ j₂, F.map (leftToMax _ _) x₁, F.map (rightToMax _ _) x₂,
+    congr_fun (t.w (leftToMax j₁ j₂)) x₁, congr_fun (t.w (rightToMax j₁ j₂)) x₂⟩
+
 end CategoryTheory.Limits.Types.FilteredColimit
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean
index 77d45f0447dc20..fc3aff663c7eae 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@@ -125,6 +125,8 @@ variable (P : MorphismProperty C)
 /-- The set in `Set (Arrow C)` which corresponds to `P : MorphismProperty C`. -/
 def toSet : Set (Arrow C) := setOf (fun f ↦ P f.hom)
 
+lemma mem_toSet_iff (f : Arrow C) : f ∈ P.toSet ↔ P f.hom := Iff.rfl
+
 /-- The family of morphisms indexed by `P.toSet` which corresponds
 to `P : MorphismProperty C`, see `MorphismProperty.ofHoms_homFamily`. -/
 def homFamily (f : P.toSet) : f.1.left ⟶ f.1.right := f.1.hom
diff --git a/Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean b/Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
index b3119203920c5c..63c33f6e234eda 100644
--- a/Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
+++ b/Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
@@ -74,6 +74,10 @@ instance : IsClosedUnderIsomorphisms (isoClosure P) where
     rintro X Y e ⟨Z, hZ, ⟨f⟩⟩
     exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩
 
+lemma isClosedUnderIsomorphisms_iff_isoClosure_eq_self :
+    IsClosedUnderIsomorphisms P ↔ isoClosure P = P :=
+  ⟨fun _ ↦ isoClosure_eq_self _, fun h ↦ by rw [← h]; infer_instance⟩
+
 instance (F : C ⥤ D) : IsClosedUnderIsomorphisms (P.map F) where
   of_iso := by
     rintro _ _ e ⟨X, hX, ⟨e'⟩⟩
diff --git a/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean
new file mode 100644
index 00000000000000..4009739895be12
--- /dev/null
+++ b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
+import Mathlib.Order.CompleteLattice.Basic
+
+/-!
+# ObjectProperty is a complete lattice
+
+-/
+
+universe v u
+
+namespace CategoryTheory.ObjectProperty
+
+variable {C : Type u} [Category.{v} C]
+
+example : CompleteLattice (ObjectProperty C) := inferInstance
+
+section
+
+variable (P Q : ObjectProperty C) (X : C)
+
+@[simp high] lemma prop_inf_iff : (P ⊓ Q) X ↔ P X ∧ Q X := Iff.rfl
+
+@[simp high] lemma prop_sup_iff : (P ⊔ Q) X ↔ P X ∨ Q X := Iff.rfl
+
+lemma isoClosure_sup : (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure := by
+  ext X
+  simp only [prop_sup_iff]
+  constructor
+  · rintro ⟨Y, hY, ⟨e⟩⟩
+    simp only [prop_sup_iff] at hY
+    obtain hY | hY := hY
+    · exact Or.inl ⟨Y, hY, ⟨e⟩⟩
+    · exact Or.inr ⟨Y, hY, ⟨e⟩⟩
+  · rintro (hY | hY)
+    · exact monotone_isoClosure le_sup_left _ hY
+    · exact monotone_isoClosure le_sup_right _ hY
+
+instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
+    (P ⊔ Q).IsClosedUnderIsomorphisms := by
+  simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self, isoClosure_sup, isoClosure_eq_self]
+
+end
+
+section
+
+variable {α : Sort*} (P : α → ObjectProperty C) (X : C)
+
+@[simp high] lemma prop_iSup_iff :
+    (⨆ (a : α), P a) X ↔ ∃ (a : α), P a X := by simp
+
+lemma isoClosure_iSup :
+    ((⨆ (a : α), P a)).isoClosure = ⨆ (a : α), (P a).isoClosure := by
+  refine le_antisymm ?_ ?_
+  · rintro X ⟨Y, hY, ⟨e⟩⟩
+    simp only [prop_iSup_iff] at hY ⊢
+    obtain ⟨a, hY⟩ := hY
+    exact ⟨a, _, hY, ⟨e⟩⟩
+  · simp only [iSup_le_iff]
+    intro a
+    rw [isoClosure_le_iff]
+    exact (le_iSup P a).trans (le_isoClosure _)
+
+instance [∀ a, (P a).IsClosedUnderIsomorphisms] :
+    ((⨆ (a : α), P a)).IsClosedUnderIsomorphisms := by
+  simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self,
+    isoClosure_iSup, isoClosure_eq_self]
+
+end
+
+end CategoryTheory.ObjectProperty
diff --git a/Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean b/Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean
new file mode 100644
index 00000000000000..2e6fbc869a108e
--- /dev/null
+++ b/Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean
@@ -0,0 +1,215 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
+import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
+import Mathlib.Order.TransfiniteIteration
+import Mathlib.SetTheory.Cardinal.HasCardinalLT
+
+/-!
+# Closure of a property of objects under limits of certain shapes
+
+In this file, given a property `P` of objects in a category `C` and
+family of categories `J : α → Type _`, we introduce the closure
+`P.limitsClosure J` of `P` under limits of shapes `J a` for all `a : α`,
+and under certain smallness assumptions, we show that its essentially small.
+
+-/
+universe w w' t v' u' v u
+
+namespace CategoryTheory.ObjectProperty
+
+open Limits
+
+variable {C : Type u} [Category.{v} C] (P : ObjectProperty C)
+  {α : Type t} (J : α → Type u') [∀ a, Category.{v'} (J a)]
+
+/-- The closure of property of objects of a category under limits of
+shape `J a` for a family of categories `J`. -/
+inductive limitsClosure : ObjectProperty C
+  | of_mem (X : C) (hX : P X) : limitsClosure X
+  | of_isoClosure {X Y : C} (e : X ≅ Y) (hX : limitsClosure X) : limitsClosure Y
+  | of_limitPresentation {X : C} {a : α} (pres : LimitPresentation (J a) X)
+      (h : ∀ j, limitsClosure (pres.diag.obj j)) : limitsClosure X
+
+@[simp]
+lemma le_limitsClosure : P ≤ P.limitsClosure J :=
+  fun X hX ↦ .of_mem X hX
+
+instance : (P.limitsClosure J).IsClosedUnderIsomorphisms where
+  of_iso e hX := .of_isoClosure e hX
+
+instance (a : α) : (P.limitsClosure J).IsClosedUnderLimitsOfShape (J a) where
+  limitsOfShape_le := by
+    rintro X ⟨hX⟩
+    exact .of_limitPresentation hX.toLimitPresentation hX.prop_diag_obj
+
+variable {P J} in
+lemma limitsClosure_le {Q : ObjectProperty C} [Q.IsClosedUnderIsomorphisms]
+    [∀ (a : α), Q.IsClosedUnderLimitsOfShape (J a)] (h : P ≤ Q) :
+    P.limitsClosure J ≤ Q := by
+  intro X hX
+  induction hX with
+  | of_mem X hX => exact h _ hX
+  | of_isoClosure e hX hX' => exact Q.prop_of_iso e hX'
+  | of_limitPresentation pres h h' => exact Q.prop_of_isLimit pres.isLimit h'
+
+variable {P} in
+lemma limitsClosure_monotone {Q : ObjectProperty C} (h : P ≤ Q) :
+    P.limitsClosure J ≤ Q.limitsClosure J :=
+  limitsClosure_le (h.trans (Q.le_limitsClosure J))
+
+lemma limitsClosure_isoClosure :
+    P.isoClosure.limitsClosure J = P.limitsClosure J := by
+  refine le_antisymm (limitsClosure_le ?_)
+    (limitsClosure_monotone _ P.le_isoClosure)
+  rw [isoClosure_le_iff]
+  exact le_limitsClosure P J
+
+/-- Given `P : ObjectProperty C` and a family of categories `J : α → Type _`,
+this property objects contains `P` and all objects that are equal to `lim F`
+for some functor `F : J a ⥤ C` such that `F.obj j` satisfies `P` for any `j`. -/
+def strictLimitsClosureStep : ObjectProperty C :=
+  P ⊔ (⨆ (a : α), P.strictLimitsOfShape (J a))
+
+@[simp]
+lemma le_strictLimitsClosureStep : P ≤ P.strictLimitsClosureStep J := le_sup_left
+
+variable {P} in
+lemma strictLimitsClosureStep_monotone {Q : ObjectProperty C} (h : P ≤ Q) :
+    P.strictLimitsClosureStep J ≤ Q.strictLimitsClosureStep J := by
+  dsimp [strictLimitsClosureStep]
+  simp only [sup_le_iff, iSup_le_iff]
+  exact ⟨h.trans le_sup_left, fun a ↦ (strictLimitsOfShape_monotone (J a) h).trans
+    (le_trans (by rfl) ((le_iSup _ a).trans le_sup_right))⟩
+
+section
+
+variable {β : Type w'} [LinearOrder β] [OrderBot β] [SuccOrder β] [WellFoundedLT β]
+
+/-- Given `P : ObjectProperty C`, a family of categories `J a`, this
+is the transfinite iteration of `Q ↦ Q.strictLimitsClosureStep J`. -/
+abbrev strictLimitsClosureIter (b : β) : ObjectProperty C :=
+  transfiniteIterate (φ := fun Q ↦ Q.strictLimitsClosureStep J) b P
+
+lemma le_strictLimitsClosureIter (b : β) :
+    P ≤ P.strictLimitsClosureIter J b :=
+  le_of_eq_of_le (transfiniteIterate_bot _ _).symm
+    (monotone_transfiniteIterate _ _ (fun _ ↦ le_strictLimitsClosureStep _ _) bot_le)
+
+lemma strictLimitsClosureIter_le_limitsClosure (b : β) :
+    P.strictLimitsClosureIter J b ≤ P.limitsClosure J := by
+  induction b using SuccOrder.limitRecOn with
+  | isMin b hb =>
+    obtain rfl := hb.eq_bot
+    simp
+  | succ b hb hb' =>
+    rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
+      strictLimitsClosureStep, sup_le_iff, iSup_le_iff]
+    exact ⟨hb', fun a ↦ ((strictLimitsOfShape_le_limitsOfShape _ _).trans
+      (limitsOfShape_monotone _ hb')).trans (limitsOfShape_le _ _)⟩
+  | isSuccLimit b hb hb' =>
+    simp only [transfiniteIterate_limit _ _ _ hb,
+      iSup_le_iff, Subtype.forall, Set.mem_Iio]
+    intro c hc
+    exact hb' _ hc
+
+instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} α]
+    [∀ a, Small.{w} (J a)] [∀ a, LocallySmall.{w} (J a)] (b : β)
+    [hb₀ : Small.{w} (Set.Iio b)] :
+    ObjectProperty.Small.{w} (P.strictLimitsClosureIter J b) := by
+  have H {b c : β} (hbc : b ≤ c) [Small.{w} (Set.Iio c)] : Small.{w} (Set.Iio b) :=
+    small_of_injective (f := fun x ↦ (⟨x.1, lt_of_lt_of_le x.2 hbc⟩ : Set.Iio c))
+      (fun _ _ _ ↦ by aesop)
+  induction b using SuccOrder.limitRecOn generalizing hb₀ with
+  | isMin b hb =>
+    obtain rfl := hb.eq_bot
+    simp only [transfiniteIterate_bot]
+    infer_instance
+  | succ b hb hb' =>
+    have := H (Order.le_succ b)
+    rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
+      strictLimitsClosureStep]
+    infer_instance
+  | isSuccLimit b hb hb' =>
+    simp only [transfiniteIterate_limit _ _ _ hb]
+    have (c : Set.Iio b) : ObjectProperty.Small.{w}
+      (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) c.1 P) := by
+      have := H c.2.le
+      exact hb' c.1 c.2
+    infer_instance
+
+end
+
+section
+
+variable (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (a : α), HasCardinalLT (J a) κ)
+
+include h
+
+lemma strictLimitsClosureStep_strictLimitsClosureIter_eq_self :
+    (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J =
+      (P.strictLimitsClosureIter J κ.ord) := by
+  have hκ : κ.IsRegular := Fact.out
+  have (a : α) := (h a).small
+  refine le_antisymm (fun X hX ↦ ?_) (le_strictLimitsClosureStep _ _)
+  simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff] at hX
+  obtain (hX | ⟨a, F, hF⟩) := hX
+  · exact hX
+  · simp only [strictLimitsClosureIter, transfiniteIterate_limit _ _ _
+      (Cardinal.isSuccLimit_ord hκ.aleph0_le), prop_iSup_iff,
+      Subtype.exists, Set.mem_Iio, exists_prop] at hF
+    choose o ho ho' using hF
+    obtain ⟨m, hm, hm'⟩ : ∃ (m : Ordinal.{w}) (hm : m < κ.ord), ∀ (j : J a), o j ≤ m := by
+      refine ⟨⨆ j, o ((equivShrink.{w} (J a)).symm j),
+          Ordinal.iSup_lt_ord ?_ (fun _ ↦ ho _), fun j ↦ ?_⟩
+      · rw [hκ.cof_eq, ← hasCardinalLT_iff_cardinal_mk_lt _ κ,
+          ← hasCardinalLT_iff_of_equiv (equivShrink.{w} (J a))]
+        exact h a
+      · obtain ⟨j, rfl⟩ := (equivShrink.{w} (J a)).symm.surjective j
+        exact le_ciSup (Ordinal.bddAbove_range _) _
+    refine monotone_transfiniteIterate _ _
+      (fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J) (Order.succ_le_iff.2 hm) _ ?_
+    dsimp
+    rw [transfiniteIterate_succ _ _ _ (by simp)]
+    simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff]
+    exact Or.inr ⟨a, ⟨_, fun j ↦ monotone_transfiniteIterate _ _
+      (fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J)  (hm' j) _ (ho' j)⟩⟩
+
+lemma isoClosure_strictLimitsClosureIter_eq_limitsClosure :
+    (P.strictLimitsClosureIter J κ.ord).isoClosure = P.limitsClosure J := by
+  refine le_antisymm ?_ ?_
+  · rw [isoClosure_le_iff]
+    exact P.strictLimitsClosureIter_le_limitsClosure J κ.ord
+  · have (a : α) :
+        (P.strictLimitsClosureIter J κ.ord).isoClosure.IsClosedUnderLimitsOfShape (J a) := ⟨by
+      conv_rhs => rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]
+      rw [limitsOfShape_isoClosure, ← isoClosure_strictLimitsOfShape,
+        strictLimitsClosureStep]
+      exact monotone_isoClosure ((le_trans (by rfl) (le_iSup _ a)).trans le_sup_right)⟩
+    refine limitsClosure_le
+      ((P.le_strictLimitsClosureIter J κ.ord).trans (le_isoClosure _))
+
+lemma isEssentiallySmall_limitsClosure
+    [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] [Small.{w} α]
+    [∀ a, Small.{w} (J a)] [∀ a, LocallySmall.{w} (J a)] :
+    ObjectProperty.EssentiallySmall.{w} (P.limitsClosure J) := by
+  obtain ⟨Q, hQ, hQ₁, hQ₂⟩ := EssentiallySmall.exists_small_le.{w} P
+  have : ObjectProperty.EssentiallySmall.{w} (Q.isoClosure.limitsClosure J) := by
+    rw [limitsClosure_isoClosure,
+      ← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h]
+    infer_instance
+  exact .of_le (limitsClosure_monotone J hQ₂)
+
+end
+
+instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] [Small.{w} α]
+    [∀ a, Small.{w} (J a)] [∀ a, LocallySmall.{w} (J a)] :
+    ObjectProperty.EssentiallySmall.{w} (P.limitsClosure J) := by
+  obtain ⟨κ, h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall J
+  have : Fact κ.IsRegular := ⟨h₁⟩
+  exact isEssentiallySmall_limitsClosure P J κ h₂
+
+end CategoryTheory.ObjectProperty
diff --git a/Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean b/Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean
index c038dea4401a51..54911ac43aa62f 100644
--- a/Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean
+++ b/Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean
@@ -144,6 +144,11 @@ instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} J] [Locall
   rintro ⟨_, ⟨F, hF⟩⟩
   exact ⟨⟨P.lift F hF, by assumption⟩, rfl⟩
 
+instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} J] [LocallySmall.{w} J] :
+    ObjectProperty.EssentiallySmall.{w} (P.limitsOfShape J) := by
+  rw [← isoClosure_strictLimitsOfShape]
+  infer_instance
+
 /-- A property of objects satisfies `P.IsClosedUnderLimitsOfShape J` if it
 is stable by limits of shape `J`. -/
 @[mk_iff]
diff --git a/Mathlib/CategoryTheory/ObjectProperty/Small.lean b/Mathlib/CategoryTheory/ObjectProperty/Small.lean
index 291fd3a2125b5f..0ca7e80c945c97 100644
--- a/Mathlib/CategoryTheory/ObjectProperty/Small.lean
+++ b/Mathlib/CategoryTheory/ObjectProperty/Small.lean
@@ -3,6 +3,7 @@ Copyright (c) 2025 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
+import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
 import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
 import Mathlib.CategoryTheory.ObjectProperty.Opposite
 import Mathlib.Logic.Small.Basic
@@ -50,4 +51,97 @@ instance (X Y : C) : ObjectProperty.Small.{w} (.pair X Y) := by
   dsimp [pair]
   infer_instance
 
+instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} Q] :
+    ObjectProperty.Small.{w} (P ⊓ Q) :=
+  Small.of_le inf_le_right
+
+instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} P] :
+    ObjectProperty.Small.{w} (P ⊓ Q) :=
+  Small.of_le inf_le_left
+
+instance {P Q : ObjectProperty C} [ObjectProperty.Small.{w} P] [ObjectProperty.Small.{w} Q] :
+    ObjectProperty.Small.{w} (P ⊔ Q) :=
+  small_of_surjective (f := fun (x : Subtype P ⊕ Subtype Q) ↦ match x with
+      | .inl x => ⟨x.1, Or.inl x.2⟩
+      | .inr x => ⟨x.1, Or.inr x.2⟩)
+    (by rintro ⟨x, hx | hx⟩ <;> aesop)
+
+instance {α : Type*} (P : α → ObjectProperty C)
+    [∀ a, ObjectProperty.Small.{w} (P a)] [Small.{w} α] :
+    ObjectProperty.Small.{w} (⨆ a, P a) :=
+  small_of_surjective (f := fun (x : Σ a, Subtype (P a)) ↦ ⟨x.2.1, by aesop⟩)
+    (fun ⟨x, hx⟩ ↦ by aesop)
+
+/-- A property of objects is essentially small relative to a universe `w`
+if it is contained in the closure by isomorphisms of a small property. -/
+@[pp_with_univ]
+protected class EssentiallySmall (P : ObjectProperty C) : Prop where
+  exists_small_le' (P) : ∃ (Q : ObjectProperty C) (_ : ObjectProperty.Small.{w} Q),
+    P ≤ Q.isoClosure
+
+lemma EssentiallySmall.exists_small_le (P : ObjectProperty C)
+    [ObjectProperty.EssentiallySmall.{w} P] :
+    ∃ (Q : ObjectProperty C) (_ : ObjectProperty.Small.{w} Q), Q ≤ P ∧ P ≤ Q.isoClosure := by
+  obtain ⟨Q, _, hQ⟩ := exists_small_le' P
+  let P' := Q ⊓ P.isoClosure
+  have h (X' : Subtype P') : ∃ (X : Subtype P), Nonempty (X'.1 ≅ X.1) :=
+    ⟨⟨X'.2.2.choose, X'.2.2.choose_spec.choose⟩, X'.2.2.choose_spec.choose_spec⟩
+  choose φ hφ using h
+  refine ⟨fun X ↦ X ∈ Set.range (Subtype.val ∘ φ), ?_, ?_, ?_⟩
+  · exact small_of_surjective (f := fun X ↦ ⟨(φ X).1, by tauto⟩)
+      (by rintro ⟨_, Z, rfl⟩; exact ⟨Z, rfl⟩)
+  · intro X hX
+    simp only [Set.mem_range, Function.comp_apply, Subtype.exists] at hX
+    obtain ⟨Y, hY, rfl⟩ := hX
+    exact (φ ⟨Y, hY⟩).2
+  · intro X hX
+    obtain ⟨Y, hY, ⟨e⟩⟩ := hQ _ hX
+    let Z : Subtype P' := ⟨Y, hY, ⟨X, hX, ⟨e.symm⟩⟩⟩
+    exact ⟨_, ⟨Z, rfl⟩, ⟨e ≪≫ (hφ Z).some⟩⟩
+
+instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] :
+    ObjectProperty.EssentiallySmall.{w} P where
+  exists_small_le' := ⟨P, inferInstance, le_isoClosure P⟩
+
+instance (P : ObjectProperty C) [ObjectProperty.EssentiallySmall.{w} P] :
+    ObjectProperty.EssentiallySmall.{w} P.isoClosure where
+  exists_small_le' := by
+    obtain ⟨Q, _, _, _⟩ := EssentiallySmall.exists_small_le.{w} P
+    exact ⟨Q, inferInstance, by rwa [isoClosure_le_iff]⟩
+
+lemma EssentiallySmall.exists_small (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms]
+    [ObjectProperty.EssentiallySmall.{w} P] :
+    ∃ (P₀ : ObjectProperty C) (_ : ObjectProperty.Small.{w} P₀), P = P₀.isoClosure := by
+  obtain ⟨Q, _, hQ₁, hQ₂⟩ := exists_small_le P
+  exact ⟨Q, inferInstance, le_antisymm hQ₂ (by rwa [isoClosure_le_iff])⟩
+
+lemma EssentiallySmall.of_le {P Q : ObjectProperty C}
+    [ObjectProperty.EssentiallySmall.{w} Q] (h : P ≤ Q) :
+    ObjectProperty.EssentiallySmall.{w} P where
+  exists_small_le' := by
+    obtain ⟨R, _, hR⟩ := EssentiallySmall.exists_small_le' Q
+    exact ⟨R, inferInstance, h.trans hR⟩
+
+instance {P Q : ObjectProperty C}
+    [ObjectProperty.EssentiallySmall.{w} P] [ObjectProperty.EssentiallySmall.{w} Q] :
+    ObjectProperty.EssentiallySmall.{w} (P ⊔ Q) := by
+  obtain ⟨P', _, hP'⟩ := EssentiallySmall.exists_small_le' P
+  obtain ⟨Q', _, hQ'⟩ := EssentiallySmall.exists_small_le' Q
+  refine ⟨P' ⊔ Q', inferInstance, ?_⟩
+  simp only [sup_le_iff]
+  constructor
+  · exact hP'.trans (monotone_isoClosure le_sup_left)
+  · exact hQ'.trans (monotone_isoClosure le_sup_right)
+
+instance {α : Type*} (P : α → ObjectProperty C)
+    [∀ a, ObjectProperty.EssentiallySmall.{w} (P a)] [Small.{w} α] :
+    ObjectProperty.EssentiallySmall.{w} (⨆ a, P a) where
+  exists_small_le' := by
+    have h (a : α) := EssentiallySmall.exists_small_le' (P a)
+    choose Q _ hQ using h
+    refine ⟨⨆ a, Q a, inferInstance, ?_⟩
+    simp only [iSup_le_iff]
+    intro a
+    exact (hQ a).trans (monotone_isoClosure (le_iSup Q a))
+
 end CategoryTheory.ObjectProperty
diff --git a/Mathlib/CategoryTheory/Presentable/Basic.lean b/Mathlib/CategoryTheory/Presentable/Basic.lean
index eead4b228e6558..058150811d5f18 100644
--- a/Mathlib/CategoryTheory/Presentable/Basic.lean
+++ b/Mathlib/CategoryTheory/Presentable/Basic.lean
@@ -106,6 +106,13 @@ when the functor `Hom(X, _)` preserves colimits indexed by
 `κ`-filtered categories. -/
 abbrev IsCardinalPresentable : Prop := (coyoneda.obj (op X)).IsCardinalAccessible κ
 
+variable (C) in
+/-- The property of objects that are `κ`-presentable. -/
+def isCardinalPresentable : ObjectProperty C := fun X ↦ IsCardinalPresentable X κ
+
+lemma isCardinalPresentable_iff (X : C) :
+    isCardinalPresentable C κ X ↔ IsCardinalPresentable X κ := Iff.rfl
+
 lemma preservesColimitsOfShape_of_isCardinalPresentable [IsCardinalPresentable X κ]
     (J : Type w) [SmallCategory.{w} J] [IsCardinalFiltered J κ] :
     PreservesColimitsOfShape J (coyoneda.obj (op X)) :=
@@ -123,11 +130,23 @@ lemma isCardinalPresentable_of_le [IsCardinalPresentable X κ]
     IsCardinalPresentable X κ' :=
   (coyoneda.obj (op X)).isCardinalAccessible_of_le h
 
+variable (C) {κ} in
+lemma isCardinalPresentable_monotone {κ' : Cardinal.{w}} [Fact κ'.IsRegular] (h : κ ≤ κ') :
+    isCardinalPresentable C κ ≤ isCardinalPresentable C κ' := by
+  intro X hX
+  rw [isCardinalPresentable_iff] at hX ⊢
+  exact isCardinalPresentable_of_le _ h
+
 include e in
 variable {X Y} in
 lemma isCardinalPresentable_of_iso [IsCardinalPresentable X κ] : IsCardinalPresentable Y κ :=
   Functor.isCardinalAccessible_of_natIso (coyoneda.mapIso e.symm.op) κ
 
+instance : (isCardinalPresentable C κ).IsClosedUnderIsomorphisms where
+  of_iso e hX := by
+    rw [isCardinalPresentable_iff] at hX ⊢
+    exact isCardinalPresentable_of_iso e _
+
 lemma isCardinalPresentable_of_equivalence
     {C' : Type u₃} [Category.{v₃} C'] [IsCardinalPresentable X κ] (e : C ≌ C') :
     IsCardinalPresentable (e.functor.obj X) κ := by
diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
new file mode 100644
index 00000000000000..232db26dab9900
--- /dev/null
+++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Limits.FullSubcategory
+import Mathlib.Order.Category.PartOrdEmb
+import Mathlib.CategoryTheory.Presentable.Directed
+import Mathlib.CategoryTheory.Presentable.LocallyPresentable
+
+/-!
+# The κ-accessible category of κ-directed posets
+
+Given a regular cardinal `κ : Cardinal.{u}`, we define the
+category `CardinalFilteredPoset κ` of `κ`-directed partially ordered
+types (with order embeddings as morphisms), and we show that it is
+a `κ`-accessible category.
+
+-/
+
+universe u
+
+open CategoryTheory Limits
+
+namespace PartOrdEmb
+
+variable (κ : Cardinal.{u}) [Fact κ.IsRegular]
+
+/-- The property of objects in `PartOrdEmb` that are
+satisfied by partially ordered types of cardinality `< κ`. -/
+abbrev isCardinalFiltered : ObjectProperty PartOrdEmb.{u} :=
+    fun X ↦ IsCardinalFiltered X κ
+
+@[simp]
+lemma isCardinalFiltered_iff (X : PartOrdEmb.{u}) :
+    isCardinalFiltered κ X ↔ IsCardinalFiltered X κ := Iff.rfl
+
+instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms where
+  of_iso e _ := .of_equivalence κ (orderIsoOfIso e).equivalence
+
+namespace Limits.CoconePt
+
+variable {κ} {J : Type u} [SmallCategory J] [IsCardinalFiltered J κ]
+  {F : J ⥤ PartOrdEmb.{u}} {c : Cocone (F ⋙ forget _)} (hc : IsColimit c)
+
+lemma isCardinalFiltered_pt (hF : ∀ j, IsCardinalFiltered (F.obj j) κ) :
+    letI := isFiltered_of_isCardinalFiltered J κ
+    IsCardinalFiltered (CoconePt hc) κ := by
+  letI := isFiltered_of_isCardinalFiltered J κ
+  refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_)
+  rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
+  choose j₀ x₀ hx₀ using fun k ↦ Types.jointly_surjective_of_isColimit hc (f k)
+  let j := IsCardinalFiltered.max j₀ hK
+  let x₁ (k : K) : F.obj j := F.map (IsCardinalFiltered.toMax j₀ hK k) (x₀ k)
+  have hx₁ (k : K) : c.ι.app j (x₁ k) = c.ι.app (j₀ k) (x₀ k) :=
+    congr_fun (c.w (IsCardinalFiltered.toMax j₀ hK k))  _
+  refine ⟨(cocone hc).ι.app j (IsCardinalFiltered.max x₁ hK),
+    fun k ↦ ?_⟩
+  rw [← hx₀, ← hx₁]
+  exact ((cocone hc).ι.app j).hom.monotone
+    (leOfHom (IsCardinalFiltered.toMax x₁ hK k))
+
+end Limits.CoconePt
+
+instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] :
+    (isCardinalFiltered κ).IsClosedUnderColimitsOfShape J where
+  colimitsOfShape_le := by
+    have := isFiltered_of_isCardinalFiltered J κ
+    rintro X ⟨p⟩
+    have hc := colimit.isColimit (p.diag ⋙ forget PartOrdEmb)
+    simp only [(isCardinalFiltered κ).prop_iff_of_iso
+      (p.isColimit.coconePointUniqueUpToIso
+        (Limits.isColimitCocone (colimit.isColimit (p.diag ⋙ forget PartOrdEmb)))),
+      isCardinalFiltered_iff, Limits.cocone_pt_coe]
+    exact Limits.CoconePt.isCardinalFiltered_pt _ p.prop_diag_obj
+
+end PartOrdEmb
+
+namespace CategoryTheory
+
+variable (κ : Cardinal.{u}) [Fact κ.IsRegular]
+
+/-- The category of `κ`-filtered partially ordered types,
+with morphisms given by order embeddings. -/
+abbrev CardinalFilteredPoset :=
+  (PartOrdEmb.isCardinalFiltered κ).FullSubcategory
+
+variable {κ} in
+/-- The embedding of the category of `κ`-filtered
+partially ordered types in the category of partially
+ordered types. -/
+abbrev CardinalFilteredPoset.ι :
+    CardinalFilteredPoset κ ⥤ PartOrdEmb :=
+  ObjectProperty.ι _
+
+instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ where
+  hasColimitsOfShape J _ _ := by
+    have := isFiltered_of_isCardinalFiltered J κ
+    infer_instance
+
+instance : IsCardinalAccessibleCategory (CardinalFilteredPoset κ) κ where
+  exists_generator := sorry
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean b/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean
index 1c5007f138f6ec..50812a21fe688a 100644
--- a/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean
+++ b/Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean
@@ -3,26 +3,25 @@ Copyright (c) 2025 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
+import Mathlib.CategoryTheory.ObjectProperty.Small
 import Mathlib.CategoryTheory.Presentable.Limits
-import Mathlib.CategoryTheory.Limits.Presentation
+import Mathlib.CategoryTheory.Generator.StrongGenerator
 
 /-!
 # Presentable generators
 
-Let `C` be a category, `G : ι → C` a family of objects and `κ` a regular cardinal
-(with `ι` and `κ` both in the same universe `w`). In this file, we
-introduce a property `h : AreCardinalFilteredGenerators G κ`:
-this property says that the objects `G i` are all `κ`-presentable and that
-any object in `C` identifies as a `κ`-filtered colimit of these objects.
-We show in the lemma `AreCardinalFilteredGenerators.presentable` that it
-follows that any object `X` is presentable (relatively to a possibly
-larger regular cardinal `κ'`).
-
-Finally, we define a typeclass `HasCardinalFilteredGenerators C κ` saying
-that `C` is locally `w`-small and that there exists a family `G : ι → C`
-indexed by `ι : Type w` such that `AreCardinalFilteredGenerators G κ` holds.
-This is used in the definition of locally presentable and accessible
-categories in the file `CategoryTheory.Presentable.LocallyPresentable`.
+Let `C` be a category, a regular cardinal `κ` and `P : ObjectProperty C`.
+We define a predicate `P.IsCardinalFilteredGenerator κ` saying that
+`P` consists of `κ`-presentable objects and that any objects in `C`
+is a `κ`-filtered colimit of objects satisfying `P`.
+We show that if this condition is satisfied, then `P` is a strong generator
+(see `IsCardinalFilteredGenerator.isStrongGenerator`). Moreover,
+if `C` is locally small, we show that any object in `C` is presentable
+(see `IsCardinalFilteredGenerator.presentable`).
+
+Finally, we define a typeclass `HasCardinalFilteredGenerator C κ` saying
+that `C` is locally `w`-small and that there exists an (essentially) small `P`
+such that `P.IsCardinalFilteredGenerator κ` holds.
 
 ## References
 * [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994]
@@ -50,81 +49,108 @@ end Limits.ColimitPresentation
 
 open Limits
 
-section
-
-variable {ι : Type w} (G : ι → C) (κ : Cardinal.{w}) [Fact κ.IsRegular]
-
-/-- Given a regular cardinal `κ`, this is the property that a family
-of objects `G : ι → C` consists of `κ`-presentable objects and that any
-object in `C` identifies to a `κ`-filtered colimit of these objects. -/
-structure AreCardinalFilteredGenerators : Prop where
-  isCardinalPresentable (i : ι) : IsCardinalPresentable (G i) κ
-  exists_colimitPresentation (X : C) :
-    ∃ (J : Type w) (_ : SmallCategory J) (_ : IsCardinalFiltered J κ)
-      (p : ColimitPresentation J X),
-        ∀ (j : J), ∃ (i : ι), Nonempty (p.diag.obj j ≅ G i)
+namespace ObjectProperty
 
-namespace AreCardinalFilteredGenerators
+variable {P : ObjectProperty C}
 
-variable {G κ} (h : AreCardinalFilteredGenerators G κ) (X : C)
-
-/-- When `G : ι → C` is a family of objects such that `AreCardinalFilteredGenerators G κ`
-holds, and `X : C`, this is the index category of a presentation of `X`
-as a `κ`-filtered colimit of objects in the family `G`. -/
-def J : Type w := (h.exists_colimitPresentation X).choose
+lemma ColimitOfShape.isCardinalPresentable {X : C} {J : Type w} [SmallCategory J]
+    (p : P.ColimitOfShape J X) {κ : Cardinal.{w}} [Fact κ.IsRegular]
+    (hP : P ≤ isCardinalPresentable C κ) [LocallySmall.{w} C]
+    (κ' : Cardinal.{w}) [Fact κ'.IsRegular] (h : κ ≤ κ')
+    (hJ : HasCardinalLT (Arrow J) κ') :
+    IsCardinalPresentable X κ' :=
+  p.toColimitPresentation.isCardinalPresentable κ
+    (fun j ↦ hP _ (p.prop_diag_obj j)) _ h hJ
 
-noncomputable instance : SmallCategory (h.J X) :=
-  (h.exists_colimitPresentation X).choose_spec.choose
+variable {κ : Cardinal.{w}} [Fact κ.IsRegular]
 
-noncomputable instance : IsCardinalFiltered (h.J X) κ :=
-  (h.exists_colimitPresentation X).choose_spec.choose_spec.choose
+variable (P κ) in
+/-- The condition that `P : ObjectProperty C` consists of `κ`-presentable objects
+and that any object of `C` is a `κ`-filtered colimit of objects satisfying `P`.
+(This notion is particularly relevant when `C` is locally `w`-small and `P` is
+essentially `w`-small, see `HasCardinalFilteredGenerators`, which appears in
+the definitions of locally presentable and accessible categories.) -/
+structure IsCardinalFilteredGenerator : Prop where
+  le_isCardinalPresentable : P ≤ isCardinalPresentable C κ
+  exists_colimitsOfShape (X : C) :
+    ∃ (J : Type w) (_ : SmallCategory J) (_ : IsCardinalFiltered J κ),
+      P.colimitsOfShape J X
 
-/-- A choice of a presentation of an object `X` in a category `C`
-as a `κ`-filtered colimit of objects in the family `G : ι → C`
-when `h : AreCardinalFilteredGenerators G κ`. -/
-noncomputable def colimitPresentation : ColimitPresentation (h.J X) X :=
-  (h.exists_colimitPresentation X).choose_spec.choose_spec.choose_spec.choose
+namespace IsCardinalFilteredGenerator
 
-lemma exists_colimitPresentation_diag_obj_iso (j : h.J X) :
-    ∃ (i : ι), Nonempty ((h.colimitPresentation X).diag.obj j ≅ G i) :=
-  (h.exists_colimitPresentation X).choose_spec.choose_spec.choose_spec.choose_spec j
+variable (h : P.IsCardinalFilteredGenerator κ) (X : C)
 
-instance (j : h.J X) :
-    IsCardinalPresentable.{w} ((h.colimitPresentation X).diag.obj j) κ := by
-  obtain ⟨i, ⟨e⟩⟩ := h.exists_colimitPresentation_diag_obj_iso X j
-  have := h.isCardinalPresentable
-  exact isCardinalPresentable_of_iso e.symm κ
+include h in
+lemma of_le_isoClosure {P' : ObjectProperty C} (h₁ : P ≤ P'.isoClosure)
+    (h₂ : P' ≤ isCardinalPresentable C κ) :
+    P'.IsCardinalFilteredGenerator κ where
+  le_isCardinalPresentable := h₂
+  exists_colimitsOfShape X := by
+    obtain ⟨J, _, _, hX⟩ := h.exists_colimitsOfShape X
+    exact ⟨J, inferInstance, inferInstance, by
+      simpa only [colimitsOfShape_isoClosure] using colimitsOfShape_monotone J h₁ _ hX⟩
 
 include h in
-lemma isPresentable (i : ι) : IsPresentable.{w} (G i) :=
-  have := h.isCardinalPresentable
-  isPresentable_of_isCardinalPresentable _ κ
+lemma isoClosure : P.isoClosure.IsCardinalFilteredGenerator κ :=
+  h.of_le_isoClosure (P.le_isoClosure.trans P.isoClosure.le_isoClosure)
+    (by simpa only [ObjectProperty.isoClosure_le_iff] using h.le_isCardinalPresentable)
 
-instance (j : h.J X) : IsPresentable.{w} ((h.colimitPresentation X).diag.obj j) :=
-  isPresentable_of_isCardinalPresentable _ κ
+lemma isoClosure_iff :
+    P.isoClosure.IsCardinalFilteredGenerator κ ↔ P.IsCardinalFilteredGenerator κ :=
+  ⟨fun h ↦ h.of_le_isoClosure (by rfl) (P.le_isoClosure.trans h.le_isCardinalPresentable),
+    isoClosure⟩
 
 include h in
-lemma presentable [LocallySmall.{w} C] (X : C) : IsPresentable.{w} X := by
+lemma presentable [LocallySmall.{w} C] (X : C) :
+    IsPresentable.{w} X := by
+  obtain ⟨J, _, _, ⟨hX⟩⟩ := h.exists_colimitsOfShape X
   obtain ⟨κ', _, le, hκ'⟩ : ∃ (κ' : Cardinal.{w}) (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'),
-      HasCardinalLT (Arrow (h.J X)) κ' := by
+      HasCardinalLT (Arrow J) κ' := by
     obtain ⟨κ', h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall.{w}
-      (Sum.elim (fun (_ : Unit) ↦ Arrow (h.J X)) (fun (_ : Unit) ↦ κ.ord.toType))
+      (Sum.elim (fun (_ : Unit) ↦ Arrow J) (fun (_ : Unit) ↦ κ.ord.toType))
     exact ⟨κ', ⟨h₁⟩,
       le_of_lt (by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)),
       h₂ (Sum.inl ⟨⟩)⟩
-  have := (h.colimitPresentation X).isCardinalPresentable κ (by infer_instance) κ' le hκ'
+  have := hX.isCardinalPresentable h.le_isCardinalPresentable _ le hκ'
   exact isPresentable_of_isCardinalPresentable _ κ'
 
-end AreCardinalFilteredGenerators
+include h in
+lemma isStrongGenerator : P.IsStrongGenerator :=
+  IsStrongGenerator.mk_of_exists_colimitsOfShape.{w} (fun X ↦ by
+    obtain ⟨_, _, _, hX⟩ := h.exists_colimitsOfShape X
+    exact ⟨_, _, hX⟩)
+
+end IsCardinalFilteredGenerator
 
-end
+end ObjectProperty
 
 /-- The property that a category `C` and a regular cardinal `κ`
-satisfy `AreCardinalFilteredGenerators G κ` for a suitable family
-of objects `G : ι → C`. -/
-class HasCardinalFilteredGenerators (C : Type u) [hC : Category.{v} C]
+satisfy `P.IsCardinalFilteredGenerators κ` for an suitable essentially
+small `P : ObjectProperty C`. -/
+class HasCardinalFilteredGenerator (C : Type u) [hC : Category.{v} C]
     (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] : Prop extends LocallySmall.{w} C where
-  exists_generators (C κ) [hC] [hκ] : ∃ (ι : Type w) (G : ι → C),
-    AreCardinalFilteredGenerators G κ
+  exists_generator (C κ) [hC] [hκ] :
+    ∃ (P : ObjectProperty C) (_ : ObjectProperty.EssentiallySmall.{w} P),
+      P.IsCardinalFilteredGenerator κ
+
+lemma ObjectProperty.IsCardinalFilteredGenerator.hasCardinalFilteredGenerator
+    {P : ObjectProperty C} [ObjectProperty.EssentiallySmall.{w} P]
+    [LocallySmall.{w} C] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
+    (hP : P.IsCardinalFilteredGenerator κ) :
+    HasCardinalFilteredGenerator C κ where
+  exists_generator := ⟨P, inferInstance, hP⟩
+
+lemma HasCardinalFilteredGenerator.exists_small_generator (C : Type u) [Category.{v} C]
+    (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasCardinalFilteredGenerator C κ] :
+    ∃ (P : ObjectProperty C) (_ : ObjectProperty.Small.{w} P),
+      P.IsCardinalFilteredGenerator κ := by
+  obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
+  obtain ⟨Q, _, h₁, h₂⟩ := ObjectProperty.EssentiallySmall.exists_small_le P
+  exact ⟨Q, inferInstance, hP.of_le_isoClosure h₂ (h₁.trans hP.le_isCardinalPresentable)⟩
+
+@[deprecated (since := "2025-10-12")] alias AreCardinalFilteredGenerators :=
+  ObjectProperty.IsCardinalFilteredGenerator
+@[deprecated (since := "2025-10-12")] alias HasCardinalFilteredGenerators :=
+  HasCardinalFilteredGenerator
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Presentable/Directed.lean b/Mathlib/CategoryTheory/Presentable/Directed.lean
new file mode 100644
index 00000000000000..4d330b69f83ab7
--- /dev/null
+++ b/Mathlib/CategoryTheory/Presentable/Directed.lean
@@ -0,0 +1,599 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Presentable.Basic
+import Mathlib.CategoryTheory.Limits.Final
+import Mathlib.CategoryTheory.MorphismProperty.Basic
+import Mathlib.CategoryTheory.Filtered.Final
+import Mathlib.CategoryTheory.Products.Unitor
+import Mathlib.Data.Finite.Sigma
+
+/-!
+# `κ`-filtered categories and `κ`-directed poset
+
+In this file, we formalize the proof by Deligne (SGA 4 I 8.1.6) that for
+any (small) filtered category `J`, there exists a final functor `F : α ⥤ J`
+where `α` is a directed partially ordered set (`IsFiltered.exists_directed`).
+The construction applies more generally to `κ`-filtered categories and
+`κ`-directed posets (`IsCardinalFiltered.exists_cardinal_directed`).
+
+Note: the argument by Deligne is reproduced (without reference) in the book
+by Adámek and Rosický (theorem 1.5), but with a mistake:
+the construction by Deligne involves considering diagrams
+(see `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal`)
+which are not necessarily *subcategories* (the class of morphisms `W` does not
+have to be multiplicative.)
+
+## References
+* [Alexander Grothendieck and Jean-Louis Verdier, *Exposé I : Préfaisceaux*,
+  SGA 4 I 8.1.6][sga-4-tome-1]
+* [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994]
+
+-/
+
+universe u v w
+
+lemma CategoryTheory.MorphismProperty.toSet_iSup {C : Type*} [Category C]
+    {ι : Type*} (W : ι → MorphismProperty C) :
+    (⨆ i , W i).toSet = ⋃ i, (W i).toSet := by
+  ext
+  simp [MorphismProperty.toSet]
+
+lemma CategoryTheory.MorphismProperty.toSet_max {C : Type*} [Category C]
+    (W₁ W₂ : MorphismProperty C) :
+    (W₁ ⊔ W₂).toSet = W₁.toSet ∪ W₂.toSet := rfl
+
+section
+
+open CategoryTheory Limits
+
+lemma hasCardinalLT_toSet_morphismPropertyOfHoms {C : Type*} [Category C]
+    {ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) {κ : Cardinal}
+    (h : HasCardinalLT ι κ) : HasCardinalLT (MorphismProperty.ofHoms f).toSet κ :=
+  h.of_surjective (fun i ↦ ⟨Arrow.mk (f i), ⟨i⟩⟩) (by
+    rintro ⟨f, hf⟩
+    rw [MorphismProperty.mem_toSet_iff, MorphismProperty.ofHoms_iff] at hf
+    obtain ⟨i, hf⟩ := hf
+    obtain rfl : f = _ := hf
+    exact ⟨i, rfl⟩)
+
+lemma hasCardinalLT_subtype_objectPropertyOfObj {C : Type*} [Category C]
+    {ι : Type*} (X : ι → C) {κ : Cardinal}
+    (h : HasCardinalLT ι κ) : HasCardinalLT (Subtype (ObjectProperty.ofObj X)) κ :=
+  h.of_surjective (fun i ↦ ⟨X i, by simp⟩) (by rintro ⟨_, ⟨i⟩⟩; exact ⟨i, rfl⟩)
+
+end
+
+namespace CategoryTheory
+
+open Limits
+
+namespace IsCardinalFiltered
+
+instance prod (J₁ J₂ : Type*) [Category J₁] [Category J₂]
+    (κ : Cardinal.{w}) [Fact κ.IsRegular]
+    [IsCardinalFiltered J₁ κ] [IsCardinalFiltered J₂ κ] :
+    IsCardinalFiltered (J₁ × J₂) κ where
+  nonempty_cocone {C _} F hC := ⟨by
+    let c₁ := cocone (F ⋙ Prod.fst _ _) hC
+    let c₂ := cocone (F ⋙ Prod.snd _ _) hC
+    exact
+      { pt := (c₁.pt, c₂.pt)
+        ι.app i := (c₁.ι.app i, c₂.ι.app i)
+        ι.naturality i j f := by
+          ext
+          · simpa using c₁.w f
+          · simpa using c₂.w f}⟩
+
+namespace exists_cardinal_directed
+
+variable (J : Type w) [SmallCategory J] (κ : Cardinal.{w})
+
+/-!
+Let `J` is a `κ`-filtered category. In order to construct a cofinal functor `α ⥤ J`
+with a `κ`-directed poset `α`, we first consider the case where there is no
+object `m : J` such that for any object `j : J`, there exists a map `j ⟶ m`.
+Under this assumption (`hJ`), the partially ordered type `DiagramWithUniqueTerminal J κ`
+of `κ`-bounded diagrams with a unique terminal object in `J` shall be a possible
+choice for `α`.
+-/
+
+/-- If `κ` is a cardinal, this structure contains the data of a `κ`-bounded diagram
+in a category `J`. -/
+@[ext]
+structure Diagram where
+  /-- the morphisms which belongs to the diagram -/
+  W : MorphismProperty J
+  /-- the objects in the diagram -/
+  P : ObjectProperty J
+  src {i j : J} {f : i ⟶ j} : W f → P i
+  tgt {i j : J} {f : i ⟶ j} : W f → P j
+  hW : HasCardinalLT W.toSet κ
+  hP : HasCardinalLT (Subtype P) κ
+
+namespace Diagram
+
+variable {J κ}
+
+/-- Given a `κ`-bounded diagram `D` in a category `J`, an object `e : J`
+is terminal if for any object `j` of `D`, there is a unique morphism `j ⟶ e` in `D`,
+that these unique morphisms are compatible with precomposition with morphims in `D`,
+and that `𝟙 e` belongs to `D`. -/
+structure IsTerminal (D : Diagram J κ) (e : J) where
+  prop_id : D.W (𝟙 e)
+  /-- the unique map to the terminal object in the diagram -/
+  lift {j : J} (hj : D.P j) : j ⟶ e
+  hlift {j : J} (hj : D.P j) : D.W (lift hj)
+  uniq {j : J} (hj : D.P j) {φ : j ⟶ e} (hφ : D.W φ) : lift hj = φ
+  comm {i j : J} (f : i ⟶ j) (hf : D.W f) : f ≫ lift (D.tgt hf) = lift (D.src hf)
+
+namespace IsTerminal
+
+attribute [reassoc] IsTerminal.comm
+
+variable {D : Diagram J κ} {e : J}
+
+lemma prop (h : D.IsTerminal e) : D.P e := D.src (h.prop_id)
+
+@[simp]
+lemma lift_self (h : D.IsTerminal e) : h.lift h.prop = 𝟙 e := h.uniq _ h.prop_id
+
+instance : Subsingleton (D.IsTerminal e) where
+  allEq h₁ h₂ := by
+    have : @h₁.lift = @h₂.lift := by
+      ext j hj
+      exact h₁.uniq hj (h₂.hlift hj)
+    cases h₁
+    cases h₂
+    aesop
+
+/-- Constructor for `Diagram.IsTerminal` for which no data is provided,
+but only its existence. -/
+noncomputable def ofExistsUnique (prop_id : D.W (𝟙 e))
+    (h₁ : ∀ ⦃j : J⦄ (_ : D.P j), ∃ (lift : j ⟶ e), D.W lift)
+    (h₂ : ∀ ⦃j : J⦄ (_ : D.P j) (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂)
+    (h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j) (_ : D.W f), ∃ (li : i ⟶ e) (lj : j ⟶ e),
+      D.W li ∧ D.W lj ∧ f ≫ lj = li) :
+    D.IsTerminal e where
+  prop_id := prop_id
+  lift hj := (h₁ hj).choose
+  hlift hj := (h₁ hj).choose_spec
+  uniq hj φ hφ := h₂ hj (h₁ hj).choose φ (h₁ hj).choose_spec hφ
+  comm _ hf := by
+    obtain ⟨li, lj, hli, hlj, fac⟩ := h₃ _ hf
+    rw [h₂ (D.src hf) _ li (h₁ (D.src hf)).choose_spec hli,
+      h₂ (D.tgt hf) _ lj (h₁ (D.tgt hf)).choose_spec hlj, fac]
+
+end IsTerminal
+
+end Diagram
+
+/-- If `κ` is a cardinal, this structure contains the data of a `κ`-bounded diagram
+with a unique terminal object in a category `J`. -/
+structure DiagramWithUniqueTerminal extends Diagram J κ where
+  /-- the terminal object -/
+  top : J
+  /-- `top` is terminal -/
+  isTerminal : toDiagram.IsTerminal top
+  uniq_terminal (j : J) (hj : toDiagram.IsTerminal j) : j = top
+
+@[ext]
+lemma DiagramWithUniqueTerminal.ext {D₁ D₂ : DiagramWithUniqueTerminal J κ}
+    (hW : D₁.W = D₂.W) (hP : D₁.P = D₂.P) : D₁ = D₂ := by
+  obtain ⟨D₁, top, h₁, h₁'⟩ := D₁
+  obtain ⟨D₂, top', h₂, h₂'⟩ := D₂
+  obtain rfl : D₁ = D₂ := by aesop
+  obtain rfl : top = top' := h₂' _ h₁
+  obtain rfl : h₁ = h₂ := by subsingleton
+  rfl
+
+instance : PartialOrder (DiagramWithUniqueTerminal J κ) where
+  le D₁ D₂ := D₁.W ≤ D₂.W ∧ D₁.P ≤ D₂.P
+  le_refl _ := ⟨by rfl, by rfl⟩
+  le_trans _ _ _ h₁ h₂ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩
+  le_antisymm _ _ h₁ h₂ := by
+    ext : 1
+    · exact le_antisymm h₁.1 h₂.1
+    · exact le_antisymm h₁.2 h₂.2
+
+section
+
+variable {J κ}
+
+/-- Auxiliary definition for `functor`. -/
+def functorMap {D₁ D₂ : DiagramWithUniqueTerminal J κ} (h : D₁ ≤ D₂) : D₁.top ⟶ D₂.top :=
+  D₂.isTerminal.lift (h.2 _ D₁.isTerminal.prop)
+
+@[simp]
+lemma functorMap_id (D : DiagramWithUniqueTerminal J κ) : functorMap (le_refl D) = 𝟙 D.top := by
+  simp [functorMap]
+
+@[reassoc (attr := simp)]
+lemma functorMap_comp {D₁ D₂ D₃ : DiagramWithUniqueTerminal J κ} (h₁₂ : D₁ ≤ D₂) (h₂₃ : D₂ ≤ D₃) :
+    functorMap h₁₂ ≫ functorMap h₂₃ = functorMap (h₁₂.trans h₂₃) :=
+  D₃.isTerminal.comm _ (h₂₃.1 _ (D₂.isTerminal.hlift _))
+
+end
+
+/-- The functor which sends a `κ`-bounded diagram with a unique terminal object to
+its terminal object. -/
+@[simps]
+def functor : DiagramWithUniqueTerminal J κ ⥤ J where
+  obj D := D.top
+  map h := functorMap (leOfHom h)
+
+variable [Fact κ.IsRegular]
+
+variable {J κ} in
+/-- The diagram containing a single object (and its identity morphism). -/
+@[simps]
+def Diagram.single (j : J) : Diagram J κ where
+  W := .ofHoms (fun (_ : Unit) ↦ 𝟙 j)
+  P := .ofObj (fun (_ : Unit) ↦ j)
+  src := by rintro _ _ _ ⟨⟩; exact ⟨⟨⟩⟩
+  tgt := by rintro _ _ _ ⟨⟩; exact ⟨⟨⟩⟩
+  hW :=
+    (hasCardinalLT_of_finite _ κ (Cardinal.IsRegular.aleph0_le Fact.out)).of_surjective
+        (fun (_ : Unit) ↦ ⟨Arrow.mk (𝟙 j), ⟨⟨⟩⟩⟩) (by
+      rintro ⟨f, hf⟩
+      refine ⟨⟨⟩, ?_⟩
+      ext
+      exact ((MorphismProperty.ofHoms_iff _ _).1
+        ((MorphismProperty.arrow_mk_mem_toSet_iff _ _).1 hf)).choose_spec.symm)
+  hP :=
+    (hasCardinalLT_of_finite _ κ (Cardinal.IsRegular.aleph0_le Fact.out)).of_surjective
+      (fun (_ : Unit) ↦ ⟨j, by simp⟩) (fun ⟨k, hk⟩ ↦ ⟨⟨⟩, by aesop⟩)
+
+instance (j : J) : Finite (Subtype (Diagram.single (κ := κ) j).P) :=
+  Finite.of_surjective (fun (_ : Unit) ↦ ⟨j, by simp⟩)
+    (by rintro ⟨_, ⟨⟩⟩; exact ⟨⟨⟩, rfl⟩)
+
+variable {J κ} in
+/-- The diagram with a unique terminal object containing a single object
+(and its identity morphism). -/
+noncomputable def DiagramWithUniqueTerminal.single (j : J) :
+    DiagramWithUniqueTerminal J κ where
+  toDiagram := .single j
+  top := j
+  isTerminal := by
+    refine .ofExistsUnique ⟨⟨⟩⟩ (fun _ h ↦ ?_) (fun _ h₁ _ _ h₂ h₃ ↦ ? _) (fun _ _ _ h ↦ ?_)
+    · simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h
+      subst h
+      exact ⟨𝟙 _, ⟨⟨⟩⟩⟩
+    · simp only [Diagram.single_P, ObjectProperty.singleton_iff] at h₁
+      subst h₁
+      obtain ⟨⟨⟩⟩ := h₂
+      obtain ⟨⟨⟩⟩ := h₃
+      simp
+    · obtain ⟨⟨⟩⟩ := h
+      exact ⟨𝟙 _, 𝟙 _, ⟨⟨⟩⟩, ⟨⟨⟩⟩, by simp⟩
+  uniq_terminal := by rintro _ ⟨⟨⟩⟩; rfl
+
+variable {J κ} in
+/-- The union of a `κ`-bounded family of `κ`-bounded diagrams. -/
+@[simps]
+def Diagram.iSup {ι : Type*} (D : ι → Diagram J κ) (hι : HasCardinalLT ι κ) :
+    Diagram J κ where
+  W := ⨆ (i : ι), (D i).W
+  P := ⨆ (i : ι), (D i).P
+  src hf := by
+    simp only [MorphismProperty.iSup_iff, iSup_apply, iSup_Prop_eq] at hf ⊢
+    obtain ⟨i, hi⟩ := hf
+    exact ⟨i, (D i).src hi⟩
+  tgt hf := by
+    simp only [MorphismProperty.iSup_iff, iSup_apply, iSup_Prop_eq] at hf ⊢
+    obtain ⟨i, hi⟩ := hf
+    exact ⟨i, (D i).tgt hi⟩
+  hW := by
+    rw [MorphismProperty.toSet_iSup]
+    exact hasCardinalLT_iUnion _ hι (fun i ↦ (D i).hW)
+  hP := hasCardinalLT_subtype_iSup _ hι (fun i ↦ (D i).hP)
+
+variable {J κ} in
+/-- The union of two `κ`-bounded diagrams. -/
+@[simps]
+def Diagram.max (D₁ D₂ : Diagram J κ) :
+    Diagram J κ where
+  W := D₁.W ⊔ D₂.W
+  P := D₁.P ⊔ D₂.P
+  src := by
+    rintro _ _ _ (h | h)
+    · exact Or.inl (D₁.src h)
+    · exact Or.inr (D₂.src h)
+  tgt := by
+    rintro _ _ _ (h | h)
+    · exact Or.inl (D₁.tgt h)
+    · exact Or.inr (D₂.tgt h)
+  hW := hasCardinalLT_union (Cardinal.IsRegular.aleph0_le Fact.out) D₁.hW D₂.hW
+  hP := hasCardinalLT_union (Cardinal.IsRegular.aleph0_le Fact.out) D₁.hP D₂.hP
+
+variable [IsCardinalFiltered J κ]
+  (hJ : ∀ (e : J), ∃ (m : J) (_ : e ⟶ m), IsEmpty (m ⟶ e))
+
+include hJ
+
+lemma isCardinalFiltered_aux
+    {ι : Type w} (D : ι → DiagramWithUniqueTerminal J κ) (hι : HasCardinalLT ι κ) :
+    ∃ (m : J) (u : ∀ i, (D i).top ⟶ m), (∀ (i : ι), IsEmpty (m ⟶ (D i).top)) ∧
+      ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
+        (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂ := by
+  choose m₀ t₀ hm₀ using fun i ↦ hJ (D i).top
+  let m₁ := IsCardinalFiltered.max m₀ hι
+  let t₁ (i : ι) : m₀ i ⟶ m₁ := IsCardinalFiltered.toMax m₀ hι i
+  let u (i : ι) : (D i).top ⟶ m₁ := t₀ i ≫ t₁ i
+  let S := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
+  let shape : MultispanShape.{w, w} :=
+    { L := { x : ι × ι × J // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
+      R := PUnit
+      fst _ := ⟨⟩
+      snd _ := ⟨⟩ }
+  let index : MultispanIndex shape J :=
+    { left x := x.1.2.2
+      right _ := m₁
+      fst x := (D x.1.1).isTerminal.lift x.2.1 ≫ u x.1.1
+      snd x := (D x.1.2.1).isTerminal.lift x.2.2 ≫ u x.1.2.1 }
+  have hκ : Cardinal.aleph0 ≤ κ := Cardinal.IsRegular.aleph0_le Fact.out
+  have hL : HasCardinalLT shape.L κ := by
+    have : HasCardinalLT (ι × (Σ (i : ι), Subtype (D i).P)) κ :=
+      hasCardinalLT_prod hκ hι (hasCardinalLT_sigma _ _ hι (fun i ↦ (D i).hP))
+    refine this.of_injective (fun ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩ ↦ ⟨i₁, i₂, ⟨j, h₂⟩⟩) ?_
+    rintro ⟨⟨i₁, i₂, j⟩, _, _⟩ ⟨⟨i₁', i₂', j'⟩, _, _⟩ h
+    rw [Prod.ext_iff, Sigma.ext_iff] at h
+    dsimp at h
+    obtain rfl : i₁ = i₁' := h.1
+    obtain rfl : i₂ = i₂' := h.2.1
+    obtain rfl : j = j' := by simpa using h
+    rfl
+  have hR : HasCardinalLT shape.R κ := hasCardinalLT_of_finite _ _ hκ
+  have hshape : HasCardinalLT (Arrow (WalkingMultispan shape)) κ := by
+    rw [hasCardinalLT_iff_of_equiv (WalkingMultispan.arrowEquiv shape),
+      hasCardinalLT_sum_iff _ _ _ hκ, hasCardinalLT_sum_iff _ _ _ hκ,
+      hasCardinalLT_iff_of_equiv (WalkingMultispan.equiv shape),
+      hasCardinalLT_sum_iff _ _ _ hκ]
+    refine ⟨⟨?_, ?_⟩, ?_, ?_⟩ <;> assumption
+  let c : Multicofork _ := IsCardinalFiltered.cocone index.multispan hshape
+  exact ⟨c.pt, fun i ↦ u i ≫ c.π ⟨⟩,
+    fun i ↦ ⟨fun hi ↦ (hm₀ i).false (t₁ i ≫ c.π ⟨⟩ ≫ hi)⟩,
+    fun i₁ i₂ j h₁ h₂ ↦ by simpa [index, shape] using c.condition ⟨⟨i₁, i₂, j⟩, h₁, h₂⟩⟩
+
+lemma isCardinalFiltered : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ :=
+  isCardinalFiltered_preorder _ _ (fun ι D hι ↦ by
+    have hκ : Cardinal.aleph0 ≤ κ := Cardinal.IsRegular.aleph0_le Fact.out
+    simp only [← hasCardinalLT_iff_cardinal_mk_lt] at hι
+    obtain ⟨m, u, hm₀, hm⟩ := isCardinalFiltered_aux J κ hJ D hι
+    let φ (x : (Σ (i : ι), (Subtype (D i).P))) : x.2.1 ⟶ m :=
+      (D x.1).isTerminal.lift x.2.2 ≫ u x.1
+    have hD {i : ι} : ¬ (D i).P m := fun hi ↦ (hm₀ i).false ((D i).isTerminal.lift hi)
+    let D₀ := Diagram.iSup (fun i ↦ (D i).toDiagram) hι
+    let D₁ := D₀.max (.single m)
+    let D₂ : Diagram J κ :=
+      { W := D₁.W ⊔ .ofHoms φ
+        P := D₁.P
+        src := by
+          simp only [Diagram.max_W, Diagram.iSup_W, Diagram.single_W, Diagram.max_P, Pi.sup_apply,
+            Diagram.iSup_P, iSup_apply, iSup_Prop_eq, Diagram.single_P,
+            ObjectProperty.singleton_iff, sup_Prop_eq, D₁, D₀]
+          rintro _ _ _ ((hf | ⟨⟨⟩⟩) | ⟨i, j, hj⟩)
+          · simp only [MorphismProperty.iSup_iff] at hf
+            obtain ⟨i, hf⟩ := hf
+            exact Or.inl ⟨i, (D i).src hf⟩
+          · exact Or.inr rfl
+          · exact Or.inl ⟨i, hj⟩
+        tgt := by
+          simp only [Diagram.max_W, Diagram.iSup_W, Diagram.single_W, Diagram.max_P, Pi.sup_apply,
+            Diagram.iSup_P, iSup_apply, iSup_Prop_eq, Diagram.single_P,
+            ObjectProperty.singleton_iff, sup_Prop_eq, D₁, D₀]
+          rintro _ _ _ ((hf | ⟨⟨⟩⟩) | ⟨i, j, hj⟩)
+          · simp only [MorphismProperty.iSup_iff] at hf
+            obtain ⟨i, hf⟩ := hf
+            exact Or.inl ⟨i, (D i).tgt hf⟩
+          · exact Or.inr rfl
+          · exact Or.inr rfl
+        hW := by
+          rw [MorphismProperty.toSet_max]
+          exact hasCardinalLT_union hκ D₁.hW
+            (hasCardinalLT_toSet_morphismPropertyOfHoms _
+              (hasCardinalLT_sigma _ _ hι (fun i ↦ (D i).hP)))
+        hP := hasCardinalLT_subtype_max hκ
+                (hasCardinalLT_subtype_iSup _ hι (fun i ↦ (D i).hP))
+                (hasCardinalLT_of_finite _ _ hκ) }
+    have hD₂ {f : m ⟶ m} (hf : D₂.W f) : f = 𝟙 _ := by
+      simp only [Diagram.max_W, Diagram.iSup_W, Diagram.single_W, D₁, D₀, D₂] at hf
+      obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
+      · simp only [MorphismProperty.iSup_iff] at hf
+        obtain ⟨i, hi⟩ := hf
+        exact (hD ((D i).src hi)).elim
+      · rfl
+      · rw [MorphismProperty.ofHoms_iff] at hf
+        obtain ⟨⟨i, j, hj⟩, hi⟩ := hf
+        obtain rfl : m = j := congr_arg Arrow.leftFunc.obj hi
+        exact (hD hj).elim
+    let he : D₂.IsTerminal m := by
+      have H {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m} (hf : D₂.W f) :
+          f = φ ⟨i, ⟨_, hj⟩⟩ := by
+        simp only [Diagram.max_W, Diagram.iSup_W, Diagram.single_W, D₁, D₀, D₂] at hf
+        obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨i', j, hj'⟩⟩) := hf
+        · simp only [MorphismProperty.iSup_iff] at hf
+          obtain ⟨i, hf⟩ := hf
+          exact (hD ((D i).tgt hf)).elim
+        · exact (hD hj).elim
+        · apply hm
+      refine .ofExistsUnique ?_ ?_ ?_ ?_
+      · exact Or.inl (Or.inr ⟨⟨⟩⟩)
+      · simp only [Diagram.max_P, Pi.sup_apply, Diagram.iSup_P, iSup_apply, iSup_Prop_eq,
+          Diagram.single_P, ObjectProperty.singleton_iff, sup_Prop_eq, Diagram.max_W,
+          Diagram.iSup_W, Diagram.single_W, D₁, D₀, D₂]
+        rintro j (⟨i, hi⟩ | rfl)
+        · exact ⟨φ ⟨i, _, hi⟩, Or.inr (.mk _)⟩
+        · exact ⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩
+      · intro j hj l₁ l₂ hl₁ hl₂
+        simp only [Diagram.max_P, Pi.sup_apply, Diagram.iSup_P, iSup_apply, iSup_Prop_eq,
+          Diagram.single_P, ObjectProperty.singleton_iff, sup_Prop_eq, D₁, D₀, D₂] at hj
+        obtain (⟨i, hj⟩ | rfl) := hj
+        · obtain rfl := H hj hl₁
+          obtain rfl := H hj hl₂
+          rfl
+        · rw [hD₂ hl₁, hD₂ hl₂]
+      · rintro j k f ((hf | ⟨⟨⟩⟩) | ⟨⟨i, j, hj⟩⟩)
+        · simp only [Diagram.iSup_W, MorphismProperty.iSup_iff, D₀] at hf
+          obtain ⟨i, hf⟩ := hf
+          exact ⟨φ ⟨i, j, (D i).src hf⟩, φ ⟨i, k, (D i).tgt hf⟩, Or.inr ⟨_⟩, Or.inr ⟨_⟩,
+            by simp [φ, (D i).isTerminal.comm_assoc _ hf]⟩
+        · exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
+        · exact ⟨φ ⟨i, j, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
+    let D₂' : DiagramWithUniqueTerminal J κ :=
+      { toDiagram := D₂
+        top := _
+        isTerminal := he
+        uniq_terminal j hj := by
+          have := hj.prop
+          simp only [Diagram.max_P, Pi.sup_apply, Diagram.iSup_P, iSup_apply, iSup_Prop_eq,
+            Diagram.single_P, ObjectProperty.singleton_iff, sup_Prop_eq, D₁, D₀, D₂] at this
+          obtain (⟨i, hi⟩ | rfl) := this
+          · exfalso
+            exact (hm₀ i).false (hj.lift (by simp [D₂, D₁]) ≫ (D i).isTerminal.lift hi)
+          · rfl }
+    refine ⟨D₂', fun i ↦ ⟨?_, ?_⟩⟩
+    · exact le_trans (le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left) le_sup_left
+    · exact le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left)
+
+lemma final_functor : (functor J κ).Final := by
+  have hκ : Cardinal.aleph0 ≤ κ := Cardinal.IsRegular.aleph0_le Fact.out
+  have := isCardinalFiltered J κ hJ
+  have := isFiltered_of_isCardinalFiltered J κ
+  have := isFiltered_of_isCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
+  rw [Functor.final_iff_of_isFiltered]
+  refine ⟨fun j ↦ ⟨.single j, ⟨𝟙 _⟩⟩, fun {j D} (f₁ f₂ : j ⟶ D.top) ↦ ?_⟩
+  obtain ⟨m₀, t, hm₀⟩ := hJ D.top
+  obtain ⟨m₁, u, hu⟩ : ∃ (m₁ : J) (u : m₀ ⟶ m₁), f₁ ≫ t ≫ u = f₂ ≫ t ≫ u :=
+    ⟨_, IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t),
+      by simpa using IsFiltered.coeq_condition (f₁ ≫ t) (f₂ ≫ t)⟩
+  have h₁ : ¬ (D.P m₁) := fun h₁ ↦ hm₀.false (u ≫ D.isTerminal.lift h₁)
+  let φ (x : Subtype D.P) : x.1 ⟶ m₁ := D.isTerminal.lift x.2 ≫ t ≫ u
+  let D₀ := D.toDiagram.max (.single m₁)
+  let D₁ : Diagram J κ :=
+    { W := D₀.W ⊔ .ofHoms φ
+      P := D₀.P
+      src := by
+        rintro i j f (hf | ⟨⟨j, hj⟩⟩)
+        · exact D₀.src hf
+        · exact Or.inl hj
+      tgt := by
+        rintro i j f (hf | ⟨⟨j, hj⟩⟩)
+        · exact D₀.tgt hf
+        · exact Or.inr ⟨⟨⟩⟩
+      hW :=
+        hasCardinalLT_union hκ
+          (hasCardinalLT_union hκ D.hW
+            (hasCardinalLT_toSet_morphismPropertyOfHoms _
+            (hasCardinalLT_of_finite _ _ hκ)))
+          (hasCardinalLT_toSet_morphismPropertyOfHoms _ D.hP)
+      hP :=
+        hasCardinalLT_union hκ D.hP
+          (hasCardinalLT_subtype_objectPropertyOfObj _
+            (hasCardinalLT_of_finite _ _ hκ)) }
+  have h₂ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : D₁.W f) :
+      f = φ ⟨_, hj⟩ := by
+    obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf
+    · exact (h₁ (D.tgt hf)).elim
+    · exact (h₁ hj).elim
+    · rfl
+  have h₃ {f : m₁ ⟶ m₁} (hf : D₁.W f) : f = 𝟙 _ := by
+    obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
+    · exact (h₁ (D.src hf)).elim
+    · rfl
+    · rw [MorphismProperty.ofHoms_iff] at hf
+      obtain ⟨⟨j, hj⟩, hf⟩ := hf
+      obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
+      exact (h₁ hj).elim
+  let hm₁ : D₁.IsTerminal m₁ :=
+    .ofExistsUnique (Or.inl (Or.inr ⟨⟨⟩⟩)) (by
+        rintro j (hj | ⟨⟨⟨⟩⟩⟩)
+        · exact ⟨φ ⟨_, hj⟩, Or.inr ⟨_⟩⟩
+        · exact ⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩) (by
+        rintro j (hj | ⟨⟨⟨⟩⟩⟩) l₁ l₂ hl₁ hl₂
+        · obtain rfl := h₂ hj hl₁
+          obtain rfl := h₂ hj hl₂
+          rfl
+        · rw [h₃ hl₁, h₃ hl₂]) (by
+      rintro j k f ((hf | ⟨⟨⟩⟩) | ⟨⟨j, hj⟩⟩)
+      · exact ⟨φ ⟨_, D.src hf⟩, φ ⟨_, D.tgt hf⟩,
+          Or.inr ⟨_⟩, Or.inr ⟨_⟩, D.isTerminal.comm_assoc _ hf _⟩
+      · exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
+      · exact ⟨φ ⟨_, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩)
+  have lift_eq (j : J) (hj : D.P j) : hm₁.lift (Or.inl hj) = φ ⟨_, hj⟩ :=
+    hm₁.uniq _ (Or.inr ⟨_⟩)
+  let D₁' : DiagramWithUniqueTerminal J κ :=
+    { toDiagram := D₁
+      top := m₁
+      isTerminal := hm₁
+      uniq_terminal j hj := by
+        obtain (hj' | ⟨⟨⟩⟩) := hj.prop
+        · exact hm₀.elim (u ≫ hj.lift (Or.inr ⟨⟨⟩⟩) ≫ D.isTerminal.lift hj')
+        · rfl}
+  exact ⟨D₁', homOfLE ⟨le_sup_left.trans le_sup_left, le_sup_left⟩,
+    by simpa [functorMap, D₁', lift_eq _ D.isTerminal.prop, φ]⟩
+
+lemma aux :
+    ∃ (α : Type w) (_ : PartialOrder α) (_ : IsCardinalFiltered α κ)
+      (F : α ⥤ J), F.Final :=
+  ⟨DiagramWithUniqueTerminal J κ, _, isCardinalFiltered J κ hJ,
+    functor J κ, final_functor J κ hJ⟩
+
+end exists_cardinal_directed
+
+
+/-!
+The previous lemma `IsCardinalFiltered.exists_cardinal_directed.aux`
+is the particular case of the main lemma
+`IsCardinalFiltered.exists_cardinal_directed` below in the particular
+case the `κ`-filtered category `J` has no object `m : J` such that for any
+object `j : J`, there exists a map `j ⟶ m`.
+
+The general case is obtained by applying the previous result to
+the cartesian product `J × κ.ord.toType`.
+-/
+
+@[stacks 0032]
+lemma exists_cardinal_directed (J : Type w) [SmallCategory J] (κ : Cardinal.{w})
+    [Fact κ.IsRegular] [IsCardinalFiltered J κ] :
+    ∃ (α : Type w) (_ : PartialOrder α) (_ : IsCardinalFiltered α κ)
+      (F : α ⥤ J), F.Final := by
+  have := isFiltered_of_isCardinalFiltered κ.ord.toType κ
+  obtain ⟨α, _, _, F, _⟩ :=
+    exists_cardinal_directed.aux (J × κ.ord.toType) κ (fun ⟨j, x⟩ ↦
+      ⟨⟨j, Order.succ x⟩, (𝟙 _, homOfLE (Order.le_succ x)), ⟨fun ⟨_, f⟩ ↦ by
+        have : NoMaxOrder κ.ord.toType :=
+          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
+        exact not_isMax _ (Order.max_of_succ_le (leOfHom f))⟩⟩)
+  exact ⟨_, _, inferInstance, F ⋙ Prod.fst _ _, inferInstance⟩
+
+end IsCardinalFiltered
+
+lemma IsFiltered.isDirected (α : Type w) [PartialOrder α] [IsFiltered α] :
+    IsDirected α (· ≤ ·) where
+  directed i j := ⟨max i j, leOfHom (leftToMax i j), leOfHom (rightToMax i j)⟩
+
+attribute [local instance] Cardinal.fact_isRegular_aleph0 in
+@[stacks 0032]
+lemma IsFiltered.exists_directed
+    (J : Type w) [SmallCategory J] [IsFiltered J] :
+    ∃ (α : Type w) (_ : PartialOrder α) (_ : IsDirected α (· ≤ ·)) (_ : Nonempty α)
+      (F : α ⥤ J), F.Final := by
+  have := (isCardinalFiltered_aleph0_iff.{w} J).2 inferInstance
+  obtain ⟨α, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J .aleph0
+  have : IsFiltered α := by rwa [← isCardinalFiltered_aleph0_iff.{w}]
+  exact ⟨α, _, IsFiltered.isDirected _, nonempty, F, inferInstance⟩
+
+lemma HasCardinalFilteredColimits.mk' {C : Type u} [Category.{v} C]
+    {κ : Cardinal.{w}} [Fact κ.IsRegular]
+    (hC : ∀ (α : Type w) [PartialOrder α] [IsCardinalFiltered α κ],
+      HasColimitsOfShape α C) :
+    HasCardinalFilteredColimits C κ where
+  hasColimitsOfShape J _ _ := by
+    obtain ⟨α, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J κ
+    exact Functor.Final.hasColimitsOfShape_of_final F
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean b/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
index 4669c1f0d56f5f..106715f34ed56b 100644
--- a/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
+++ b/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
@@ -199,4 +199,31 @@ instance isCardinalFiltered_under
               dsimp at this ⊢
               simp only [reassoc_of% this, Category.comp_id] } }⟩
 
+instance isCardinalFiltered_prod (J₁ : Type u) (J₂ : Type u')
+    [Category.{v} J₁] [Category.{v'} J₂] (κ : Cardinal.{w}) [Fact κ.IsRegular]
+    [IsCardinalFiltered J₁ κ] [IsCardinalFiltered J₂ κ] :
+    IsCardinalFiltered (J₁ × J₂) κ where
+  nonempty_cocone F hC := ⟨by
+    let c₁ := cocone (F ⋙ Prod.fst _ _) hC
+    let c₂ := cocone (F ⋙ Prod.snd _ _) hC
+    exact
+      { pt := (c₁.pt, c₂.pt)
+        ι.app i := (c₁.ι.app i, c₂.ι.app i)
+        ι.naturality i j f := by
+          ext
+          · simpa using c₁.w f
+          · simpa using c₂.w f}⟩
+
+instance isCardinalFiltered_pi {ι : Type u'} (J : ι → Type u) [∀ i, Category.{v} (J i)]
+    (κ : Cardinal.{w}) [Fact κ.IsRegular] [∀ i, IsCardinalFiltered (J i) κ] :
+    IsCardinalFiltered (∀ i, J i) κ where
+  nonempty_cocone {C _} F hC := ⟨by
+    let c (i : ι) := cocone (F ⋙ Pi.eval J i) hC
+    exact
+      { pt i := (c i).pt
+        ι.app X i := (c i).ι.app X
+        ι.naturality {X Y} f := by
+          ext i
+          simpa using (c i).ι.naturality f }⟩
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean b/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean
index 0af2bca046cdad..34d8bc6058321e 100644
--- a/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean
+++ b/Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean
@@ -35,13 +35,13 @@ variable (C : Type u) [Category.{v} C] (κ : Cardinal.{w}) [Fact κ.IsRegular]
 if it is cocomplete and admits a (small) family `G : ι → C` of `κ`-presentable
 objects such that any object identifies as a `κ`-filtered colimit of these objects. -/
 class IsCardinalLocallyPresentable : Prop
-  extends HasCardinalFilteredGenerators C κ, HasColimitsOfSize.{w, w} C where
+  extends HasCardinalFilteredGenerator C κ, HasColimitsOfSize.{w, w} C where
 
 /-- Given a regular cardinal `κ`, a category `C` is `κ`-accessible
 if it has `κ`-filtered colimits and admits a (small) family `G : ι → C` of `κ`-presentable
 objects such that any object identifies as a `κ`-filtered colimit of these objects. -/
 class IsCardinalAccessibleCategory : Prop
-  extends HasCardinalFilteredGenerators C κ, HasCardinalFilteredColimits.{w} C κ where
+  extends HasCardinalFilteredGenerator C κ, HasCardinalFilteredColimits.{w} C κ where
 
 instance [IsCardinalLocallyPresentable C κ] : IsCardinalAccessibleCategory C κ where
 
@@ -72,9 +72,11 @@ instance [IsLocallyPresentable.{w} C] : IsAccessibleCategory.{w} C where
 
 instance [IsAccessibleCategory.{w} C] (X : C) : IsPresentable.{w} X := by
   obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal C
-  obtain ⟨ι, G, h⟩ := HasCardinalFilteredGenerators.exists_generators C κ
+  obtain ⟨_, _, h⟩ := HasCardinalFilteredGenerator.exists_generator C κ
   apply h.presentable
 
+example [IsLocallyPresentable.{w} C] (X : C) : IsPresentable.{w} X := inferInstance
+
 end
 
 end CategoryTheory
diff --git a/Mathlib/Order/Category/PartOrdEmb.lean b/Mathlib/Order/Category/PartOrdEmb.lean
new file mode 100644
index 00000000000000..1180cd99b4427b
--- /dev/null
+++ b/Mathlib/Order/Category/PartOrdEmb.lean
@@ -0,0 +1,321 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Johan Commelin
+-/
+import Mathlib.Order.Category.PartOrd
+import Mathlib.CategoryTheory.Limits.Types.Filtered
+import Mathlib.CategoryTheory.Limits.Preserves.Filtered
+import Mathlib.CategoryTheory.Limits.Filtered
+
+/-!
+# Category of partial orders, with order embeddings as morphisms
+
+This defines `PartOrdEmb`, the category of partial orders with order embeddings
+as morphisms. We also show that `PartOrdEmb` has filtered colimits.
+
+-/
+
+open CategoryTheory Limits
+
+universe u
+
+/-- The category of partial orders. -/
+structure PartOrdEmb where
+  /-- The underlying partially ordered type. -/
+  (carrier : Type*)
+  [str : PartialOrder carrier]
+
+attribute [instance] PartOrdEmb.str
+
+initialize_simps_projections PartOrdEmb (carrier → coe, -str)
+
+namespace PartOrdEmb
+
+instance : CoeSort PartOrdEmb (Type _) :=
+  ⟨PartOrdEmb.carrier⟩
+
+attribute [coe] PartOrdEmb.carrier
+
+/-- Construct a bundled `PartOrdEmb` from the underlying type and typeclass. -/
+abbrev of (X : Type*) [PartialOrder X] : PartOrdEmb := ⟨X⟩
+
+/-- The type of morphisms in `PartOrdEmb R`. -/
+@[ext]
+structure Hom (X Y : PartOrdEmb.{u}) where
+  private mk ::
+  /-- The underlying `OrderEmbedding`. -/
+  hom' : X ↪o Y
+
+instance : Category PartOrdEmb.{u} where
+  Hom X Y := Hom X Y
+  id _ := ⟨RelEmbedding.refl _⟩
+  comp f g := ⟨f.hom'.trans g.hom'⟩
+
+instance : ConcreteCategory PartOrdEmb (· ↪o ·) where
+  hom := Hom.hom'
+  ofHom := Hom.mk
+
+/-- Turn a morphism in `PartOrdEmb` back into a `OrderEmbedding`. -/
+abbrev Hom.hom {X Y : PartOrdEmb.{u}} (f : Hom X Y) :=
+  ConcreteCategory.hom (C := PartOrdEmb) f
+
+/-- Typecheck a `OrderEmbedding` as a morphism in `PartOrdEmb`. -/
+abbrev ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X ↪o Y) : of X ⟶ of Y :=
+  ConcreteCategory.ofHom (C := PartOrdEmb) f
+
+variable {R} in
+/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas. -/
+def Hom.Simps.hom (X Y : PartOrdEmb.{u}) (f : Hom X Y) :=
+  f.hom
+
+initialize_simps_projections Hom (hom' → hom)
+
+/-!
+The results below duplicate the `ConcreteCategory` simp lemmas, but we can keep them for `dsimp`.
+-/
+
+@[simp]
+lemma coe_id {X : PartOrdEmb} : (𝟙 X : X → X) = id := rfl
+
+@[simp]
+lemma coe_comp {X Y Z : PartOrdEmb} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
+
+@[simp]
+lemma forget_map {X Y : PartOrdEmb} (f : X ⟶ Y) :
+    (forget PartOrdEmb).map f = f := rfl
+
+@[ext]
+lemma ext {X Y : PartOrdEmb} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
+  ConcreteCategory.hom_ext _ _ w
+
+-- This is not `simp` to avoid rewriting in types of terms.
+theorem coe_of (X : Type u) [PartialOrder X] : (PartOrdEmb.of X : Type u) = X := rfl
+
+lemma hom_id {X : PartOrdEmb} : (𝟙 X : X ⟶ X).hom = RelEmbedding.refl _ := rfl
+
+/- Provided for rewriting. -/
+lemma id_apply (X : PartOrdEmb) (x : X) :
+    (𝟙 X : X ⟶ X) x = x := by simp
+
+@[simp]
+lemma hom_comp {X Y Z : PartOrdEmb} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).hom = f.hom.trans g.hom := rfl
+
+/- Provided for rewriting. -/
+lemma comp_apply {X Y Z : PartOrdEmb} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
+    (f ≫ g) x = g (f x) := by simp
+
+lemma Hom.injective {X Y : PartOrdEmb.{u}} (f : X ⟶ Y) : Function.Injective f :=
+  f.hom'.injective
+
+lemma Hom.le_iff_le {X Y : PartOrdEmb.{u}} (f : X ⟶ Y) (x₁ x₂ : X) :
+    f x₁ ≤ f x₂ ↔ x₁ ≤ x₂ :=
+  f.hom'.le_iff_le
+
+@[ext]
+lemma hom_ext {X Y : PartOrdEmb} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g :=
+  Hom.ext hf
+
+@[simp]
+lemma hom_ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X ↪o Y) :
+    (ofHom f).hom = f :=
+  rfl
+
+@[simp]
+lemma ofHom_hom {X Y : PartOrdEmb} (f : X ⟶ Y) : ofHom (Hom.hom f) = f := rfl
+
+@[simp]
+lemma ofHom_id {X : Type u} [PartialOrder X] : ofHom (RelEmbedding.refl _) = 𝟙 (of X) := rfl
+
+@[simp]
+lemma ofHom_comp {X Y Z : Type u} [PartialOrder X] [PartialOrder Y] [PartialOrder Z]
+    (f : X ↪o Y) (g : Y ↪o Z) :
+    ofHom (f.trans g) = ofHom f ≫ ofHom g :=
+  rfl
+
+lemma ofHom_apply {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X ↪o Y) (x : X) :
+    (ofHom f) x = f x := rfl
+
+lemma inv_hom_apply {X Y : PartOrdEmb} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x := by
+  simp
+
+lemma hom_inv_apply {X Y : PartOrdEmb} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s := by
+  simp
+
+instance hasForgetToPartOrd : HasForget₂ PartOrdEmb PartOrd where
+  forget₂.obj X := .of X
+  forget₂.map f := PartOrd.ofHom f.hom
+
+/-- Constructs an equivalence between partial orders from an order isomorphism between them. -/
+@[simps]
+def Iso.mk {α β : PartOrdEmb.{u}} (e : α ≃o β) : α ≅ β where
+  hom := ofHom e
+  inv := ofHom e.symm
+
+/-- The order isomorphism induced by an isomorphism in `PartOrdEmb`. -/
+def orderIsoOfIso {α β : PartOrdEmb.{u}} (e : α ≅ β) :
+    α ≃o β := sorry
+
+/-- `OrderDual` as a functor. -/
+@[simps map]
+def dual : PartOrdEmb ⥤ PartOrdEmb where
+  obj X := of Xᵒᵈ
+  map f := ofHom f.hom.dual
+
+/-- The equivalence between `PartOrdEmb` and itself induced by `OrderDual` both ways. -/
+@[simps functor inverse]
+def dualEquiv : PartOrdEmb ≌ PartOrdEmb where
+  functor := dual
+  inverse := dual
+  unitIso := NatIso.ofComponents fun X => Iso.mk <| OrderIso.dualDual X
+  counitIso := NatIso.ofComponents fun X => Iso.mk <| OrderIso.dualDual X
+
+end PartOrdEmb
+
+theorem partOrdEmb_dual_comp_forget_to_pardOrd :
+    PartOrdEmb.dual ⋙ forget₂ PartOrdEmb PartOrd =
+      forget₂ PartOrdEmb PartOrd ⋙ PartOrd.dual :=
+  rfl
+
+namespace PartOrdEmb
+
+variable {J : Type u} [SmallCategory J] [IsFiltered J] {F : J ⥤ PartOrdEmb.{u}}
+
+namespace Limits
+
+variable {c : Cocone (F ⋙ forget _)} (hc : IsColimit c)
+
+/-- Given a functor `F : J ⥤ PartOrdEmb` and a colimit cocone `c` for
+`F ⋙ forget _`, this is the type `c.pt` on which we define a partial order
+which makes it the colimit of `F`. -/
+@[nolint unusedArguments]
+def CoconePt (_ : IsColimit c) : Type u := c.pt
+
+open IsFiltered
+
+instance : PartialOrder (CoconePt hc) where
+  le x y := ∃ (j : J) (x' y' : F.obj j) (hx : c.ι.app j x' = x)
+      (hy : c.ι.app j y' = y), x' ≤ y'
+  le_refl x := by
+    obtain ⟨j, x', hx⟩ := Types.jointly_surjective_of_isColimit hc x
+    exact ⟨j, x', x', hx, hx, le_rfl⟩
+  le_trans := by
+    rintro x y z ⟨j, x₁, y₁, hx₁, hy₁, hxy⟩ ⟨k, y₂, z₁, hy₂, hz₁, hyz⟩
+    obtain ⟨l, a, b, h⟩ :=
+      (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := y₁) (xj := y₂)).1
+        (hy₁.trans hy₂.symm)
+    exact ⟨l, F.map a x₁, F.map b z₁,
+      (ConcreteCategory.congr_hom (c.w a) x₁).trans hx₁,
+      (ConcreteCategory.congr_hom (c.w b) z₁).trans hz₁,
+      ((F.map a).hom.monotone hxy).trans
+        (le_of_eq_of_le h ((F.map b).hom.monotone hyz))⟩
+  le_antisymm := by
+    rintro x y ⟨j, x₁, y₁, hx₁, hy₁, h₁⟩ ⟨k, y₂, x₂, hy₂, hx₂, h₂⟩
+    obtain ⟨l, a, b, x₃, y₃, h₃, h₄, h₅, h₆⟩ :
+        ∃ (l : J) (a : j ⟶ l) (b : k ⟶ l) (x₃ y₃ : _),
+        x₃ = F.map a x₁ ∧ x₃ = F.map b x₂ ∧ y₃ = F.map a y₁ ∧ y₃ = F.map b y₂ := by
+      obtain ⟨l₁, a, b, h₃⟩ :=
+        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := x₁) (xj := x₂)).1
+          (hx₁.trans hx₂.symm)
+      obtain ⟨l₂, a', b', h₄⟩ :=
+        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := y₁) (xj := y₂)).1
+          (hy₁.trans hy₂.symm)
+      obtain ⟨l, d, d', h₅, h₆⟩ := IsFiltered.bowtie a a' b b'
+      exact ⟨l, a ≫ d, b ≫ d, F.map (a ≫ d) x₁, F.map (a' ≫ d') y₁, rfl,
+        by simpa, by rw [h₅], by simpa [h₆]⟩
+    have h₇ : x₃ = y₃ :=
+      le_antisymm
+        (by simpa only [h₃, h₅] using (F.map a).hom.monotone h₁)
+        (by simpa only [h₄, h₆] using (F.map b).hom.monotone h₂)
+    exact hx₁.symm.trans ((ConcreteCategory.congr_hom (c.w a) x₁).symm.trans
+      ((congr_arg (c.ι.app l) (h₃.symm.trans (h₇.trans h₅))).trans
+        ((ConcreteCategory.congr_hom (c.w a) y₁).trans hy₁)))
+
+/-- The colimit cocone for a functor `F : J ⥤ PartOrdEmb` from a filtered
+category that is constructed from a colimit cocone for `F ⋙ forget _`. -/
+@[simps]
+def cocone : Cocone F where
+  pt := .of (CoconePt hc)
+  ι.app j := ofHom
+    { toFun := c.ι.app j
+      inj' x y h := by
+        obtain ⟨k, a, ha⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc x y).1 h
+        exact (F.map a).injective ha
+      map_rel_iff' {x y} := by
+        refine ⟨?_, fun h ↦ ⟨j, x, y, rfl, rfl, h⟩⟩
+        rintro ⟨k, x', y', hx, hy, h⟩
+        obtain ⟨l₁, a₁, b₁, hl₁⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hx
+        obtain ⟨l₂, a₂, b₂, hl₂⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hy
+        dsimp at hx hy hl₁ hl₂
+        obtain ⟨m, d, d', h₁, h₂⟩ := bowtie a₁ a₂ b₁ b₂
+        rw [← (F.map (a₁ ≫ d)).le_iff_le] at h
+        rw [← (F.map (b₁ ≫ d)).le_iff_le]
+        conv_rhs => rw [h₂]
+        conv_rhs at h => rw [h₁]
+        simp only [Functor.map_comp, hom_comp, RelEmbedding.coe_trans, Function.comp_apply,
+          ← hl₁, ← hl₂]
+        simpa using h }
+  ι.naturality _ _ f := by ext x; exact ConcreteCategory.congr_hom (c.w f) x
+
+/-- Auxiliary definition for `isColimitCocone`. -/
+def CoconePt.desc (s : Cocone F) : CoconePt hc ↪o s.pt where
+  toFun := hc.desc ((forget _).mapCocone s)
+  inj' x y h := by
+    obtain ⟨j, x', y', rfl, rfl⟩ :=
+      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y
+    obtain rfl := (s.ι.app j).injective
+      (((congr_fun (hc.fac ((forget _).mapCocone s) j) x').symm.trans h).trans
+        (congr_fun (hc.fac ((forget _).mapCocone s) j) y'))
+    rfl
+  map_rel_iff' {x y} := by
+    obtain ⟨j, x', y', rfl, rfl⟩ :=
+      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y
+    have hx := (congr_fun (hc.fac ((forget _).mapCocone s) j) x')
+    have hy := (congr_fun (hc.fac ((forget _).mapCocone s) j) y')
+    dsimp at hx hy ⊢
+    rw [hx, hy, OrderEmbedding.le_iff_le]
+    refine ⟨fun h ↦ ⟨j, _, _, rfl, rfl, h⟩, fun ⟨k, x, y, hx', hy', h⟩ ↦ ?_⟩
+    obtain ⟨l, f, g, hl⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hx'
+    obtain ⟨l', f', g', hl'⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hy'
+    obtain ⟨m, a, b, h₁, h₂⟩ := bowtie f f' g g'
+    dsimp at hl hl'
+    rw [← (F.map (f ≫ a)).le_iff_le] at h
+    rw [← (F.map (g ≫ a)).le_iff_le]
+    exact le_of_eq_of_le (by simp [hl]) (le_of_le_of_eq h (by simp [h₁, h₂, hl']))
+
+@[simp]
+lemma CoconePt.fac_apply (s : Cocone F) (j : J) (x : F.obj j) :
+    CoconePt.desc hc s (c.ι.app j x) = s.ι.app j x :=
+  congr_fun (hc.fac ((forget _).mapCocone s) j) x
+
+/-- A colimit cocone for `F : J ⥤ PartOrdEmb` (with `J` filtered) can be
+obtained from a colimit cocone for `F ⋙ forget _`. -/
+def isColimitCocone : IsColimit (cocone hc) where
+  desc s := ofHom (CoconePt.desc hc s)
+  uniq s m hm := by
+    ext x
+    obtain ⟨j, x, rfl⟩ := Types.jointly_surjective_of_isColimit hc x
+    exact ((ConcreteCategory.congr_hom (hm j)) x).trans (CoconePt.fac_apply hc s j x).symm
+
+instance : HasColimit F where
+  exists_colimit := ⟨_, isColimitCocone (colimit.isColimit (F ⋙ forget _))⟩
+
+instance : PreservesColimit F (forget _) :=
+  preservesColimit_of_preserves_colimit_cocone
+    (isColimitCocone (colimit.isColimit (F ⋙ forget _)))
+    (colimit.isColimit (F ⋙ forget _))
+
+instance : HasColimitsOfShape J PartOrdEmb.{u} where
+
+instance : PreservesColimitsOfShape J (forget PartOrdEmb.{u}) where
+
+instance : HasFilteredColimitsOfSize.{u, u} PartOrdEmb.{u} where
+  HasColimitsOfShape _ := inferInstance
+
+instance : PreservesFilteredColimitsOfSize.{u, u} (forget PartOrdEmb.{u}) where
+  preserves_filtered_colimits _ := inferInstance
+
+end Limits
+
+end PartOrdEmb
diff --git a/Mathlib/SetTheory/Cardinal/HasCardinalLT.lean b/Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
index 0acdb59e0b6f26..85a1a133ec2182 100644
--- a/Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
+++ b/Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
@@ -75,6 +75,21 @@ lemma hasCardinalLT_aleph0_iff (X : Type u) :
     HasCardinalLT X Cardinal.aleph0.{v} ↔ Finite X := by
   simpa [HasCardinalLT] using Cardinal.mk_lt_aleph0_iff
 
+lemma hasCardinalLT_of_finite
+    (X : Type*) [Finite X] (κ : Cardinal) (hκ : Cardinal.aleph0 ≤ κ) :
+    HasCardinalLT X κ :=
+  .of_le (by rwa [hasCardinalLT_aleph0_iff]) hκ
+
+@[simp]
+lemma hasCardinalLT_lift_iff (X : Type v) (κ : Cardinal.{w}) :
+    HasCardinalLT X (Cardinal.lift.{u} κ) ↔ HasCardinalLT X κ := by
+  simp [HasCardinalLT, ← (Cardinal.lift_strictMono.{max v w, max u}).lt_iff_lt]
+
+@[simp]
+lemma hasCardinalLT_ulift_iff (X : Type v) (κ : Cardinal.{w}) :
+    HasCardinalLT (ULift.{u} X) κ ↔ HasCardinalLT X κ :=
+  hasCardinalLT_iff_of_equiv Equiv.ulift κ
+
 lemma hasCardinalLT_sum_iff (X : Type u) (Y : Type u') (κ : Cardinal.{w})
     (hκ : Cardinal.aleph0 ≤ κ) :
     HasCardinalLT (X ⊕ Y) κ ↔ HasCardinalLT X κ ∧ HasCardinalLT Y κ := by
@@ -98,6 +113,84 @@ lemma hasCardinalLT_option_iff (X : Type u) (κ : Cardinal.{w})
   rw [hasCardinalLT_aleph0_iff]
   infer_instance
 
+lemma hasCardinalLT_subtype_max
+    {X : Type*} {P₁ P₂ : X → Prop} {κ : Cardinal} (hκ : Cardinal.aleph0 ≤ κ)
+    (h₁ : HasCardinalLT (Subtype P₁) κ) (h₂ : HasCardinalLT (Subtype P₂) κ) :
+    HasCardinalLT (Subtype (P₁ ⊔ P₂)) κ := by
+  have : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ := by
+    rw [hasCardinalLT_sum_iff _ _ _ hκ]
+    exact ⟨h₁, h₂⟩
+  refine this.of_surjective (Sum.elim (fun x ↦ ⟨x.1, Or.inl x.2⟩)
+    (fun x ↦ ⟨x.1, Or.inr x.2⟩)) ?_
+  rintro ⟨x, hx | hx⟩
+  · exact ⟨Sum.inl ⟨x, hx⟩, rfl⟩
+  · exact ⟨Sum.inr ⟨x, hx⟩, rfl⟩
+
+lemma hasCardinalLT_union
+    {X : Type*} {S₁ S₂ : Set X} {κ : Cardinal} (hκ : Cardinal.aleph0 ≤ κ)
+    (h₁ : HasCardinalLT S₁ κ) (h₂ : HasCardinalLT S₂ κ) :
+    HasCardinalLT (S₁ ∪ S₂ : Set _) κ :=
+  hasCardinalLT_subtype_max hκ h₁ h₂
+
+/-- The particular case of `hasCardinatLT_sigma` when all the inputs are in the
+same universe `w`. It is used to prove the general case. -/
+lemma hasCardinalLT_sigma' {ι : Type w} (α : ι → Type w) (κ : Cardinal.{w}) [Fact κ.IsRegular]
+    (hι : HasCardinalLT ι κ) (hα : ∀ i, HasCardinalLT (α i) κ) :
+    HasCardinalLT (Σ i, α i) κ := by
+  simp only [hasCardinalLT_iff_cardinal_mk_lt] at hι hα ⊢
+  rw [Cardinal.mk_sigma]
+  exact Cardinal.sum_lt_lift_of_isRegular.{w, w} Fact.out (by simpa) hα
+
+lemma hasCardinalLT_sigma {ι : Type u} (α : ι → Type v) (κ : Cardinal.{w}) [Fact κ.IsRegular]
+    (hι : HasCardinalLT ι κ) (hα : ∀ i, HasCardinalLT (α i) κ) :
+    HasCardinalLT (Σ i, α i) κ := by
+  have : Fact (Cardinal.lift.{max u v} κ).IsRegular := ⟨Cardinal.IsRegular.lift Fact.out⟩
+  have := hasCardinalLT_sigma'
+    (fun (i : ULift.{max v w} ι) ↦ ULift.{max u w} (α (ULift.down i)))
+    (Cardinal.lift.{max u v} κ) (by simpa)
+    (fun i ↦ by simpa using hα (ULift.down i))
+  rw [hasCardinalLT_lift_iff] at this
+  exact this.of_surjective (fun ⟨i, a⟩ ↦ ⟨ULift.down i, ULift.down a⟩)
+    (fun ⟨i, a⟩ ↦ ⟨⟨ULift.up i, ULift.up a⟩, rfl⟩)
+
+lemma hasCardinalLT_subtype_iSup
+    {ι : Type*} {X : Type*} (P : ι → X → Prop) {κ : Cardinal} [Fact κ.IsRegular]
+    (hι : HasCardinalLT ι κ) (hP : ∀ i, HasCardinalLT (Subtype (P i)) κ) :
+    HasCardinalLT (Subtype (⨆ i, P i)) κ :=
+  (hasCardinalLT_sigma (fun i ↦ Subtype (P i)) κ hι hP).of_surjective
+    (fun ⟨i, x, hx⟩ ↦ ⟨x, by simp only [iSup_apply, iSup_Prop_eq]; exact ⟨i, hx⟩⟩) (by
+    rintro ⟨_, h⟩
+    simp only [iSup_apply, iSup_Prop_eq] at h
+    obtain ⟨i, hi⟩ := h
+    exact ⟨⟨i, _, hi⟩, rfl⟩)
+
+lemma hasCardinalLT_iUnion
+    {ι : Type*} {X : Type*} (S : ι → Set X) {κ : Cardinal} [Fact κ.IsRegular]
+    (hι : HasCardinalLT ι κ) (hS : ∀ i, HasCardinalLT (S i) κ) :
+    HasCardinalLT (⋃ i, S i) κ := by
+  convert hasCardinalLT_subtype_iSup S hι hS using 2
+  ext x
+  change _ ↔ ((⨆ i, S i) : X → Prop) x
+  aesop
+
+/-- The particular case of `hasCardinatLT_prod` when all the inputs are in the
+same universe `w`. It is used to prove the general case. -/
+lemma hasCardinalLT_prod' {T₁ T₂ : Type w} {κ : Cardinal.{w}} (hκ : Cardinal.aleph0 ≤ κ)
+    (h₁ : HasCardinalLT T₁ κ) (h₂ : HasCardinalLT T₂ κ) :
+    HasCardinalLT (T₁ × T₂) κ := by
+  rw [hasCardinalLT_iff_cardinal_mk_lt] at h₁ h₂ ⊢
+  simpa using Cardinal.mul_lt_of_lt hκ h₁ h₂
+
+lemma hasCardinalLT_prod {T₁ : Type u} {T₂ : Type u'}
+    {κ : Cardinal.{w}} (hκ : Cardinal.aleph0 ≤ κ)
+    (h₁ : HasCardinalLT T₁ κ) (h₂ : HasCardinalLT T₂ κ) :
+    HasCardinalLT (T₁ × T₂) κ := by
+  have := hasCardinalLT_prod' (T₁ := ULift.{max u' w} T₁) (T₂ := ULift.{max u w} T₂)
+    (κ := Cardinal.lift.{max u u'} κ) (by simpa) (by simpa) (by simpa)
+  simp only [hasCardinalLT_lift_iff] at this
+  exact this.of_surjective (fun ⟨x₁, x₂⟩ ↦ ⟨ULift.down x₁, ULift.down x₂⟩) (fun ⟨x₁, x₂⟩ ↦
+    ⟨⟨ULift.up x₁, ULift.up x₂⟩, rfl⟩)
+
 namespace HasCardinalLT
 
 /-- For any `w`-small type `X`, there exists a regular cardinal `κ : Cardinal.{w}`
diff --git a/Mathlib/SetTheory/Cardinal/Regular.lean b/Mathlib/SetTheory/Cardinal/Regular.lean
index 2bd7be04afb8f6..bbe916cfba6e7d 100644
--- a/Mathlib/SetTheory/Cardinal/Regular.lean
+++ b/Mathlib/SetTheory/Cardinal/Regular.lean
@@ -103,6 +103,18 @@ theorem isRegular_aleph_succ (o : Ordinal) : IsRegular (ℵ_ (succ o)) := by
   rw [aleph_succ]
   exact isRegular_succ (aleph0_le_aleph o)
 
+lemma IsRegular.lift {κ : Cardinal.{v}} (h : κ.IsRegular) :
+    (Cardinal.lift.{u} κ).IsRegular := by
+  obtain ⟨h₁, h₂⟩ := h
+  constructor
+  · simpa
+  · rwa [← Cardinal.lift_ord, ← Ordinal.lift_cof, lift_le]
+
+@[simp]
+lemma isRegular_lift_iff {κ : Cardinal.{v}} :
+    (Cardinal.lift.{u} κ).IsRegular ↔ κ.IsRegular :=
+  ⟨fun ⟨h₁, h₂⟩ ↦ ⟨by simpa using h₁, by simpa [← lift_le.{u, v}]⟩, fun h ↦ h.lift⟩
+
 theorem lsub_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c)
     (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c.ord) → Ordinal.lsub.{u, v} f < c.ord :=
   lsub_lt_ord_lift (by rwa [hc.cof_eq])
diff --git a/docs/references.bib b/docs/references.bib
index cfe3f4d8e7d643..b9a0949b3617e4 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -4238,6 +4238,31 @@ @Book{            serre1968
   mrnumber      = {354618}
 }
 
+@Book{            sga-4-tome-1,
+  editor        = {Artin, Michael and Grothendieck, Alexander and Verdier, J.
+                  L. and Bourbaki, N. and Deligne, P. and Saint-Donat,
+                  Bernard},
+  title         = {S{\'e}minaire de g{\'e}om{\'e}trie alg{\'e}brique du
+                  {Bois}-{Marie} 1963--1964. {Th{\'e}orie} des topos et
+                  cohomologie {\'e}tale des sch{\'e}mas. ({SGA} 4). {Un}
+                  s{\'e}minaire dirig{\'e} par {M}. {Artin}, {A}.
+                  {Grothendieck}, {J}. {L}. {Verdier}. {Avec} la
+                  collaboration de {N}. {Bourbaki}, {P}. {Deligne}, {B}.
+                  {Saint}-{Donat}. {Tome} 1: {Th{\'e}orie} des topos.
+                  {Expos{\'e}s} {I} {\`a} {IV}. 2e {\'e}d.},
+  fseries       = {Lecture Notes in Mathematics},
+  series        = {Lect. Notes Math.},
+  issn          = {0075-8434},
+  volume        = {269},
+  year          = {1972},
+  publisher     = {Springer, Cham},
+  language      = {French},
+  doi           = {10.1007/BFb0081551},
+  keywords      = {00B15,14-06},
+  zbMATH        = {3370272},
+  Zbl           = {0234.00007}
+}
+
 @Book{            silverman2009,
   author        = {Silverman, Joseph},
   publisher     = {Springer New York, NY},