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