O1 O2 : _ <~> O_eq O1 O2 := ltac:(issig). Global Instance reflexive_O_eq : Reflexive O_eq | 10. Proof. intros; split; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.