(A B : Type) : A * O B -> O (A * B) := fun aob => O_rec (fun b a => to O (A*B) (a,b)) (snd aob) (fst aob).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.