fact: Definition OO_inverts_functor_pushout (O O' : ReflectiveSubuniverse) `{O' <= Sep O} {A B C A' B' C'} (f : A -> B) (g : A -> C) {f' : A' -> B'} {g' : A' -> C'} (h : A -> A') (k : B -> B') (l : C -> C') (p : k o f == f' o h) (q : l o g == g' o h) `{IsConnMap O _ _ h} `{O_inverts O' k} `{O_inverts O' l} : O_inverts O' (functor_pushout h k l p q).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout