(A B : Type) `{In O B} (s : A -> B) (r : B -> A) (K : r o s == idmap) : In O A. Proof. nrapply (inO_to_O_retract A (r o (to O B)^-1 o (O_functor s))). intro a. lhs exact (ap (r o (to O B)^-1) (to_O_natural s a)). lhs nrefine (ap r (eissect _ (s a))). apply K. 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.