C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso f.right).inv) ≫ T.map (Subobject.arrow (Subobject.mk f.right)) = A.hom
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).right).inv) ≫
      T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) =
    A.hom
dsimp
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso f.right).inv) ≫ T.map (Subobject.arrow (Subobject.mk f.right)) = A.hom
simp [← T.map_comp]