{A B C : Type} (f : A <~> B) (g : B -> C) `{MapIn O _ _ (g o f)} : MapIn O g := cancelR_isequiv_mapinO f g. Global Instance mapinO_pullback {A B C} (f : B -> A) (g : C -> A) `{MapIn O _ _ g} : MapIn O (f^* g). Proof. intros b. refine (inO_equiv_inO _ (hfiber_pullback_along f g b)^-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.