proposition: Theorem iscontrhomstounit {σ: signature} (A: algebra σ): iscontr (hom A (unitalgebra σ)).
proof: Proof. exists (unithom A). intro. apply subtypePairEquality'. - apply proofirrelevancecontr. apply iscontr_sfuntosunit. - apply isapropishom. unfold has_supportsets. intros. apply isasetunit. Defined.
imports: UniMath.Foundations.All UniMath.Algebra.Universal.SortedTypes UniMath.Algebra.Universal.Signatures