apply Hom.ext
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
⊢ hom = Term.algebraHom target f
case a
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
⊢ hom.hom = (Term.algebraHom target f).hom