Library ZFfixfuntyp

Require Import ZF.
Require Import ZFrelations.
Import IZF.

Require Import ZFord.
Require Import ZFnats.

Section TransfiniteIteration.

  Variable F : set -> set -> set.
  Hypothesis Fmorph : Proper (eq_set ==> eq_set ==> eq_set) F.

Let G f o := sup o (fun o' => F o' (f o')).

Lemma Gmorph : forall o o' f f',
    o == o' -> eq_fun o f f' -> G f o == G f' o'.
Hint Resolve Gmorph.

  Definition TIO := TR G.

  Instance TIO_morph : morph1 TIO.
Qed.

  Lemma TIO_fun_ext : forall x, ext_fun x (fun y => F y (TIO y)).
Hint Resolve TIO_fun_ext.

  Lemma TIO_eq : forall o,
    isOrd o ->
    TIO o == sup o (fun o' => F o' (TIO o')).

  Lemma TIO_intro : forall o o' x,
    isOrd o ->
    lt o' o ->
    x \in F o' (TIO o') ->
    x \in TIO o.

  Lemma TIO_elim : forall o x,
    isOrd o ->
    x \in TIO o ->
    exists2 o', lt o' o & x \in F o' (TIO o').

  Lemma TIO_initial : TIO zero == empty.

  Lemma TIO_typ : forall n X,
    (forall o a, isOrd o -> a \in X -> F o a \in X) ->
    isOrd n ->
    (forall m G, isOrd m -> m \incl n ->
     ext_fun m G ->
     (forall x, lt x m -> G x \in X) -> sup m G \in X) ->
    TIO n \in X.

End TransfiniteIteration.
Hint Resolve TIO_fun_ext.

Section IterMonotone.

  Variable F : set -> set -> set.
  Variable Fmorph : morph2 F.
  Variable Fmono : forall o o', isOrd o -> isOrd o' -> o \incl o' ->
    TIO F o \incl TIO F o' -> F o (TIO F o) \incl F o' (TIO F o').

  Lemma TIO_mono : increasing (TIO F).

  Lemma TIO_incl : forall o, isOrd o ->
    forall o', lt o' o ->
    TIO F o' \incl TIO F o.

  Lemma TIO_mono_succ : forall o,
    isOrd o ->
    TIO F (osucc o) == F o (TIO F o).

End IterMonotone.