Library ZFind_w

Require Import ZF ZFpairs ZFsum ZFnats ZFrelations ZFord ZFfix ZFstable.
Require Import ZFgrothendieck.
Require Import ZFlist.
Import ZFrepl.

In this file we develop the theory of W-types:

typing
existence of a fixpoint
recursor

Section W_theory.

Definition and properties of the W-type operator

Variable A : set.
Variable B : set -> set.
Hypothesis Bext : ext_fun A B.

Definition W_F X := sigma A (fun x => cc_arr (B x) X).

Lemma wfm1 : ∀ X, ext_fun A (fun x => cc_arr (B x) X).
Hint Resolve wfm1.

Lemma W_F_intro X a f :
  ext_fun (B a) f ->
  a ∈ A ->
  (∀ i, i ∈ B a -> f i ∈ X) ->
  couple a (cc_lam (B a) f) ∈ W_F X.

Lemma W_F_elim X x :
  x ∈ W_F X ->
  fst x ∈ A /\
  (∀ i, i ∈ B (fst x) -> cc_app (snd x) i ∈ X ) /\
  x ==couple (fst x) (cc_lam (B (fst x)) (cc_app (snd x))).

Instance W_F_mono : Proper (incl_set ==> incl_set) W_F.
Qed.

Instance W_F_morph : morph1 W_F.
Qed.

Lemma W_F_stable : stable W_F.

Lemma WFi_ext a a' f f' :
  a ∈ A ->
  a == a' ->
  (a == a' -> eq_fun (B a) f f') ->
  couple a (cc_lam (B a) f) == couple a' (cc_lam (B a') f').

