# 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 α.

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

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

• ind: ∀ {n : } {F : TypeVec.{u} (n + 1)Type u} [inst : ] [q : ] {α : } (a : ().A) (f' : (().drop.B a).Arrow α) (f₀ f₁ : ().last.B a().W α), (∀ (x : ().last.B a), MvQPF.WEquiv (f₀ x) (f₁ x))MvQPF.WEquiv (().wMk a f' f₀) (().wMk a f' f₁)
• abs: ∀ {n : } {F : TypeVec.{u} (n + 1)Type u} [inst : ] [q : ] {α : } (a₀ : ().A) (f'₀ : (().drop.B a₀).Arrow α) (f₀ : ().last.B a₀().W α) (a₁ : ().A) (f'₁ : (().drop.B a₁).Arrow α) (f₁ : ().last.B a₁().W α), MvQPF.abs a₀, ().appendContents f'₀ f₀ = MvQPF.abs a₁, ().appendContents f'₁ f₁MvQPF.WEquiv (().wMk a₀ f'₀ f₀) (().wMk a₁ f'₁ f₁)
• trans: ∀ {n : } {F : TypeVec.{u} (n + 1)Type u} [inst : ] [q : ] {α : } (u v w : ().W α),
Instances For
theorem MvQPF.recF_eq_of_wEquiv {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] (α : ) {β : Type u} (u : F (α.append1 β)β) (x : ().W α) (y : ().W α) :
=
theorem MvQPF.wEquiv.abs' {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (x : ().W α) (y : ().W α) (h : MvQPF.abs (().wDest' x) = MvQPF.abs (().wDest' y)) :
theorem MvQPF.wEquiv.refl {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (x : ().W α) :
theorem MvQPF.wEquiv.symm {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (x : ().W α) (y : ().W α) :
def MvQPF.wrepr {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } :
().W α().W α

maps every element of the W type to a canonical representative

Equations
Instances For
theorem MvQPF.wrepr_wMk {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (a : ().A) (f' : (().drop.B a).Arrow α) (f : ().last.B a().W α) :
MvQPF.wrepr (().wMk a f' f) = ().wMk' (MvQPF.repr (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.wrepr) a, ().appendContents f' f)))
theorem MvQPF.wrepr_equiv {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (x : ().W α) :
theorem MvQPF.wEquiv_map {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } {β : } (g : α.Arrow β) (x : ().W α) (y : ().W α) :
MvQPF.WEquiv () ()
def MvQPF.wSetoid {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] (α : ) :
Setoid (().W α)

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

Equations
• = { r := MvQPF.WEquiv, iseqv := }
Instances For
def MvQPF.Fix {n : } (F : TypeVec.{u_1} (n + 1)Type u_1) [] [q : ] (α : ) :
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
Instances For
def MvQPF.Fix.map {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } {β : } (g : α.Arrow β) :

Fix F is a functor

Equations
Instances For
instance MvQPF.Fix.mvfunctor {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] :
Equations
def MvQPF.Fix.rec {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α.append1 β)β) :
β

Recursor for Fix F

Equations
Instances For
def MvQPF.fixToW {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } :
().W α

Access W-type underlying Fix F

Equations
Instances For
def MvQPF.Fix.mk {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (x : F (α.append1 ())) :

Constructor for Fix F

Equations
Instances For
def MvQPF.Fix.dest {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } :
F (α.append1 ())

Destructor for Fix F

Equations
Instances For
theorem MvQPF.Fix.rec_eq {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α.append1 β)β) (x : F (α.append1 ())) :
= g (MvFunctor.map (TypeVec.id ::: ) x)
theorem MvQPF.Fix.ind_aux {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (a : ().A) (f' : (().drop.B a).Arrow α) (f : ().last.B a().W α) :
MvQPF.Fix.mk (MvQPF.abs a, ().appendContents f' fun (x : ().last.B a) => f x) = ().wMk a f' f
theorem MvQPF.Fix.ind_rec {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g₁ : β) (g₂ : β) (h : ∀ (x : F (α.append1 ())), MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (TypeVec.id ::: g₂) xg₁ () = g₂ ()) (x : ) :
g₁ x = g₂ x
theorem MvQPF.Fix.rec_unique {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } {β : Type u} (g : F (α.append1 β)β) (h : β) (hyp : ∀ (x : F (α.append1 ())), h () = g (MvFunctor.map (TypeVec.id ::: h) x)) :
theorem MvQPF.Fix.mk_dest {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (x : ) :
MvQPF.Fix.mk x.dest = x
theorem MvQPF.Fix.dest_mk {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (x : F (α.append1 ())) :
().dest = x
theorem MvQPF.Fix.ind {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] {α : } (p : Prop) (h : ∀ (x : F (α.append1 ())), MvFunctor.LiftP (α.PredLast p) xp ()) (x : ) :
p x
instance MvQPF.mvqpfFix {n : } {F : TypeVec.{u} (n + 1)Type u} [] [q : ] :
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} [] [q : ] {α : } {β : Type u} (g : (x : F (α.append1 ())) → β (MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) x))) (x : ) :
β x

Dependent recursor for fix F

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