{X Y} (f : X -> Y) : F X -> F Y := F_corec (F_inF F X) (f o fromF F X). Local Instance ishprop_coreflection A `{IsHProp A} : IsHProp (F A). Proof. apply hprop_allpath; intros x y. exact (F_coindpaths (F_inF F A) (const x) (const y) (fun _ => path_ishprop _ _) x). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.