Library Nest

Showing a nested inductive type operator is isomorphic to a W-type.

Set Implicit Arguments.

Parameter A: Type.
Parameter B: A->Type.
Parameter C: A->Type.

Binary type operator: X is the parameter of the nested type (and the outer inductive type); Y is the nested inductive type. It is assumed to be equivalent to a mixed W-type: F(X,Y) = \Sigma x:A. (B x -> X) * (C x -> Y)

Record F X Y := mkF { fa : A ; fb : B fa -> X ; fc : C fa -> Y }.
Implicit Arguments mkF [X Y].

The nested inductive type

Inductive N (X:Type) :=
CN : F X (N X) -> N X.

The container of the inductive type

Inductive I :=
CI : N I -> I.

The label of the container: a tree following the structure of N, labelled with A.

Inductive A' :=
CA' : ∀ x:A, (C x -> A') -> A'.
Implicit Arguments CA' [ ].
Definition fst' (x':A') : A := let (a,_) := x' in a.
Definition snd' (x':A') : C (fst' x') -> A' :=
match x' with CA' _ f => f end.

The arity of the container: it is an inductive family with a non-uniform parameter. It is the set of paths of the tree (of type A'), every node has subterms indexed following B.

Inductive B' (x':A') :=
| B'nil : B (fst' x') -> B' x'
| B'cons (i:C (fst' x')) (b':B'(snd' x' i)) : B' x'.

Parameter X:Type.

The equivalent W-type

Record W_F X := mkWF { fA' : A' ; fB' : B' fA' -> X }.
Implicit Arguments mkWF [X].

Definition iso_step (Y:Type) (f:Y-> W_F X) (n:F X Y) : W_F X :=
  let x' := CA' (fa n) (fun i => fA' (f (fc n i))) in
  let f' (b:B' x') :=
   match b return X with
   | B'nil l => fb n l
   | B'cons i b' => fB' (f (fc n i)) b'
   end in
  mkWF x' f'.

Iso: N --> W-type

Fixpoint iso (n:N X) : W_F X :=
let (nF) := n in iso_step iso nF.

For the reverse iso, it is necessary to split the W-type in a couple of a A' and a function B'->X

Definition iso'_step Y (f:∀ a',(B' a'->X)->Y) (a':A') (fb':B' a' -> X) : F X Y :=
  let x := fst' a' in
  let fb (b:B x) : X := fb' (B'nil _ b) in
  let fc (i:C x) : Y :=
    f (snd' a' i) (fun b'':B'(snd' a' i)=> fb' (B'cons _ i b'')) in
  mkF x fb fc.
Implicit Arguments iso'_step [Y].

Fixpoint iso' (a':A') (fb':B' a' -> X) : N X :=
  CN (iso'_step iso' a' fb').
Implicit Arguments iso' [ ].

Definition iso'' (w:W_F X) : N X := iso' (fA' w) (fB' w).