X : inF F X <~> (X -> F Unit). Proof. apply equiv_iff_hprop. - intros ?. apply F_corec; try assumption. exact (fun _ => tt). - intros f. simple refine (inF_fromF_sect X _ _). + intros x. exact (F_functor (unit_name x) (f x)). + intros x; unfold F_functor. exact (F_corec_beta (F_inF F Unit) (const x) (f x)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.