(A : Type) : O_functor (@snd Unit A) o O_monad_strength Unit A == @snd Unit (O A). Proof. intros [[] a]. strip_reflections. unfold O_monad_strength, O_functor. simpl. rewrite O_rec_beta. nrapply O_rec_beta. 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.