rfl
V₁ : Type u_5
E₁ : Type u_6
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
⊢ (comp g f).toFuncE = g.toFuncE ∘ f.toFuncE
no goals