(O : Subuniverse) {T : Type} {U : Type} (f : T <~> U) : In O T <-> In O U := (fun H => inO_equiv_inO' _ f, fun H => inO_equiv_inO' _ f^-1).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.