(A : Type) : O_monad_mult A o (O_functor (to O A)) == idmap. Proof. apply O_indpaths; intros x; unfold O_monad_mult, O_functor. repeat rewrite O_rec_beta. 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.