(A B C : Type) : O_functor (equiv_prod_assoc A B C)^-1 o O_monad_strength (A*B) C == O_monad_strength A (B*C) o functor_prod idmap (O_monad_strength B C) o (equiv_prod_assoc A B (O C))^-1. Proof. intros [[a b] c]. revert a; apply ap10. revert b; apply ap10. strip_reflections. apply path_arrow; intros b. apply path_arrow; intros a. unfold O_monad_strength, O_functor, functor_prod. 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.