# 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.