proposition: Lemma isaprop_NullHomotopyTo {X} {Y} (is:isaset Y) (f:X->Y) : ∥ X ∥ -> isaprop (NullHomotopyTo f).
proof: Proof. apply factor_through_squash. apply isapropisaprop. intros x. apply invproofirrelevance. intros [r i] [s j]. apply subtypePairEquality. - intros n. apply (isaprop_nullHomotopyTo is). - exact (!i x @ j x). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations