The initial algebra of a multivariate qpf is again a qpf.

For an (n+1)-ary QPF F (α₀,..,αₙ), we take the least fixed point of F with regards to its last argument αₙ. The result is an n-ary functor: Fix F (α₀,..,αₙ₋₁). Making Fix F into a functor allows us to take the fixed point, compose with other functors and take a fixed point again.

Main definitions

• Fix.mk - constructor
• Fix.dest - destructor
• Fix.rec - recursor: basis for defining functions by structural recursion on Fix F α
• Fix.drec - dependent recursor: generalization of Fix.rec where the result type of the function is allowed to depend on the Fix F α value
• Fix.rec_eq - defining equation for recursor
• Fix.ind - induction principle for Fix F α

Implementation notes

For F a QPF, we define Fix F α in terms of the W-type of the polynomial functor P of F. We define the relation WEquiv and take its quotient as the definition of Fix F α.

See [avigad-carneiro-hudon2019] for more details.

Reference

• Jeremy Avigad, Mario M. Carneiro and Simon Hudon. [Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]

def MvQPF.recF {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) : (P F).W α → β

recF is used as a basis for defining the recursor on Fix F α. recF traverses recursively the W-type generated by q.P using a function on F as a recursive step

theorem MvQPF.recF_eq {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (a : (P F).A) (f' : ((P F).drop.B a).Arrow α) (f : (P F).last.B a → (P F).W α) : recF g ((P F).wMk a f' f) = g (abs ⟨a, TypeVec.splitFun f' (recF g ∘ f)⟩)

theorem MvQPF.recF_eq' {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (x : (P F).W α) : recF g x = g (abs (MvFunctor.map (TypeVec.id ::: recF g) ((P F).wDest' x)))

inductive MvQPF.WEquiv {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : (P F).W α → (P F).W α → Prop

Equivalence relation on W-types that represent the same Fix F value

• ind {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (P F).A) (f' : ((P F).drop.B a).Arrow α) (f₀ f₁ : (P F).last.B a → (P F).W α) : (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) → WEquiv ((P F).wMk a f' f₀) ((P F).wMk a f' f₁)
• abs {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a₀ : (P F).A) (f'₀ : ((P F).drop.B a₀).Arrow α) (f₀ : (P F).last.B a₀ → (P F).W α) (a₁ : (P F).A) (f'₁ : ((P F).drop.B a₁).Arrow α) (f₁ : (P F).last.B a₁ → (P F).W α) : MvQPF.abs ⟨a₀, (P F).appendContents f'₀ f₀⟩ = MvQPF.abs ⟨a₁, (P F).appendContents f'₁ f₁⟩ → WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
• trans {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (u v w : (P F).W α) : WEquiv u v → WEquiv v w → WEquiv u w

theorem MvQPF.recF_eq_of_wEquiv {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] (α : TypeVec.{u} n) {β : Type u} (u : F (α ::: β) → β) (x y : (P F).W α) : WEquiv x y → recF u x = recF u y

theorem MvQPF.wEquiv.abs' {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : (P F).W α) (h : abs ((P F).wDest' x) = abs ((P F).wDest' y)) : WEquiv x y

theorem MvQPF.wEquiv.refl {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (P F).W α) : WEquiv x x

theorem MvQPF.wEquiv.symm {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : (P F).W α) : WEquiv x y → WEquiv y x

def MvQPF.wrepr {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : (P F).W α → (P F).W α

maps every element of the W type to a canonical representative

theorem MvQPF.wrepr_wMk {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (P F).A) (f' : ((P F).drop.B a).Arrow α) (f : (P F).last.B a → (P F).W α) : wrepr ((P F).wMk a f' f) = (P F).wMk' (repr (abs (MvFunctor.map (TypeVec.id ::: wrepr) ⟨a, (P F).appendContents f' f⟩)))

theorem MvQPF.wrepr_equiv {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (P F).W α) : WEquiv (wrepr x) x

theorem MvQPF.wEquiv_map {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α β : TypeVec.{u} n} (g : α.Arrow β) (x y : (P F).W α) : WEquiv x y → WEquiv (MvFunctor.map g x) (MvFunctor.map g y)

def MvQPF.wSetoid {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] (α : TypeVec.{u} n) : Setoid ((P F).W α)

Define the fixed point as the quotient of trees under the equivalence relation.

def MvQPF.Fix {n : ℕ} (F : TypeVec.{u_1} (n + 1) → Type u_1) [q : MvQPF F] (α : TypeVec.{u_1} n) : Type u_1

Least fixed point of functor F. The result is a functor with one fewer parameters than the input. For F a b c a ternary functor, Fix F is a binary functor such that

Fix F a b = F a b (Fix F a b)

def MvQPF.Fix.map {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α β : TypeVec.{u} n} (g : α.Arrow β) : Fix F α → Fix F β

Fix F is a functor

instance MvQPF.Fix.mvfunctor {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] : MvFunctor (Fix F)

def MvQPF.Fix.rec {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) : Fix F α → β

Recursor for Fix F

def MvQPF.fixToW {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : Fix F α → (P F).W α

Access W-type underlying Fix F

def MvQPF.Fix.mk {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: Fix F α)) : Fix F α

Constructor for Fix F

def MvQPF.Fix.dest {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : Fix F α → F (α ::: Fix F α)

Destructor for Fix F

theorem MvQPF.Fix.rec_eq {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (x : F (α ::: Fix F α)) : rec g (mk x) = g (MvFunctor.map (TypeVec.id ::: rec g) x)

theorem MvQPF.Fix.ind_aux {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (P F).A) (f' : ((P F).drop.B a).Arrow α) (f : (P F).last.B a → (P F).W α) : mk (abs ⟨a, (P F).appendContents f' fun (x : (P F).last.B a) => ⟦f x⟧⟩) = ⟦(P F).wMk a f' f⟧

theorem MvQPF.Fix.ind_rec {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g₁ g₂ : Fix F α → β) (h : ∀ (x : F (α ::: Fix F α)), MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (TypeVec.id ::: g₂) x → g₁ (mk x) = g₂ (mk x)) (x : Fix F α) : g₁ x = g₂ x

theorem MvQPF.Fix.rec_unique {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (h : Fix F α → β) (hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g (MvFunctor.map (TypeVec.id ::: h) x)) : rec g = h

theorem MvQPF.Fix.mk_dest {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : Fix F α) : mk x.dest = x

theorem MvQPF.Fix.dest_mk {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: Fix F α)) : (mk x).dest = x

theorem MvQPF.Fix.ind {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (p : Fix F α → Prop) (h : ∀ (x : F (α ::: Fix F α)), MvFunctor.LiftP (α.PredLast p) x → p (mk x)) (x : Fix F α) : p x

instance MvQPF.mvqpfFix {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] : MvQPF (Fix F)

def MvQPF.Fix.drec {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Fix F α → Type u} (g : (x : F (α ::: Sigma β)) → β (mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) x))) (x : Fix F α) : β x

Dependent recursor for fix F