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 (α ::: β) → β) : (MvQPF.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

Equations

• One or more equations did not get rendered due to their size.

theorem MvQPF.recF_eq {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (a : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f : (MvQPF.P F).last.B a → (MvQPF.P F).W α) : MvQPF.recF g ((MvQPF.P F).wMk a f' f) = g (MvQPF.abs ⟨a, TypeVec.splitFun f' (MvQPF.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 : (MvQPF.P F).W α) : MvQPF.recF g x = g (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.recF g) ((MvQPF.P F).wDest' x)))

inductive MvQPF.WEquiv {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} : (MvQPF.P F).W α → (MvQPF.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 : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f₀ f₁ : (MvQPF.P F).last.B a → (MvQPF.P F).W α), (∀ (x : (MvQPF.P F).last.B a), MvQPF.WEquiv (f₀ x) (f₁ x)) → MvQPF.WEquiv ((MvQPF.P F).wMk a f' f₀) ((MvQPF.P F).wMk a f' f₁)
• abs: ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a₀ : (MvQPF.P F).A) (f'₀ : ((MvQPF.P F).drop.B a₀).Arrow α) (f₀ : (MvQPF.P F).last.B a₀ → (MvQPF.P F).W α) (a₁ : (MvQPF.P F).A) (f'₁ : ((MvQPF.P F).drop.B a₁).Arrow α) (f₁ : (MvQPF.P F).last.B a₁ → (MvQPF.P F).W α), MvQPF.abs ⟨a₀, (MvQPF.P F).appendContents f'₀ f₀⟩ = MvQPF.abs ⟨a₁, (MvQPF.P F).appendContents f'₁ f₁⟩ → MvQPF.WEquiv ((MvQPF.P F).wMk a₀ f'₀ f₀) ((MvQPF.P F).wMk a₁ f'₁ f₁)
• trans: ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (u v w : (MvQPF.P F).W α), MvQPF.WEquiv u v → MvQPF.WEquiv v w → MvQPF.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 : (MvQPF.P F).W α) (y : (MvQPF.P F).W α) : MvQPF.WEquiv x y → MvQPF.recF u x = MvQPF.recF u y

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

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

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

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

maps every element of the W type to a canonical representative

Equations

• MvQPF.wrepr = MvQPF.recF ((MvQPF.P F).wMk' ∘ MvQPF.repr)

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

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

theorem MvQPF.wEquiv_map {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : α.Arrow β) (x : (MvQPF.P F).W α) (y : (MvQPF.P F).W α) : MvQPF.WEquiv x y → MvQPF.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 ((MvQPF.P F).W α)

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

Equations

• MvQPF.wSetoid α = { r := MvQPF.WEquiv, iseqv := ⋯ }

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)

Equations

• MvQPF.Fix F α = Quotient (MvQPF.wSetoid α)

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

Fix F is a functor

Equations

• MvQPF.Fix.map g = Quotient.lift (fun (x : (MvQPF.P F).W α) => ⟦(MvQPF.P F).wMap g x⟧) ⋯

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

Equations

• MvQPF.Fix.mvfunctor = { map := fun {α β : TypeVec.{u} n} => MvQPF.Fix.map }

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

Recursor for Fix F

Equations

• MvQPF.Fix.rec g = Quot.lift (MvQPF.recF g) ⋯

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

Access W-type underlying Fix F

Equations

• MvQPF.fixToW = Quotient.lift MvQPF.wrepr ⋯

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

Constructor for Fix F

Equations

• MvQPF.Fix.mk x = Quot.mk Setoid.r ((MvQPF.P F).wMk' (MvFunctor.map (TypeVec.id ::: MvQPF.fixToW) (MvQPF.repr x)))

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

Destructor for Fix F

Equations

• MvQPF.Fix.dest = MvQPF.Fix.rec (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.mk))

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 (α ::: MvQPF.Fix F α)) : MvQPF.Fix.rec g (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.rec g) x)

theorem MvQPF.Fix.ind_aux {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (a : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f : (MvQPF.P F).last.B a → (MvQPF.P F).W α) : MvQPF.Fix.mk (MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' fun (x : (MvQPF.P F).last.B a) => ⟦f x⟧⟩) = ⟦(MvQPF.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₁ : MvQPF.Fix F α → β) (g₂ : MvQPF.Fix F α → β) (h : ∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (TypeVec.id ::: g₂) x → g₁ (MvQPF.Fix.mk x) = g₂ (MvQPF.Fix.mk x)) (x : MvQPF.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 : MvQPF.Fix F α → β) (hyp : ∀ (x : F (α ::: MvQPF.Fix F α)), h (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: h) x)) : MvQPF.Fix.rec g = h

theorem MvQPF.Fix.mk_dest {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Fix F α) : MvQPF.Fix.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 (α ::: MvQPF.Fix F α)) : (MvQPF.Fix.mk x).dest = x

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

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

Equations

• MvQPF.mvqpfFix = MvQPF.mk (MvQPF.P F).wp (fun {α : TypeVec.{u} n} (α_1 : ↑(MvQPF.P F).wp α) => Quot.mk MvQPF.WEquiv α_1) (fun {α : TypeVec.{u} n} (α_1 : MvQPF.Fix F α) => MvQPF.fixToW α_1) ⋯ ⋯

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

Dependent recursor for fix F

Equations

• MvQPF.Fix.drec g x = let y := MvQPF.Fix.rec (fun (i : F (α ::: Sigma β)) => ⟨MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) i), g i⟩) x; let_fun this := ⋯; cast ⋯ y.snd