Section Greatest_Fixpoints.

Variable F : Set -> Set.

Variable FMON : forall X Y : Set, (X -> Y) -> F X -> F Y.
Notation Fmon := (FMON _ _) (only parsing).

Inductive nu : Set :=
    CoIt : forall X : Set, (X -> F X) -> X -> nu.

Definition Out (m : nu) : F nu :=
  let (X, f, x) return (F nu) := m in FMON _ _ (CoIt X f) (f x).

Definition In (x : F nu) : nu := CoIt (F nu) (FMON _ _ Out) x.

Definition CoRec (X : Set) (f : X -> F (nu + X)) (x : X) : nu :=
  CoIt (nu + X)
    (fun z : nu + X =>
     match z return (F (nu + X)) with
     | inl n => FMON _ _ (inl (A:=nu) X) (Out n)
     | inr y => f y
     end) (inr nu x).

End Greatest_Fixpoints.