MvPFunctor.w_cases
theorem MvPFunctor.w_cases :
∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : P.W α → Prop},
(∀ (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α), C (P.wMk a f' f)) → ∀ (x : P.W α), C x
This theorem states that for any natural number `n`, multivariate polynomial functor `P` of arity `n+1`, and `α` which is an `n`-tuple of types, and a predicate `C` on `W`-type of `P` with `α`, if `C` holds for any value constructed by `MvPFunctor.wMk` with inputs `a`, `f'`, and `f` where `a` is in the sort of `P`, `f'` is an arrow in the `TypeVec` category from `(MvPFunctor.drop P).B a` to `α`, and `f` is a function from `(MvPFunctor.last P).B a` to `MvPFunctor.W P α`, then `C` holds for any element in `MvPFunctor.W P α`. This can be seen as a form of structural induction over the `W`-type of a multivariate polynomial functor.
More concisely: If a predicate `C` holds for all values constructed by `MvPFunctor.wMk` from an `n+1`-ary multivariate polynomial functor `P`, inputs in the sort of `P` and functions from the base types of `P` to `α` and `MvPFunctor.W P α`, then `C` holds for all elements in `MvPFunctor.W P α`.
|
MvPFunctor.wRec_eq
theorem MvPFunctor.wRec_eq :
∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : Type u_1}
(g : (a : P.A) → (P.drop.B a).Arrow α → (P.last.B a → P.W α) → (P.last.B a → C) → C) (a : P.A)
(f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α),
P.wRec g (P.wMk a f' f) = g a f' f fun i => P.wRec g (f i)
This theorem, `MvPFunctor.wRec_eq`, establishes the defining equation for the recursor of a W-type in the context of multivariate P-functors. Given a multivariate P-functor `P` indexed by `n+1`, a type vector `α` of length `n`, and a type `C`, it states that for any function `g` that takes an argument `a` of type `P.A`, a function `f'` from `P.drop.B a` to `α`, a function `f` from `P.last.B a` to `P.W α`, and a function from `P.last.B a` to `C`, the recursive application of `g` on the W-type created by `P.wMk a f' f` is equivalent to applying `g` on `a`, `f'`, `f`, and the recursive application of `g` on `f i`. In other words, `wRec` operation is consistent with the function `g` applied on corresponding elements.
More concisely: Given a multivariate P-functor `P`, for any function `g` and elements `a : P.A`, `f' : P.drop.B a -> α`, `f : P.last.B a -> P.W α`, and `h : P.last.B a -> C`, the recursive application of `g` on `P.wMk a f' f` equals applying `g` on `a`, `f'`, `f`, and the recursive application of `g` on `f i`.
|
MvPFunctor.w_ind
theorem MvPFunctor.w_ind :
∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {C : P.W α → Prop},
(∀ (a : P.A) (f' : (P.drop.B a).Arrow α) (f : P.last.B a → P.W α),
(∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)) →
∀ (x : P.W α), C x
This theorem is an induction principle for `W`, a type associated with a multivariate polynomial functor `P`. Given a natural number `n`, a multivariate polynomial functor `P` of arity `n + 1`, a `n`-tuple of types `α`, and a property `C` over `W α`, if for any `a` from functor's object type `A`, any function `f'` from the `drop.B` object of `P` applied to `a` to `α`, and any function `f` from the `last.B` object of `P` applied to `a` to `W α`, if `C` holds for every `f i`, then `C` also holds for `P.wMk a f' f`, then the property `C` holds for all `x` in `W α`. This is essentially an application of structural induction on the structure defined by the multivariate polynomial functor `P`.
More concisely: If for all `a` in the object type of a multivariate polynomial functor `P` of arity `n+1`, and for all functions `f'` from `drop.B` and `f` from `last.B` of `P` applied to `a`, if `C` holds for all `f i`, then `C` holds for `P.wMk a f' f`.
|
MvPFunctor.wDest'_wMk
theorem MvPFunctor.wDest'_wMk :
∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (a : P.A) (f' : (P.drop.B a).Arrow α)
(f : P.last.B a → P.W α), P.wDest' (P.wMk a f' f) = ⟨a, TypeVec.splitFun f' f⟩
The theorem `MvPFunctor.wDest'_wMk` states that for any natural number `n`, any multivariable polynomial functor `P` of arity `n + 1`, any type vector `α` of length `n`, any value `a` in the set of objects of `P`, any arrow `f'` from the type vector obtained by dropping the last type from the B operation of `P` on `a` to `α`, and any function `f` from the last type in the B operation of `P` on `a` to the W-type of `P` on `α`, applying the destructor `MvPFunctor.wDest'` to the W-type constructed by `MvPFunctor.wMk` with `P`, `a`, `f'`, and `f` results in a pair whose first element is `a` and second element is the function obtained by appending `f'` and `f` using `TypeVec.splitFun`. In other words, it validates the consistency of the constructed W-type with its inputs and demonstrates that the destructor essentially reverses the construction operation.
More concisely: For any multivariable polynomial functor `P` of arity `n+1`, the destructor `MvPFunctor.wDest'` applied to the W-type constructed by `MvPFunctor.wMk` from `P`, an object `a` in `P`, the B operation projections `f'` and `f`, returns a pair `(a, g)` where `g` is the composite function of `f'` and `f`.
|