Library ZFind_wd

A theory of dependent inductive families (here W-types) as a subset of a W-type

Require Import ZF ZFpairs ZFrelations ZFord ZFstable ZFind_w ZFfixfun.

Section DependentW.

Parameters of W-types

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

Index type

Variable Arg : set.

Constraints on the subterms

Hypothesis f : set -> set -> set.
Hypothesis fm : morph2 f.
Hypothesis ftyp : ∀ x i,
x ∈ A -> i ∈ B x -> f x i ∈ Arg.

Instance introduced by the constructors

Hypothesis g : set -> set -> Prop.
Hypothesis gm : Proper (eq_set ==>eq_set ==>iff) g.

The intended type operator:

Inductive Wd : Arg->Type := C (x:A) (_:∀ i:B x, Wd(f x i)) : Wd(g x). is encoded as [Inductive Wd' (a:Arg) : Type := C' (x:A) (_:g x=a) (_:∀ i:B x, Wd(f x i)).

Definition W_Fd (X:set->set) (a:set) :=
  sigma (subset A (fun x => g x a)) (fun x => cc_prod (B x) (fun i => X (f x i))).

Instance W_Fd_morph :
  Proper ((eq_set ==> eq_set ) ==> eq_set ==> eq_set) W_Fd.

Qed.

Lemma W_Fd_mono : mono_fam Arg W_Fd.
Hint Resolve W_Fd_mono.

Lemma W_Fd_incl_W_F X Y :
  ext_fun Arg X ->
  (∀ a, a ∈ Arg -> X a ⊆ Y) ->
  ∀ a, a ∈ Arg -> W_Fd X a ⊆ W_F A B Y.

Predicate characterizing the elements of the W-type that respect the index constraints

Inductive instance a w : Prop :=
  | I_node :
      fst w ∈ A ->
      g (fst w) a ->
      (∀ i, i ∈ B (fst w) -> instance (f (fst w) i) (cc_app (snd w) i)) ->
      instance a w.

Instance inst_m : Proper (eq_set ==> eq_set ==> iff) instance.

Qed.

Lemma inst_inv o :
  isOrd o ->
  ∀ a, a ∈ Arg ->
  subset (TI (W_F A B) o) (instance a) == TIF Arg W_Fd o a.

Fixpoint of the W_Fd operator

Definition Wd := TIF Arg W_Fd (W_ord A B).

Lemma Wd_eqn : ∀ a, a ∈ Arg -> Wd a == W_Fd Wd a.

End DependentW.