# Library ZFindtypes

Require Export basic.
Require Import ZF ZFsum ZFfix ZFnats ZFord ZFrelations.
Import IZF ZFrepl.

Lemma cst_is_ext : forall X o, ext_fun o (fun _ => X).
Hint Resolve cst_is_ext.

Lemma sum_is_ext : forall o F G,
ext_fun o F ->
ext_fun o G ->
ext_fun o (fun y => sum (F y) (G y)).
Hint Resolve sum_is_ext.

Lemma func_is_ext : forall x X F,
ext_fun x F ->
ext_fun x (fun x => func X (F x)).
Hint Resolve func_is_ext.

Lemma cst_cont : forall X o y, lt y o -> X == sup o (fun _ => X).

Lemma sum_cont : forall o F G,
ext_fun o F ->
ext_fun o G ->
sum (sup o F) (sup o G) == sup o (fun y => sum (F y) (G y)).

Require Import ZFord_equiv ZFcard.
Section ProductContinuity.

Hypothesis mu : set.
Hypothesis mu_strong : stronglyInaccessibleCard mu.

Let mu_ord : isOrd mu.
Qed.

Let mu_regular : forall x F,
lt_card x mu ->
ext_fun x F ->
(forall y, y \in x -> lt (F y) mu) -> lt (sup x F) mu.
Qed.

Lemma func_cont : forall X F,
lt_card X mu ->
increasing F ->
func X (sup mu F) == sup mu (fun x => func X (F x)).

End ProductContinuity.

Definition UNIT := succ zero.
Lemma unit_typ : zero \in UNIT.

Lemma unit_elim : forall p, p \in UNIT -> p == zero.

Definition BOOL := succ (succ zero).
Definition TRUE := zero.
Definition FALSE := succ zero.

Lemma true_typ : TRUE \in BOOL.

Lemma false_typ : FALSE \in BOOL.

Lemma bool_elim : forall b, b \in BOOL -> b == TRUE \/ b == FALSE.

Section NatOrd_theory.

Definition NATf X := sum UNIT X.

Lemma sum_ext_natf : forall A, ext_fun A NATf.

Instance NATf_mono : Proper (incl_set ==> incl_set) NATf.
Qed.
Hint Resolve NATf_mono Fmono_morph.
Instance NATf_morph : Proper (eq_set ==> eq_set) NATf.
Qed.

Definition ZERO := inl zero.
Definition SUCC x := inr x.

Lemma NATf_discr : forall n, ~ ZERO == SUCC n.

Lemma SUCC_inj : forall n m, SUCC n == SUCC m -> n == m.

Lemma ZERO_typ_gen : forall X, ZERO \in sum UNIT X.

Lemma SUCC_typ_gen : forall x X, x \in X -> SUCC x \in sum UNIT X.

Lemma NATf_case : forall X (P:Prop) x,
(x == ZERO -> P) ->
(forall n, n \in X -> x == SUCC n -> P) ->
x \in NATf X -> P.

Section IterationNat.

Definition NATi := TI NATf.

Instance NATi_morph : morph1 NATi.
Qed.

Lemma NATfun_ext : forall x, ext_fun x (fun n => NATf (NATi n)).
Hint Resolve NATfun_ext.

