{A B A' B'} (f : A -> A') (g : B -> B') `{O_inverts f} `{O_inverts g} : O_inverts (functor_sum f g). Proof. apply O_inverts_from_extendable; intros. apply extendable_functor_sum; apply ooextendable_O_inverts; assumption. 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.