(A B : Type) : O_prod_cmp A B == prod_coind (O_rec (to O _ o fst : A * B -> O A)) (O_rec (to O _ o snd : A * B -> O B)) := O_rec_functor_prod _ _. Global Instance inO_pullback {A B C} (f : B -> A) (g : C -> A) `{In O A} `{In O B} `{In O C} : In O (Pullback f g). Proof. srapply inO_to_O_retract. - intros op. exists (O_rec pr1 op). exists (O_rec (fun p => p.2.1) op). revert op; apply O_indpaths; intros [b [c a]]. refine (ap f (O_rec_beta _ _) @ _); cbn. refine (a @ ap g (O_rec_beta _ _)^). - intros [b [c a]]; cbn. srapply path_sigma'. { apply O_rec_beta. } refine (transport_sigma' _ _ @ _); cbn. srapply path_sigma'. { apply O_rec_beta. } abstract ( rewrite transport_paths_Fr; rewrite transport_paths_Fl; rewrite O_indpaths_beta; rewrite concat_V_pp; rewrite ap_V; apply concat_pV_p ). 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.