proposition: Lemma isaset_NullHomotopyTo {X Y} (i:isaset Y) (f:X->Y) : isaset (NullHomotopyTo f).
proof: Proof. intros. apply (isofhleveltotal2 2). { apply i. } intros y. apply impred; intros x. apply isasetaprop. apply i. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations