fact: Record BasepointPreservingFunctor (B C : Type) `{Is01Cat B, Is01Cat C} `{IsPointed B, IsPointed C} := { bp_map : B -> C; bp_is0functor : Is0Functor bp_map; bp_pointed : bp_map (point B) $-> point C }.
imports: Basics.Overture Basics.Tactics