Definition iscontrhomsfromgterm (a: algebra σ) (setprop: has_supportsets a) : iscontr (term_algebra σ ↷ a). Proof. exists (gevalhom a). intro f. apply subtypePairEquality'. - apply gevalhom_is_unique. - apply isapropishom. exact setprop. Defined.
Require Import UniMath.Foundations.All.