{fs : Funext} (A B C : Type) `{In O C} : ((O A) * (O B) -> C) <~> (A * B -> C) := Build_Equiv _ _ _ (isequiv_O_prod_unit_precompose A B C). Global Instance O_inverts_O_prod_unit (A B : Type) : O_inverts (O_prod_unit A B). Proof. rapply O_inverts_from_extendable. intros; rapply ooextendable_O_prod_unit. 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.