{A} (P : A -> Type) : O {x:A & O (P x)} <~> O {x:A & P x}. Proof. srapply equiv_adjointify. - apply O_rec; intros [a op]; revert op. apply O_rec; intros p. exact (to O _ (a;p)). - apply O_functor. exact (functor_sigma idmap (fun x => to O (P x))). - unfold O_functor; rapply O_indpaths. intros [a p]; simpl. abstract (repeat (rewrite O_rec_beta); reflexivity). - unfold O_functor; rapply O_indpaths. intros [a op]; revert op; rapply O_indpaths; intros p; simpl. abstract (repeat (rewrite O_rec_beta); reflexivity). 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.