{A B X Y : Type} `{In O X} `{In O Y} (f : A -> X) (g : B -> Y) : O_rec (functor_prod f g) == prod_coind (O_rec (f o fst : A * B -> X)) (O_rec (g o snd : A * B -> Y)). Proof. apply O_indpaths; intro ab. unfold functor_prod, prod_coind, prod_coind_uncurried; simpl. lhs (nrapply O_rec_beta). apply path_prod; cbn; symmetry; nrapply O_rec_beta. 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.