fact: Definition typeof_to_O (A : Type) := { OA : Type & { Ou : A -> OA & ((In O OA) * (O_inverts Ou)) }}.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout