fact: Definition O_monad_unitlaw2 (A : Type) : O_monad_mult A o (O_functor (to O A)) == idmap.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout