{A B : Type} `{In O B} (f : A -> B) `{IsConnMap O _ _ f} : IsEquiv (O_rec (O := O) f). Proof. refine (isequiv_adjointify _ (conn_map_elim f (fun _ => O A) (to O A)) _ _). - intros x. pattern x. refine (conn_map_elim f _ _ x); intros a. exact (ap (O_rec f) (conn_map_comp f (fun _ => O A) (to O A) a) @ O_rec_beta f a). - apply O_indpaths; intros a; simpl. refine (ap _ (O_rec_beta f a) @ _). refine (conn_map_comp f (fun _ => O A) (to O A) a). 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.