{A B} (f : A -> B) : O_functor f o O_monad_mult A == O_monad_mult B o O_functor (O_functor f). Proof. apply O_indpaths; intros x; unfold O_monad_mult. rewrite (to_O_natural (O_functor f) x). rewrite (O_rec_beta idmap x). rewrite (O_rec_beta idmap (O_functor f x)). 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.