fact: Definition O_monad_strength_assoc2 (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).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout