C : Type u
inst✝¹ : Category C
D : Type ?u.86593
inst✝ : Category D
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : universally P f
⊢ P f
C : Type u
inst✝¹ : Category C
D : Type ?u.86593
inst✝ : Category D
P : MorphismProperty C
⊢ universally P ≤ P
intro X Y f hf
no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.86593
inst✝ : Category D
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : universally P f
⊢ P f
exact hf (𝟙 _) (𝟙 _) _ (IsPullback.of_vert_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩)
no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.86593
inst✝ : Category D
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : universally P f
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
rw [Category.comp_id, Category.id_comp]