proposition: Lemma isweq_to_isweq_unit {X:UU} (f g:X->unit) : isweq f -> isweq g.
proof: Proof. intros i. assert (h : f ~ g). { intros t. apply isProofIrrelevantUnit. } exact (isweqhomot f g h i). Defined.
imports: UniMath.Foundations.Preamble