(A B : Type) : O_monad_mult (A*B) o O_functor (O_monad_strength A B) o O_monad_strength A (O B) == O_monad_strength A B o functor_prod idmap (O_monad_mult B). Proof. intros [a b]. revert a; apply ap10. strip_reflections. apply path_arrow; intros a. unfold O_monad_strength, O_functor, O_monad_mult, functor_prod. simpl. repeat (rewrite O_rec_beta; simpl). 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.