fact: Definition O_monad_strength_unitlaw2 (A B : Type) : O_monad_strength A B o functor_prod idmap (to O B) == to O (A*B).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout