case mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
T T' T'' : D
Y Y' : C
S : C ⥤ D
left✝ : C
right✝ : Discrete PUnit
hom✝ : S.obj left✝ ⟶ (Functor.fromPUnit T).obj right✝
⊢ { left := left✝, right := right✝, hom := hom✝ } = mk { left := left✝, right := right✝, hom := hom✝ }.hom
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
T T' T'' : D
Y Y' : C
S : C ⥤ D
f : CostructuredArrow S T
⊢ f = mk f.hom
cases f
no goals
case mk
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
T T' T'' : D
Y Y' : C
S : C ⥤ D
left✝ : C
right✝ : Discrete PUnit
hom✝ : S.obj left✝ ⟶ (Functor.fromPUnit T).obj right✝
⊢ { left := left✝, right := right✝, hom := hom✝ } = mk { left := left✝, right := right✝, hom := hom✝ }.hom
congr