X : IsEquiv (O_functor (Op U) (fromF coOp X)). Proof. refine (isequiv_adjointify _ (fun ux => fun u => (ux u , u)) _ _). - intros ux; simpl in *. apply path_arrow; intros u. transitivity (O_functor (Op U) fst (to (Op U) (X * U) (ux u , u)) u). + apply ap10, ap, path_arrow; intros u'; simpl in *. apply path_prod; simpl; [ apply ap | ]; apply path_ishprop. + exact (ap10 (to_O_natural (Op U) (@fst X U) (ux u , u)) u). - intros uux; simpl in *. apply path_arrow; intros u. apply path_prod; [ simpl | apply path_ishprop ]. transitivity (O_functor (Op U) fst (to (Op U) _ (fst (uux u) , u)) u). + apply ap10, ap, path_arrow; intros u'. apply path_prod; simpl. * exact (ap fst (ap uux (path_ishprop u' u))). * apply path_ishprop. + exact (ap10 (to_O_natural (Op U) (@fst X U) (fst (uux u) , u)) u). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.