Lemma NATi_case : forall (P:set->Prop) o n,
isOrd o ->
(forall x x', x \in NATi o -> x == x' -> P x -> P x') ->
P ZERO ->
(forall m o', lt o' o -> m \in NATi o' -> P (SUCC m)) ->
n \in NATi o -> P n.

Definition NATCASE_rel (fZ:set) (fS:set->set) (n:set) :=
fun y =>
(n == ZERO -> y == fZ) /\
(forall k, n == SUCC k -> y == fS k).

Lemma NATCASE_choice_pred :
forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
uchoice_pred (NATCASE_rel fZ fS n).

Definition NATCASE (fZ:set) (fS:set->set) (n:set) :=
uchoice (NATCASE_rel fZ fS n).

Instance NATCASE_morph : Proper
(eq_set ==> (eq_set ==> eq_set) ==> eq_set ==> eq_set) NATCASE.

Qed.

Lemma NATCASE_def : forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
NATCASE_rel fZ fS n (NATCASE fZ fS n).

Lemma NATCASE_ZERO : forall fZ fS,
morph1 fS ->
NATCASE fZ fS ZERO == fZ.

Lemma NATCASE_SUCC : forall o fZ fS n,
morph1 fS ->
isOrd o ->
n \in NATi o ->
NATCASE fZ fS (SUCC n) == fS n.

Lemma NATCASE_typ :
forall (P:set->set) o fZ fS,
morph1 P ->
morph1 fS ->
isOrd o ->
fZ \in P ZERO ->
(forall n, n \in NATi o -> fS n \in P (SUCC n)) ->
forall n,
n \in NATi (osucc o) ->
NATCASE fZ fS n \in P n.

Lemma NATi_fix :
forall (P:set->Prop) o,
isOrd o ->
(forall i, isOrd i -> i \incl o ->
(forall i' m, lt i' i -> m \in NATi i' -> P m) ->
forall n, n \in NATi i -> P n) ->
forall n, n \in NATi o -> P n.

End IterationNat.

Hint Resolve NATfun_ext.

Section NatFixpoint.

Definition NAT := NATi omega.

Lemma NAT_continuous : forall F,
ext_fun omega F ->
NATf (sup omega F) == sup omega (fun n => NATf (F n)).

Lemma NAT_eq : NAT == NATf NAT.

Lemma NATi_NAT : forall o,
isOrd o ->
NATi o \incl NAT.

Lemma ZERO_typ : ZERO \in NAT.

Lemma SUCC_typ : forall n, n \in NAT -> SUCC n \in NAT.

Lemma NAT_fix :
forall (P:set->Prop),
(forall o, isOrd o ->
(forall o' m, lt o' o -> m \in NATi o' -> P m) ->
forall n, n \in NATi o -> P n) ->
forall n, n \in NAT -> P n.

Lemma NAT_ind : forall (P:set->Prop),
(forall x x', x \in NAT -> x == x' -> P x -> P x') ->
P ZERO ->
(forall n, n \in NAT -> P n -> P (SUCC n)) ->
forall n, n \in NAT -> P n.

Fixpoint nat2NAT (n:nat) : set :=
match n with
| 0 => ZERO
| S k => SUCC (nat2NAT k)
end.

Lemma nat2NAT_reflect : forall x,
x \in NAT -> exists n, x == nat2NAT n.

End NatFixpoint.

Section NatUniverse.

Variable U : set.
Hypothesis has_cstr : forall X, X \in U -> sum UNIT X \in U.
Hypothesis has_empty : empty \in U.
Hypothesis has_limit : forall F,
ext_fun omega F ->
(forall n, n \in omega -> F n \in U) -> sup omega F \in U.

Lemma has_fin_limit : forall n F,
lt n omega ->
ext_fun n F ->
(forall m, lt m n -> F m \in U) -> sup n F \in U.

Lemma NATi_pre_typ : forall n, lt n omega -> NATi n \in U.

Lemma NAT_typ : NAT \in U.

End NatUniverse.

Definition ORDf X := sum UNIT (func NAT X).

Lemma sum_ext_ordf : forall A, ext_fun A ORDf.

Instance ORDf_mono : Proper (incl_set ==> incl_set) ORDf.
Qed.
Hint Resolve ORDf_mono.
Instance ORDf_morph : Proper (eq_set ==> eq_set) ORDf.
Qed.

Definition LIM f := inr f.

Lemma LIM_typ_gen : forall x X, x \in func NAT X -> LIM x \in sum UNIT (func NAT X).

Lemma ORDf_case : forall X (P:Prop) x,
(x == ZERO -> P) ->
(forall f, f \in func NAT X -> x == LIM f -> P) ->
x \in ORDf X -> P.

Section IterationOrd.

Definition ORDi := TI ORDf.

Instance ORDi_morph : morph1 ORDi.
Qed.

Lemma ORDfun_ext : forall x, ext_fun x (fun n => ORDf (ORDi n)).
Hint Resolve ORDfun_ext.

Lemma ORDi_case : forall (P:set->Prop) o n,
isOrd o ->
(forall x x', x \in ORDi o -> x == x' -> P x -> P x') ->
P ZERO ->
(forall f o', lt o' o -> f \in func NAT (ORDi o') -> P (LIM f)) ->
n \in ORDi o -> P n.

Lemma ORDi_fix :
forall (P:set->Prop) o,
isOrd o ->
(forall i, isOrd i -> i \incl o ->
(forall i' m, lt i' i -> m \in ORDi i' -> P m) ->
forall n, n \in ORDi i -> P n) ->
forall n, n \in ORDi o -> P n.

End IterationOrd.

Hint Resolve ORDfun_ext.

Section OrdFixpoint.

Hypothesis mu : set.
Hypothesis mu_strong : stronglyInaccessibleCard mu.
Hypothesis NAT_in_mu : lt_card NAT mu.

Let mu_ord : isOrd mu.
Qed.

Let mu_lim : forall x, lt x mu -> lt (osucc x) mu.
Qed.

Definition ORD := ORDi mu.

Lemma ORD_eq : ORD == ORDf ORD.

Lemma ORDi_ORD : forall o,
isOrd o ->
ORDi o \incl ORD.

Section OrdUniverse.

Variable U : set.
Hypothesis has_cstr : forall X, X \in U -> sum UNIT (func NAT X) \in U.
Hypothesis has_empty : empty \in U.
Hypothesis mu_clos : forall x F,
le x mu ->
ext_fun x F ->
(forall n, n \in x -> F n \in U) -> sup x F \in U.

Lemma ORDi_pre_typ : forall n, lt n mu -> ORDi n \in U.

Lemma ORD_typ : ORD \in U.

End OrdUniverse.

End OrdFixpoint.

End NatOrd_theory.

Hint Resolve NATf_mono Fmono_morph NATfun_ext.