diff --git a/Mathlib.lean b/Mathlib.lean
index 93617be7efc12..d4ccdcc497893 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1712,6 +1712,7 @@ import Mathlib.CategoryTheory.Limits.IsConnected
 import Mathlib.CategoryTheory.Limits.IsLimit
 import Mathlib.CategoryTheory.Limits.Lattice
 import Mathlib.CategoryTheory.Limits.MonoCoprod
+import Mathlib.CategoryTheory.Limits.MorphismProperty
 import Mathlib.CategoryTheory.Limits.Opposites
 import Mathlib.CategoryTheory.Limits.Over
 import Mathlib.CategoryTheory.Limits.Pi
diff --git a/Mathlib/CategoryTheory/Comma/Basic.lean b/Mathlib/CategoryTheory/Comma/Basic.lean
index 01cb2d222b041..654d109cac4f1 100644
--- a/Mathlib/CategoryTheory/Comma/Basic.lean
+++ b/Mathlib/CategoryTheory/Comma/Basic.lean
@@ -163,7 +163,7 @@ theorem eqToHom_right (X Y : Comma L R) (H : X = Y) :
 
 section
 
-variable {X Y : Comma L R} (e : X ⟶ Y)
+variable {L R} {X Y : Comma L R} (e : X ⟶ Y)
 
 instance [IsIso e] : IsIso e.left :=
   (Comma.fst L R).map_isIso e
