(O : Subuniverse) : Subuniverse. Proof. unshelve econstructor. - intros A; exact (forall (x y:A), In O (x = y)). - exact _. - intros T U ? f ? x y; cbn in *. refine (inO_equiv_inO' _ (equiv_ap f^-1 x y)^-1). 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.