case mk
T : Type u
inst✝ : Category T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk { left := left✝, right := right✝, hom := hom✝ }.hom = { left := left✝, right := right✝, hom := hom✝ }
T : Type u
inst✝ : Category T
f : Arrow T
⊢ mk f.hom = f
cases f
no goals
case mk
T : Type u
inst✝ : Category T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk { left := left✝, right := right✝, hom := hom✝ }.hom = { left := left✝, right := right✝, hom := hom✝ }
rfl