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

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