Library ZFnest

Require Import ZF.
Require Import ZFstable ZFpairs ZFsum ZFrelations ZFcoc ZFord ZFfix ZFlimit.
Require Import ZFiso ZFfixrec.
Require Import ZFind_w ZFspos.
Require Import ZFlist.

Lemma TI_op_mono o o' f f' :
  morph1 f ->
  morph1 f' ->
  (incl_set ==> incl_set)%signature f f' ->
  isOrd o ->
  o == o' ->
  TI f o ⊆ TI f' o'.

Section NestedInductive.

  Variable F : set -> set -> set.
  Hypothesis Fmono : Proper (incl_set==>incl_set==>incl_set) F.

  Instance Fmono_morph2 : morph2 F.
Qed.

  Let Fnest_mono X : Proper (incl_set ==> incl_set) (fun Y => F X Y).
Qed.

  Let Fnest_morph X : morph1 (fun Y => F X Y).
Qed.

Hypothesis A : set.
Hypothesis B : set -> set.
Hypothesis C : set -> set.
Hypothesis Bm : morph1 B.
Hypothesis Cm : morph1 C.
Hypothesis Fdef : ∀ X Y,
  F X Y == sigma A (fun x => prodcart (cc_arr (B x) X) (cc_arr (C x) Y)).

Let ACm : morph1 (W_F A C).
Qed.


Lemma F_elim x X Y :
  x ∈ F X Y ->
  fst x ∈ A /\
  (∀ b, b ∈ B (fst x) -> cc_app (fst (snd x)) b ∈ X) /\
  (∀ i, i ∈ C (fst x) -> cc_app (snd (snd x)) i ∈ Y) /\
  x == (couple (fst x)
       (couple (cc_lam (B (fst x)) (cc_app (fst (snd x))))
               (cc_lam (C (fst x)) (cc_app (snd (snd x)))))).

Lemma F_intro a fb fc X Y :
  ext_fun (B a) fb ->
  ext_fun (C a) fc ->
  a ∈ A ->
  (∀ b, b ∈ B a -> fb b ∈ X) ->
  (∀ i, i ∈ C a -> fc i ∈ Y) ->
  couple a (couple (cc_lam (B a) fb) (cc_lam (C a) fc)) ∈ F X Y.

Let A'i := TI (W_F A C).

Lemma fst_A'i o x' :
  isOrd o -> x' ∈ A'i o -> fst x' ∈ A.

Let B'0 := List (sup A C ∪ sup A B).

Inductive B_ok (x':set) (b:set) : Prop :=
| Bnil l :
   l ∈ B (fst x') ->
   b == Cons l Nil ->
   B_ok x' b
| Bcons i b' :
   i ∈ C (fst x') ->
   B_ok (cc_app (snd x') i) b' ->
   b == Cons i b' ->
   B_ok x' b.

Let B' x' := subset B'0 (B_ok x').

Instance B'm : morph1 B'.
Qed.

Lemma B'notmt x' z : z ∈ B' x' -> ~ z == Nil.

Lemma B'nil o x' l :
  isOrd o ->
  x' ∈ A'i o ->
  l ∈ B (fst x') ->
  Cons l Nil ∈ B' x'.

Lemma B'cons o x' i b' :
  isOrd o ->
  x' ∈ A'i o ->
  i ∈ C (fst x') ->
  b' ∈ B' (cc_app (snd x') i) ->
  Cons i b' ∈ B' x'.

Lemma B'_elim x' z :
  z ∈ B' x' ->
  (exists2 l, l ∈ B (fst x') & z == Cons l Nil) \/
  (exists2 i, i ∈ C (fst x') & exists2 b', b' ∈ B' (cc_app (snd x') i) & z == Cons i b').

Lemma B'_ind : ∀ (P:set->set->Prop),
  (∀ x' b l,
   l ∈ B (fst x') ->
   b == Cons l Nil -> P x' b) ->
  (∀ x' b i b',
   i ∈ C (fst x') ->
   b' ∈ B' (cc_app (snd x') i) ->
   P (cc_app (snd x') i) b' ->
   b == Cons i b' ->
   P x' b) ->
  ∀ x' z,
  z ∈ B' x' ->
  P x' z.

Lemma B'_eqn o x' z :
  isOrd o ->
  x' ∈ A'i o ->
  (z ∈ B' x' <->
   (exists2 l, l ∈ B (fst x') & z == Cons l Nil) \/
   (exists2 i, i ∈ C (fst x') & exists2 b', b' ∈ B' (cc_app (snd x') i) & z == Cons i b')).

Lemma B'cases x b :
  b ∈ B' x ->
  (b == Cons (fst b) Nil /\ fst b ∈ B (fst x) /\
   ∀ f g, LIST_case (snd b) f g == f) \/
  (b == Cons (fst b) (snd b) /\ fst b ∈ C (fst x) /\ snd b ∈ B'(cc_app (snd x) (fst b)) /\
   ∀ f g, LIST_case (snd b) f g == g).

Definition B'case_typ x b f g X :
  b ∈ B' x ->
  (fst b ∈ B(fst x) -> f ∈ X) ->
  (fst b ∈ C(fst x) -> snd b ∈ B'(cc_app(snd x)(fst b)) -> g ∈ X) ->
  LIST_case (snd b) f g ∈ X.
Qed.

Let a'of a fc :=
  couple a (cc_lam (C a) (fun i => fst (fc i))).

Let a'of_typ o a fc X :
  ext_fun (C a) fc ->
  isOrd o ->
  a ∈ A ->
  typ_fun fc (C a) (W_F (A'i o) B' X) ->
  a'of a fc ∈ A'i(osucc o).

Qed.

Definition g f t :=
  let a := fst t in
  let fb := cc_app (fst (snd t)) in
  let fc := cc_app (snd (snd t)) in
  let a' := couple a (cc_lam (C a) (fun i => fst (f (fc i)))) in
  let fb' b :=
    LIST_case (snd b) (fb (fst b))
                      (cc_app (snd (f (fc (fst b)))) (snd b)) in
  couple (a'of a (fun i => f(fc i))) (cc_lam (B' (a'of a (fun i =>f(fc i)))) fb').

Lemma ecase1 : ∀ Y Z a g x f,
  iso_fun Y Z f ->
  typ_fun (cc_app (snd (snd x))) (C a) Y ->
  ext_fun (B' (a'of a g))
     (fun b => LIST_case (snd b) (cc_app (fst (snd x)) (fst b))
        (cc_app (snd (f (cc_app (snd (snd x)) (fst b)))) (snd b))).

Lemma gext f f' X Y :
  eq_fun Y f f' ->
  eq_fun (F X Y) (g f) (g f').

Instance gm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) g.




Qed.

Hint Resolve W_F_mono.

Lemma giso Y X f o:
  isOrd o ->
  iso_fun Y (W_F (A'i o) B' X) f ->
  iso_fun (F X Y) (W_F (W_F A C (A'i o)) B' X) (g f).

Lemma TRF_indep_g : ∀ X o o' x,
  isOrd o ->
  o' ∈ o ->
  x ∈ F X (TI(fun Y=>F X Y) o') ->
  TRF g o x == g (TRF g o') x.

Lemma giso_it X o:
  isOrd o ->
  iso_fun (TI(fun Y=>F X Y)o) (W_F (A'i o) B' X) (TRF g o).

Definition nest_pos (o:set) : positive :=
  mkPositive (fun X => TI (fun Y => F X Y) o) (A'i o) B' (TRF g o).

Lemma isPos_nest o :
  isOrd o ->
  isPositive (nest_pos o).


End NestedInductive.