X (s : X -> F X) (p : fromF F X o s == idmap) : inF F X. Proof. refine (transport (inF F) (path_universe (fromF F X)) (F_inF F X)). refine (isequiv_adjointify _ s p _). change (s o fromF F X == idmap). apply F_coindpaths; try apply F_inF. intros x; apply p. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.