Theorem iscontrhomstounit {σ: signature} (A: algebra σ): iscontr (hom A (unitalgebra σ)). Proof. exists (unithom A). intro. apply subtypePairEquality'. - apply proofirrelevancecontr. apply iscontr_sfuntosunit. - apply isapropishom. unfold has_supportsets. intros. apply isasetunit. Defined.
Require Import UniMath.Foundations.All.