fact: Definition NullHomotopyFrom {X Y} (f:X->Y) := total2 (nullHomotopyFrom f).
imports: UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations