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} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) : MvPFunctor.W (MvQPF.P F) α → β

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} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β) (a : (MvQPF.P F).A) (f' : TypeVec.Arrow ((MvPFunctor.drop (MvQPF.P F)).B a) α) (f : (MvPFunctor.last (MvQPF.P F)).B a → MvPFunctor.W (MvQPF.P F) α) : MvQPF.recF g (MvPFunctor.wMk (MvQPF.P F) a f' f) = g (MvQPF.abs { fst := a, snd := TypeVec.splitFun f' (MvQPF.recF g ∘ f) })

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

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

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

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

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

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

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

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

maps every element of the W type to a canonical representative

Equations

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

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

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

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

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

Equations

• MvQPF.wSetoid α = { r := MvQPF.WEquiv, iseqv := (_ : Equivalence MvQPF.WEquiv) }

def MvQPF.Fix {n : ℕ} (F : TypeVec.{u_1} (n + 1) → Type u_1) [MvFunctor F] [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} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow α β) : MvQPF.Fix F α → MvQPF.Fix F β

Fix F is a functor

Equations

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

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

Equations

• MvQPF.Fix.mvfunctor = { map := @MvQPF.Fix.map n F inst q }

def MvQPF.Fix.rec {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [MvFunctor F] [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) (_ : ∀ (x y : MvPFunctor.W (MvQPF.P F) α), MvQPF.WEquiv x y → MvQPF.recF g x = MvQPF.recF g y)

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

Access W-type underlying Fix F

Equations

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

def MvQPF.Fix.mk {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [MvFunctor F] [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 (MvPFunctor.wMk' (MvQPF.P F) (MvFunctor.map (TypeVec.id ::: MvQPF.fixToW) (MvQPF.repr x)))

def MvQPF.Fix.dest {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [MvFunctor F] [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} [MvFunctor F] [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} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (a : (MvQPF.P F).A) (f' : TypeVec.Arrow ((MvPFunctor.drop (MvQPF.P F)).B a) α) (f : (MvPFunctor.last (MvQPF.P F)).B a → MvPFunctor.W (MvQPF.P F) α) : MvQPF.Fix.mk (MvQPF.abs { fst := a, snd := MvPFunctor.appendContents (MvQPF.P F) f' fun (x : (MvPFunctor.last (MvQPF.P F)).B a) => ⟦f x⟧ }) = ⟦MvPFunctor.wMk (MvQPF.P F) a f' f⟧

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

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

theorem MvQPF.Fix.ind {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (p : MvQPF.Fix F α → Prop) (h : ∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.LiftP (TypeVec.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} [MvFunctor F] [q : MvQPF F] : MvQPF (MvQPF.Fix F)

Equations

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

def MvQPF.Fix.drec {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [MvFunctor F] [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

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