diff --git a/Mathlib/CategoryTheory/IsConnected.lean b/Mathlib/CategoryTheory/IsConnected.lean
index fc0e0c664675e..96bb16ce5927a 100644
--- a/Mathlib/CategoryTheory/IsConnected.lean
+++ b/Mathlib/CategoryTheory/IsConnected.lean
@@ -42,7 +42,7 @@ category is preserved by the functor `(X × -)`. This appears in `CategoryTheory
 -/
 
 
-universe v₁ v₂ u₁ u₂
+universe w₁ w₂ v₁ v₂ u₁ u₂
 
 noncomputable section
 
@@ -419,9 +419,7 @@ def discreteIsConnectedEquivPUnit {α : Type u₁} [IsConnected (Discrete α)] :
       unitIso := isoConstant _ (Classical.arbitrary _)
       counitIso := Functor.punitExt _ _ }
 
-universe v u
-
-variable {C : Type u} [Category.{v} C]
+variable {C : Type w₂} [Category.{w₁} C]
 
 /-- For objects `X Y : C`, any natural transformation `α : const X ⟶ const Y` from a connected
 category must be constant.
diff --git a/Mathlib/CategoryTheory/Limits/Comma.lean b/Mathlib/CategoryTheory/Limits/Comma.lean
index 5e5e2804c305b..f67006d4500bf 100644
--- a/Mathlib/CategoryTheory/Limits/Comma.lean
+++ b/Mathlib/CategoryTheory/Limits/Comma.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Comma.Arrow
-import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
+import Mathlib.CategoryTheory.Comma.Over
 import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 import Mathlib.CategoryTheory.Limits.Creates
 import Mathlib.CategoryTheory.Limits.Unit
@@ -225,6 +225,10 @@ namespace CostructuredArrow
 
 variable {G : A ⥤ T} {X : T} (F : J ⥤ CostructuredArrow G X)
 
+instance hasTerminal [G.Faithful] [G.Full] {Y : A} :
+    HasTerminal (CostructuredArrow G (G.obj Y)) :=
+  CostructuredArrow.mkIdTerminal.hasTerminal
+
 instance hasColimit [i₁ : HasColimit (F ⋙ proj G X)] [i₂ : PreservesColimit (F ⋙ proj G X) G] :
     HasColimit F := by
   haveI : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁
@@ -262,4 +266,10 @@ theorem epi_iff_epi_left [HasPushouts A] [PreservesColimitsOfShape WalkingSpan G
 
 end CostructuredArrow
 
+namespace Over
+
+instance {X : T} : HasTerminal (Over X) := CostructuredArrow.hasTerminal
+
+end Over
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/MorphismProperty.lean b/Mathlib/CategoryTheory/Limits/MorphismProperty.lean
new file mode 100644
index 0000000000000..a54a535246793
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/MorphismProperty.lean
@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.CategoryTheory.Limits.Comma
+import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
+import Mathlib.CategoryTheory.Limits.FullSubcategory
+import Mathlib.CategoryTheory.MorphismProperty.Comma
+import Mathlib.CategoryTheory.MorphismProperty.Limits
+
+/-!
+# (Co)limits in subcategories of comma categories defined by morphism properties
+
+-/
+
+namespace CategoryTheory
+
+open Limits MorphismProperty.Comma
+
+variable {T : Type*} [Category T] (P : MorphismProperty T)
+
+namespace MorphismProperty.Comma
+
+variable {A B J : Type*} [Category A] [Category B] [Category J] {L : A ⥤ T} {R : B ⥤ T}
+variable (D : J ⥤ P.Comma L R ⊤ ⊤)
+
+/-- If `P` is closed under limits of shape `J` in `Comma L R`, then when `D` has
+a limit in `Comma L R`, the forgetful functor creates this limit. -/
+noncomputable def forgetCreatesLimitOfClosed
+    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom))
+    [HasLimit (D ⋙ forget L R P ⊤ ⊤)] :
+    CreatesLimit D (forget L R P ⊤ ⊤) :=
+  createsLimitOfFullyFaithfulOfIso
+    (⟨limit (D ⋙ forget L R P ⊤ ⊤), h.limit fun j ↦ (D.obj j).prop⟩)
+    (Iso.refl _)
+
+/-- If `Comma L R` has limits of shape `J` and `Comma L R` is closed under limits of shape
+`J`, then `forget L R P ⊤ ⊤` creates limits of shape `J`. -/
+noncomputable def forgetCreatesLimitsOfShapeOfClosed [HasLimitsOfShape J (Comma L R)]
+    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom)) :
+    CreatesLimitsOfShape J (forget L R P ⊤ ⊤) where
+  CreatesLimit := forgetCreatesLimitOfClosed _ _ h
+
+lemma hasLimit_of_closedUnderLimitsOfShape
+    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom))
+    [HasLimit (D ⋙ forget L R P ⊤ ⊤)] :
+    HasLimit D :=
+  haveI : CreatesLimit D (forget L R P ⊤ ⊤) := forgetCreatesLimitOfClosed _ D h
+  hasLimit_of_created D (forget L R P ⊤ ⊤)
+
+lemma hasLimitsOfShape_of_closedUnderLimitsOfShape [HasLimitsOfShape J (Comma L R)]
+    (h : ClosedUnderLimitsOfShape J (fun f : Comma L R ↦ P f.hom)) :
+    HasLimitsOfShape J (P.Comma L R ⊤ ⊤) where
+  has_limit _ := hasLimit_of_closedUnderLimitsOfShape _ _ h
+
+end MorphismProperty.Comma
+
+section
+
+variable {A : Type*} [Category A] {L : A ⥤ T}
+
+lemma CostructuredArrow.closedUnderLimitsOfShape_discrete_empty [L.Faithful] [L.Full] {Y : A}
+    [P.ContainsIdentities] [P.RespectsIso] :
+    ClosedUnderLimitsOfShape (Discrete PEmpty.{1})
+      (fun f : CostructuredArrow L (L.obj Y) ↦ P f.hom) := by
+  rintro D c hc -
+  have : D = Functor.empty _ := Functor.empty_ext' _ _
+  subst this
+  let e : c.pt ≅ CostructuredArrow.mk (𝟙 (L.obj Y)) :=
+    hc.conePointUniqueUpToIso CostructuredArrow.mkIdTerminal
+  rw [P.costructuredArrow_iso_iff e]
+  simpa using P.id_mem (L.obj Y)
+
+end
+
+section
+
+variable {X : T}
+
+lemma Over.closedUnderLimitsOfShape_discrete_empty [P.ContainsIdentities] [P.RespectsIso] :
+    ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) (fun f : Over X ↦ P f.hom) :=
+  CostructuredArrow.closedUnderLimitsOfShape_discrete_empty P
+
+/-- Let `P` be stable under composition and base change. If `P` satisfies cancellation on the right,
+the subcategory of `Over X` defined by `P` is closed under pullbacks.
+
+Without the cancellation property, this does not in general. Consider for example
+`P = Function.Surjective` on `Type`. -/
+lemma Over.closedUnderLimitsOfShape_pullback [HasPullbacks T]
+    [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange)
+    (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (f ≫ g) → P f) :
+    ClosedUnderLimitsOfShape WalkingCospan (fun f : Over X ↦ P f.hom) := by
+  intro D c hc hf
+  have h : IsPullback (c.π.app .left).left (c.π.app .right).left (D.map WalkingCospan.Hom.inl).left
+        (D.map WalkingCospan.Hom.inr).left := IsPullback.of_isLimit_cone <|
+    Limits.isLimitOfPreserves (CategoryTheory.Over.forget X) hc
+  rw [show c.pt.hom = (c.π.app .left).left ≫ (D.obj .left).hom by simp]
+  apply P.comp_mem _ _ (hP h.flip ?_) (hf _)
+  exact of_postcomp (D.obj WalkingCospan.one).hom (hf .one) (by simpa using hf .right)
+
+end
+
+namespace MorphismProperty.Over
+
+variable (X : T)
+
+noncomputable instance [P.ContainsIdentities] [P.RespectsIso] :
+    CreatesLimitsOfShape (Discrete PEmpty.{1}) (Over.forget P ⊤ X) :=
+  haveI : HasLimitsOfShape (Discrete PEmpty.{1}) (Comma (𝟭 T) (Functor.fromPUnit X)) := by
+    show HasLimitsOfShape _ (Over X)
+    infer_instance
+  forgetCreatesLimitsOfShapeOfClosed P
+    (Over.closedUnderLimitsOfShape_discrete_empty _)
+
+variable {X} in
+instance [P.ContainsIdentities] (Y : P.Over ⊤ X) :
+    Unique (Y ⟶ Over.mk ⊤ (𝟙 X) (P.id_mem X)) where
+  default := Over.homMk Y.hom
+  uniq a := by
+    ext
+    · simp only [mk_left, Hom.hom_left, homMk_hom, Over.homMk_left]
+      rw [← Over.w a.hom]
+      simp only [mk_left, Functor.const_obj_obj, Hom.hom_left, mk_hom, Category.comp_id]
+    · rfl
+
+/-- `X ⟶ X` is the terminal object of `P.Over ⊤ X`. -/
+def mkIdTerminal [P.ContainsIdentities] :
+    IsTerminal (Over.mk ⊤ (𝟙 X) (P.id_mem X)) :=
+  IsTerminal.ofUnique _
+
+instance [P.ContainsIdentities] : HasTerminal (P.Over ⊤ X) :=
+  let h : IsTerminal (Over.mk ⊤ (𝟙 X) (P.id_mem X)) := Over.mkIdTerminal P X
+  h.hasTerminal
+
+/-- If `P` is stable under composition, base change and satisfies post-cancellation,
+`Over.forget P ⊤ X` creates pullbacks. -/
+noncomputable def createsLimitsOfShape_walkingCospan [HasPullbacks T]
+    [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange)
+    (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (f ≫ g) → P f) :
+    CreatesLimitsOfShape WalkingCospan (Over.forget P ⊤ X) :=
+  haveI : HasLimitsOfShape WalkingCospan (Comma (𝟭 T) (Functor.fromPUnit X)) :=
+    inferInstanceAs <| HasLimitsOfShape WalkingCospan (Over X)
+  forgetCreatesLimitsOfShapeOfClosed P
+    (Over.closedUnderLimitsOfShape_pullback P hP of_postcomp)
+
+/-- If `P` is stable under composition, base change and satisfies post-cancellation,
+`P.Over ⊤ X` has pullbacks -/
+lemma hasPullbacks [HasPullbacks T] [P.IsStableUnderComposition] (hP : P.StableUnderBaseChange)
+    (of_postcomp : ∀ {X Y Z : T} {f : X ⟶ Y} (g : Y ⟶ Z), P g → P (f ≫ g) → P f) :
+    HasPullbacks (P.Over ⊤ X) :=
+  haveI : HasLimitsOfShape WalkingCospan (Comma (𝟭 T) (Functor.fromPUnit X)) :=
+    inferInstanceAs <| HasLimitsOfShape WalkingCospan (Over X)
+  hasLimitsOfShape_of_closedUnderLimitsOfShape P
+    (Over.closedUnderLimitsOfShape_pullback P hP of_postcomp)
+
+end MorphismProperty.Over
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
index 44fa57f388d94..ff8b0b942c59c 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
@@ -228,6 +228,13 @@ theorem of_isLimit' (w : CommSq fst snd f g) (h : Limits.IsLimit w.cone) :
     IsPullback fst snd f g :=
   of_isLimit h
 
+/-- Variant of `of_isLimit` for an arbitrary cone on a diagram `WalkingCospan ⥤ C`. -/
+lemma of_isLimit_cone {D : WalkingCospan ⥤ C} {c : Cone D} (hc : IsLimit c) :
+    IsPullback (c.π.app .left) (c.π.app .right) (D.map WalkingCospan.Hom.inl)
+      (D.map WalkingCospan.Hom.inr) where
+  w := by simp_rw [Cone.w]
+  isLimit' := ⟨IsLimit.equivOfNatIsoOfIso _ _ _ (PullbackCone.isoMk c) hc⟩
+
 /-- The pullback provided by `HasPullback f g` fits into an `IsPullback`. -/
 theorem of_hasPullback (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
     IsPullback (pullback.fst f g) (pullback.snd f g) f g :=
@@ -428,6 +435,13 @@ theorem of_isColimit' (w : CommSq f g inl inr) (h : Limits.IsColimit w.cocone) :
     IsPushout f g inl inr :=
   of_isColimit h
 
+/-- Variant of `of_isColimit` for an arbitrary cocone on a diagram `WalkingSpan ⥤ C`. -/
+lemma of_isColimit_cocone {D : WalkingSpan ⥤ C} {c : Cocone D} (hc : IsColimit c) :
+    IsPushout (D.map WalkingSpan.Hom.fst) (D.map WalkingSpan.Hom.snd)
+      (c.ι.app .left) (c.ι.app .right) where
+  w := by simp_rw [Cocone.w]
+  isColimit' := ⟨IsColimit.equivOfNatIsoOfIso _ _ _ (PushoutCocone.isoMk c) hc⟩
+
 /-- The pushout provided by `HasPushout f g` fits into an `IsPushout`. -/
 theorem of_hasPushout (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g] :
     IsPushout f g (pushout.inl f g) (pushout.inr f g) :=
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean
index 0a3a382da8016..cf9f01545d900 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.CategoryTheory.Comma.Arrow
-import Mathlib.CategoryTheory.Pi.Basic
 import Mathlib.Order.CompleteBooleanAlgebra
 
 /-!
@@ -196,10 +195,14 @@ theorem cancel_right_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P
     (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f :=
   ⟨fun h => by simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h, RespectsIso.postcomp P g f⟩
 
+lemma comma_iso_iff (P : MorphismProperty C) [P.RespectsIso] {A B : Type*} [Category A] [Category B]
+    {L : A ⥤ C} {R : B ⥤ C} {f g : Comma L R} (e : f ≅ g) :
+    P f.hom ↔ P g.hom := by
+  simp [← Comma.inv_left_hom_right e.hom, cancel_left_of_respectsIso, cancel_right_of_respectsIso]
+
 theorem arrow_iso_iff (P : MorphismProperty C) [RespectsIso P] {f g : Arrow C}
-    (e : f ≅ g) : P f.hom ↔ P g.hom := by
-  simp [← Arrow.inv_left_hom_right e.hom, cancel_left_of_respectsIso,
-    cancel_right_of_respectsIso]
+    (e : f ≅ g) : P f.hom ↔ P g.hom :=
+  P.comma_iso_iff e
 
 theorem arrow_mk_iso_iff (P : MorphismProperty C) [RespectsIso P] {W X Y Z : C}
     {f : W ⟶ X} {g : Y ⟶ Z} (e : Arrow.mk f ≅ Arrow.mk g) : P f ↔ P g :=
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Comma.lean b/Mathlib/CategoryTheory/MorphismProperty/Comma.lean
index 605734da78131..0662c8046f120 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/Comma.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@@ -41,6 +41,15 @@ section Comma
 variable {A : Type*} [Category A] {B : Type*} [Category B] {T : Type*} [Category T]
   (L : A ⥤ T) (R : B ⥤ T)
 
+lemma costructuredArrow_iso_iff (P : MorphismProperty T) [P.RespectsIso]
+    {L : A ⥤ T} {X : T} {f g : CostructuredArrow L X} (e : f ≅ g) :
+    P f.hom ↔ P g.hom :=
+  P.comma_iso_iff e
+
+lemma over_iso_iff (P : MorphismProperty T) [P.RespectsIso] {X : T} {f g : Over X} (e : f ≅ g) :
+    P f.hom ↔ P g.hom :=
+  P.comma_iso_iff e
+
 variable (P : MorphismProperty T) (Q : MorphismProperty A) (W : MorphismProperty B)
 
 /-- `P.Comma L R Q W` is the subcategory of `Comma L R` consisting of
@@ -70,6 +79,12 @@ lemma Hom.hom_mk {X Y : P.Comma L R Q W}
     (f : CommaMorphism X.toComma Y.toComma) (hf) (hg) :
   Comma.Hom.hom ⟨f, hf, hg⟩ = f := rfl
 
+@[simp]
+lemma Hom.hom_left {X Y : P.Comma L R Q W} (f : Comma.Hom X Y) : f.hom.left = f.left := rfl
+
+@[simp]
+lemma Hom.hom_right {X Y : P.Comma L R Q W} (f : Comma.Hom X Y) : f.hom.right = f.right := rfl
+
 /-- See Note [custom simps projection] -/
 def Hom.Simps.hom {X Y : P.Comma L R Q W} (f : X.Hom Y) :
     X.toComma ⟶ Y.toComma :=
@@ -194,38 +209,59 @@ end Comma
 
 section Over
 
-variable {T : Type*} [Category T]
+variable {T : Type*} [Category T] (P Q : MorphismProperty T) (X : T) [Q.IsMultiplicative]
 
 /-- Given a morphism property `P` on a category `C` and an object `X : C`, this is the
 subcategory of `Over X` defined by `P` where morphisms satisfy `Q`. -/
-protected abbrev Over (P Q : MorphismProperty T) (X : T) : Type _ :=
-  P.Comma (Functor.id T) (Functor.fromPUnit X) Q ⊤
+protected abbrev Over : Type _ :=
+  P.Comma (Functor.id T) (Functor.fromPUnit.{0} X) Q ⊤
 
-variable (P Q : MorphismProperty T) [Q.IsMultiplicative] (X : T)
+/-- The forgetful functor from the full subcategory of `Over X` defined by `P` to `Over X`. -/
+protected abbrev Over.forget : P.Over Q X ⥤ Over X :=
+  Comma.forget (Functor.id T) (Functor.fromPUnit.{0} X) P Q ⊤
+
+variable {P Q X}
 
-/-- Construct a morphism in `P.Over Q X` from a morphism in `Over X`. -/
+/-- Construct a morphism in `P.Over Q X` from a morphism in `Over.X`. -/
 @[simps hom]
 def Over.Hom.mk {A B : P.Over Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.left) : A ⟶ B where
   __ := f
   prop_hom_left := hf
   prop_hom_right := trivial
 
-/-- The forgetful functor from the full subcategory of `Over X` defined by `P` to `Over X`. -/
-protected abbrev Over.forget : P.Over Q X ⥤ Over X :=
-  Comma.forget (Functor.id T) (Functor.fromPUnit X) P Q ⊤
+variable (Q) in
+/-- Make an object of `P.Over Q X` from a morphism `f : A ⟶ X` and a proof of `P f`. -/
+@[simps hom left]
+protected def Over.mk {A : T} (f : A ⟶ X) (hf : P f) : P.Over Q X where
+  left := A
+  right := ⟨⟨⟩⟩
+  hom := f
+  prop := hf
+
+/-- Make a morphism in `P.Over Q X` from a morphism in `T` with compatibilities. -/
+@[simps hom]
+protected def Over.homMk {A B : P.Over Q X} (f : A.left ⟶ B.left)
+    (w : f ≫ B.hom = A.hom := by aesop_cat) (hf : Q f := by trivial) : A ⟶ B where
+  __ := CategoryTheory.Over.homMk f w
+  prop_hom_left := hf
+  prop_hom_right := trivial
 
 end Over
 
 section Under
 
-variable {T : Type*} [Category T]
+variable {T : Type*} [Category T] (P Q : MorphismProperty T) (X : T) [Q.IsMultiplicative]
 
 /-- Given a morphism property `P` on a category `C` and an object `X : C`, this is the
 subcategory of `Under X` defined by `P` where morphisms satisfy `Q`. -/
-protected abbrev Under (P Q : MorphismProperty T) (X : T) : Type _ :=
-  P.Comma (Functor.fromPUnit X) (Functor.id T) ⊤ Q
+protected abbrev Under : Type _ :=
+  P.Comma (Functor.fromPUnit.{0} X) (Functor.id T) ⊤ Q
+
+/-- The forgetful functor from the full subcategory of `Under X` defined by `P` to `Under X`. -/
+protected abbrev Under.forget : P.Under Q X ⥤ Under X :=
+  Comma.forget (Functor.fromPUnit.{0} X) (Functor.id T) P ⊤ Q
 
-variable (P Q : MorphismProperty T) [Q.IsMultiplicative] (X : T)
+variable {P Q X}
 
 /-- Construct a morphism in `P.Under Q X` from a morphism in `Under.X`. -/
 @[simps hom]
@@ -234,9 +270,22 @@ def Under.Hom.mk {A B : P.Under Q X} (f : A.toComma ⟶ B.toComma) (hf : Q f.rig
   prop_hom_left := trivial
   prop_hom_right := hf
 
-/-- The forgetful functor from the full subcategory of `Under X` defined by `P` to `Under X`. -/
-protected abbrev Under.forget : P.Under Q X ⥤ Under X :=
-  Comma.forget (Functor.fromPUnit X) (Functor.id T) P ⊤ Q
+variable (Q) in
+/-- Make an object of `P.Under Q X` from a morphism `f : A ⟶ X` and a proof of `P f`. -/
+@[simps hom left]
+protected def Under.mk {A : T} (f : X ⟶ A) (hf : P f) : P.Under Q X where
+  left := ⟨⟨⟩⟩
+  right := A
+  hom := f
+  prop := hf
+
+/-- Make a morphism in `P.Under Q X` from a morphism in `T` with compatibilities. -/
+@[simps hom]
+protected def Under.homMk {A B : P.Under Q X} (f : A.right ⟶ B.right)
+    (w : A.hom ≫ f = B.hom := by aesop_cat) (hf : Q f := by trivial) : A ⟶ B where
+  __ := CategoryTheory.Under.homMk f w
+  prop_hom_left := trivial
+  prop_hom_right := hf
 
 end Under