fact: Definition O_prod_unit (A B : Type) : A * B -> O A * O B := functor_prod (to O A) (to O B).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout