{Y X} `(inF F Y) (f : Y -> X) : Y -> F X. Proof. refine ((fun (g : Y -> F X) => fromF F X o g)^-1 f). by apply isequiv_fromF_postcompose. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.