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