Lemma WFi_inv a a' Y Y' f f' :
  couple a (cc_lam Y f) == couple a' (cc_lam Y' f') ->
  ext_fun Y f ->
  ext_fun Y' f' ->
  (a == a' -> Y == Y') ->
  a == a' /\ eq_fun Y f f'.

  Definition WFmap f x :=
    couple (fst x) (cc_lam (B (fst x)) (fun i => f (cc_app (snd x) i))).

  Lemma WFmap_ext : ∀ f f' x x',
    fst x ∈ A ->
    fst x == fst x' ->
    (∀ i i', i ∈ B (fst x) -> i == i' ->
     f (cc_app (snd x) i) == f' (cc_app (snd x') i')) ->
    WFmap f x == WFmap f' x'.

  Lemma WFmap_morph : ∀ X f f',
    eq_fun X f f' ->
    eq_fun (W_F X) (WFmap f) (WFmap f').

Lemma WFmap_comp : ∀ f g X Y x,
  ext_fun X g ->
  ext_fun Y f ->
  (∀ x, x ∈ X -> g x ∈ Y) ->
  x ∈ W_F X ->
  WFmap f (WFmap g x) == WFmap (fun x => f (g x)) x.

Lemma WF_eta : ∀ X x,
  x ∈ W_F X ->
  x == WFmap (fun x => x) x.

  Lemma WFmap_inj : ∀ X Y g g' x x',
    x ∈ W_F X -> x' ∈ W_F Y ->
    ext_fun X g -> ext_fun Y g' ->
    (∀ a a', a ∈ X -> a' ∈ Y -> g a == g' a' -> a == a') ->
    WFmap g x == WFmap g' x' -> x == x'.

  Lemma WFmap_typ : ∀ X Y f x,
    ext_fun X f ->
    x ∈ W_F X ->
    (∀ a, a ∈ X -> f a ∈ Y) ->
    WFmap f x ∈ W_F Y.

Require Import ZFiso.

Lemma WFmap_iso X Y f :
  iso_fun X Y f ->
  iso_fun (W_F X) (W_F Y) (WFmap f).

Encoding W-types as sets of path in a tree

We show that up to isomorphism, W_F is equivalent to another operator Wf, which has a bound. This bound is the set of trees represented as a partial function from paths (indexed by the union of all B(x)) to labels (of type A).

The construction domain and the constructor

Definition Wdom := rel (List (sup A B)) A.

Definition Wsup x :=
   singl (couple Nil (fst x)) ∪
   sup (B (fst x)) (fun y =>
      replf (cc_app (snd x) y)
        (fun p => couple (Cons y (fst p)) (snd p))).

Lemma Wsup_morph : ∀ X, ext_fun (W_F X) Wsup.

Lemma wext1 : ∀ i y,
  ext_fun y (fun p => couple (Cons i (fst p)) (snd p)).

Lemma wext2 : ∀ X g,
  ext_fun X (fun y =>
     replf (cc_app g y) (fun p => couple (Cons y (fst p)) (snd p))).
Hint Resolve wext1 wext2.

Lemma Wsup_def :
  ∀ x p,
  (p ∈ Wsup x <->
   p == couple Nil (fst x) \/
   exists2 i, i ∈ B (fst x) &
   exists2 q, q ∈ cc_app (snd x) i &
   p == couple (Cons i (fst q)) (snd q)).

Lemma Wsup_hd_prop : ∀ a x,
  (couple Nil a ∈ Wsup x <-> a == fst x).

Lemma Wsup_tl_prop : ∀ X i l a x,
  x ∈ W_F X ->
  X ⊆ Wdom ->
  (couple (Cons i l) a ∈ Wsup x <->
   i ∈ B (fst x) /\ couple l a ∈ cc_app (snd x) i).

Lemma Wsup_inj : ∀ X Y x x',
  X ⊆ Wdom ->
  Y ⊆ Wdom ->
  x ∈ W_F X ->
  x' ∈ W_F Y ->
  Wsup x == Wsup x' -> x == x'.

Lemma Wsup_typ_gen : ∀ X x,
  X ⊆ Wdom ->
  x ∈ W_F X ->
  Wsup x ∈ Wdom.

The type operator on the construction domain

Definition Wf X := replf (W_F X) Wsup.

Hint Resolve Wsup_morph.

Lemma Wf_intro : ∀ x X,
  x ∈ W_F X ->
  Wsup x ∈ Wf X.

Lemma Wf_elim : ∀ a X,
  a ∈ Wf X ->
  exists2 x, x ∈ W_F X &
  a == Wsup x.

Instance Wf_mono : Proper (incl_set ==> incl_set) Wf.
Qed.

Instance Wf_morph : morph1 Wf.
Qed.
Hint Resolve Wf_mono Wf_morph.

Lemma Wf_typ : ∀ X,
  X ⊆ Wdom -> Wf X ⊆ Wdom.
Hint Resolve Wf_typ.

Lemma Wf_stable : ∀ X,
  X ⊆ power Wdom ->
  inter (replf X Wf) ⊆ Wf (inter X).

Lemma W_F_Wf_iso X :
  X ⊆ Wdom ->
  iso_fun (W_F X) (Wf X) Wsup.

The fixpoint of Wf (we have shown that Wf is monotone, bounded and stable)

Definition W' := Ffix Wf Wdom.

Lemma W'typ : W' ⊆ Wdom.

Lemma Wi_W' : ∀ o, isOrd o -> TI Wf o ⊆ W'.

Lemma TI_Wf_elim : ∀ a o,
  isOrd o ->
  a ∈ TI Wf o ->
  exists2 o', lt o' o &
  exists2 x, x ∈ W_F (TI Wf o') &
  a == Wsup x.

Lemma Wsup_typ : ∀ o x,
  isOrd o ->
  x ∈ W_F (TI Wf o) ->
  Wsup x ∈ TI Wf (osucc o).

Lemma W'_ind : ∀ (P:set->Prop),
  Proper (eq_set ==> iff) P ->
  (∀ o' x, isOrd o' -> x ∈ W_F (TI Wf o') ->
   (∀ i, i ∈ B (fst x) -> P (cc_app (snd x) i)) ->
   P (Wsup x)) ->
  ∀ a, a ∈ W' -> P a.

The closure ordinal of Wf (and W_F)

  Definition W_ord := Ffix_ord Wf Wdom.

  Lemma W_o_o : isOrd W_ord.
Hint Resolve W_o_o.

  Lemma W'_post : ∀ a,
   a ∈ W' ->
   a ∈ TI Wf W_ord.

  Lemma W'_clos : W' == TI Wf W_ord.

  Lemma W'_eqn : W' == Wf W'.

The fixpoint of the W_type operator

We get W the fixpoint of W_F by isomorphism

  Definition W := TI W_F W_ord.

Let g f := comp_iso (WFmap f) Wsup.

Lemma W_F_Wf_iso' o f :
  isOrd o ->
  iso_fun (TI W_F o) (TI Wf o) f ->
  iso_fun (W_F (TI W_F o)) (Wf (TI Wf o)) (g f).

Let g_ext : ∀ X f f',
  eq_fun X f f' -> eq_fun (W_F X) (g f) (g f').

Qed.

Lemma TI_W_F_Wf_iso o :
  isOrd o ->
  iso_fun (TI W_F o) (TI Wf o) (TI_iso W_F g o).

  Lemma W_eqn : W == W_F W.

Recursor on W

Require Import ZFfunext ZFfixrec.

Section Recursor.

  Hint Resolve W_F_mono.

  Lemma Wi_fix :
    ∀ (P:set->Prop) o,
    isOrd o ->
    (∀ i, isOrd i -> i ⊆ o ->
     (∀ i' m, lt i' i -> m ∈ TI W_F i' -> P m) ->
     ∀ n, n ∈ TI W_F i -> P n) ->
    ∀ n, n ∈ TI W_F o -> P n.

  Variable ord : set.
  Hypothesis oord : isOrd ord.

  Variable F : set -> set -> set.
  Hypothesis Fm : morph2 F.

  Variable U : set -> set -> set.
  Hypothesis Umono : ∀ o o' x x',
    isOrd o' -> o' ⊆ ord -> isOrd o -> o ⊆ o' ->
    x ∈ TI W_F o -> x == x' ->
    U o x ⊆ U o' x'.

  Let Ty o := cc_prod (TI W_F o) (U o).
  Hypothesis Ftyp : ∀ o f, isOrd o -> o ⊆ ord ->
    f ∈ Ty o -> F o f ∈ Ty (osucc o).

  Let Q o f := ∀ x, x ∈ TI W_F o -> cc_app f x ∈ U o x.

  Definition Wi_ord_irrel :=
    ∀ o o' f g,
    isOrd o' -> o' ⊆ ord -> isOrd o -> o ⊆ o' ->
    f ∈ Ty o -> g ∈ Ty o' ->
    fcompat (TI W_F o) f g ->
    fcompat (TI W_F (osucc o)) (F o f) (F o' g).

  Hypothesis Firrel : Wi_ord_irrel.

  Definition WREC := REC F.

Lemma Umorph : ∀ o o', isOrd o' -> o' ⊆ ord -> o == o' ->
    ∀ x x', x ∈ TI W_F o -> x == x' -> U o x == U o' x'.

Lemma Uext : ∀ o, isOrd o -> o ⊆ ord -> ext_fun (TI W_F o) (U o).

  Lemma WREC_typing : ∀ o f, isOrd o -> o ⊆ ord ->
    is_cc_fun (TI W_F o) f -> Q o f -> f ∈ Ty o.

Let Wi_cont : ∀ o,
   isOrd o -> TI W_F o == sup o (fun o' => TI W_F (osucc o')).
Qed.

Let Qm :
   ∀ o o',
   isOrd o ->
   o ⊆ ord ->
   o == o' -> ∀ f f', fcompat (TI W_F o) f f' -> Q o f -> Q o' f'.
Qed.

Let Qcont : ∀ o f : set,
isOrd o ->
o ⊆ ord ->
is_cc_fun (TI W_F o) f ->
(∀ o' : set, o' ∈ o -> Q (osucc o') f) -> Q o f.
Qed.

Let Qtyp : ∀ o f,
isOrd o ->
o ⊆ ord ->
is_cc_fun (TI W_F o) f ->
Q o f -> is_cc_fun (TI W_F (osucc o)) (F o f) /\ Q (osucc o) (F o f).

Qed.

  Lemma Firrel_W : stage_irrelevance ord (TI W_F) Q F.

  Lemma WREC_recursor : recursor ord (TI W_F) Q F.
Hint Resolve WREC_recursor.

  Lemma WREC_wt : WREC ord ∈ Ty ord.

  Lemma WREC_ind : ∀ P x,
    Proper (eq_set ==>eq_set ==>eq_set ==>iff) P ->
    (∀ o x, isOrd o -> lt o ord ->
     x ∈ W_F (TI W_F o) ->
     (∀ y, y ∈ TI W_F o -> P o y (cc_app (WREC ord) y)) ->
     ∀ w, isOrd w -> w ⊆ ord -> lt o w ->
     P w x (cc_app (F ord (WREC ord)) x)) ->
    x ∈ TI W_F ord ->
    P ord x (cc_app (WREC ord) x).

  Lemma WREC_expand : ∀ n,
    n ∈ TI W_F ord -> cc_app (WREC ord) n == cc_app (F ord (WREC ord)) n.

  Lemma WREC_irrel o o' :
    isOrd o ->
    isOrd o' ->
    o ⊆ o' ->
    o' ⊆ ord ->
    eq_fun (TI W_F o) (cc_app (WREC o)) (cc_app (WREC o')).

End Recursor.

Universe facts: when A and B belong to a given (infinite) universe, then so does W(A,B).

Section W_Univ.

  Variable U : set.
  Hypothesis Ugrot : grot_univ U.
  Hypothesis Unontriv : omega ∈ U.

  Hypothesis aU : A ∈ U.
  Hypothesis bU : ∀ a, a ∈ A -> B a ∈ U.

  Lemma G_Wdom : Wdom ∈ U.

  Lemma G_W' : W' ∈ U.

  Lemma G_W_F X : X ∈ U -> W_F X ∈ U.

  Lemma G_W_ord : W_ord ∈ U.

  Lemma G_W : W ∈ U.

End W_Univ.

End W_theory.

Lemma W_F_ext : ∀ A A' B B' X X',
  A == A' ->
  eq_fun A B B' ->
  X == X' ->
  W_F A B X == W_F A' B' X'.

Hint Resolve wfm1.

A specific instance of W-type: the type of sets (cf Ens.set)

Section Sets.

Hypothesis U : set.
Hypothesis Ugrot : grot_univ U.

  Definition sets := W U (fun X =>X).

  Let sm : ext_fun U (fun X => X).
Qed.

  Lemma sets_ind :
    ∀ P : set -> Prop,
    (∀ y X f, morph1 f ->

     y == couple X (cc_lam X f) ->
     X ∈ U ->
     (∀ x, x ∈ X -> f x ∈ sets) ->

     (∀ x, x ∈ X -> P (f x)) ->
     P y) ->
    ∀ x, x ∈ sets -> P x.

  Lemma sets_incl_U : sets ⊆ U.

End Sets.