{fs : Funext} (A B C : Type) `{In O C} : IsEquiv (fun (f : (O A) * (O B) -> C) => f o O_prod_unit A B). Proof. rapply isequiv_ooextendable. 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.