{Y X} (YF : inF F Y) (f : Y -> X) : fromF F X o F_corec YF f == f. Proof. apply ap10, (eisretr (fun g => fromF F X o g)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.