C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S S' S'' : D
Y Y' : C
T : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
this : (Functor.fromPUnit S).map f.left ≫ B.hom = A.hom ≫ T.map f.right
⊢ A.hom ≫ T.map f.right = B.hom
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S S' S'' : D
Y Y' : C
T : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
⊢ A.hom ≫ T.map f.right = B.hom
have := f.w
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S S' S'' : D
Y Y' : C
T : C ⥤ D
A B : StructuredArrow S T
f : A ⟶ B
this : (Functor.fromPUnit S).map f.left ≫ B.hom = A.hom ≫ T.map f.right
⊢ A.hom ≫ T.map f.right = B.hom
aesop_cat