{A B C : Type} (f : A -> B) (g : B -> C) `{IsEquiv _ _ f} `{MapIn O _ _ (g o f)} : MapIn O g. Proof. intros b. srefine (inO_equiv_inO' (hfiber (g o f) b) _). exact (equiv_functor_sigma f (fun a => 1%equiv)). 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.