Definition iscontr_universalmap (setprop: has_supportsets a) : iscontr (∑ h: free_algebra σ V ↷ a, ∏ v: V, h (varsort v) (varterm v) = α v). Proof. exists universalmap. intro h. induction h as [h honvars]. apply subtypePairEquality'. - apply subtypePairEquality'. + apply universalmap_is_unique. assumption. + apply isapropishom. assumption. - apply impred_isaprop. intros. apply (setprop (varsort t)). Defined.
Require Import UniMath.Foundations.All.