fact: Definition O_monad_strength_unitlaw1 (A : Type) : O_functor (@snd Unit A) o O_monad_strength Unit A == @snd Unit (O A).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout