(A A' B B' : Type) (f : A -> A') (g : B -> B') : O_functor (functor_prod f g) o O_monad_strength A B == O_monad_strength A' B' o functor_prod f (O_functor g). Proof. intros [a b]. revert a. apply ap10. strip_reflections. apply path_arrow; intros a. unfold O_monad_strength, O_functor; simpl. repeat rewrite O_rec_beta. reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.