(T:Type) (mu : O T -> T) : mu o (to O T) == idmap -> In O T. Proof. intros H. apply inO_isequiv_to_O. apply isequiv_adjointify with (g:=mu). - refine (O_indpaths (to O T o mu) idmap _). intros x; exact (ap (to O T) (H x)). - exact H. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.