{Y X} `(inF F Y) (g h : Y -> F X) (p : fromF F X o g == fromF F X o h) : g == h. Proof. apply ap10. refine (equiv_inj (fun k => fromF F X o k) _). - by apply isequiv_fromF_postcompose. - by apply path_arrow. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.