{σ} {C : Carriers σ} (A : Algebra σ) (f : forall s, C s -> A s) (s : Sort σ) (T : CarriersTermAlgebra C s) : A s := CarriersTermAlgebra_rec C A f (fun u _ r => u.#A r) s T. Global Instance is_homomorphism_map_term_algebra : @IsHomomorphism σ (TermAlgebra C) A ( A f). Proof. intros u a. by refine (ap u.#A _). Qed.
Require Import