# mathlibdocumentation

data.qpf.multivariate.basic

# Multivariate quotients of polynomial functors.

Basic definition of multivariate QPF. QPFs form a compositional framework for defining inductive and coinductive types, their quotients and nesting.

The idea is based on building ever larger functors. For instance, we can define a list using a shape functor:

inductive list_shape (a b : Type)
| nil : list_shape
| cons : a -> b -> list_shape


This shape can itself be decomposed as a sum of product which are themselves QPFs. It follows that the shape is a QPF and we can take its fixed point and create the list itself:

def list (a : Type) := fix list_shape a -- not the actual notation


We can continue and define the quotient on permutation of lists and create the multiset type:

def multiset (a : Type) := qpf.quot list.perm list a -- not the actual notion


And multiset is also a QPF. We can then create a novel data type (for Lean):

inductive tree (a : Type)
| node : a -> multiset tree -> tree


An unordered tree. This is currently not supported by Lean because it nests an inductive type inside of a quotient. We can go further and define unordered, possibly infinite trees:

coinductive tree' (a : Type)
| node : a -> multiset tree' -> tree'


by using the cofix construct. Those options can all be mixed and matched because they preserve the properties of QPF. The latter example, tree', combines fixed point, co-fixed point and quotients.

## Related modules

• constructions
• fix
• cofix
• quot
• comp
• sigma / pi
• prj
• const

each proves that some operations on functors preserves the QPF structure

## reference

• [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
@[class]
structure mvqpf {n : } (F : Type u_1) [mvfunctor F] :
Type (max (u+1) u_1)

Multivariate quotients of polynomial functors.

Instances

### Show that every mvqpf is a lawful mvfunctor.

theorem mvqpf.id_map {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F α) :
= x

@[simp]
theorem mvqpf.comp_map {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] {α β γ : typevec n} (f : α β) (g : β γ) (x : F α) :
(g f) <$$> x = g <$$> f <$$> x @[instance] def mvqpf.is_lawful_mvfunctor {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] : theorem mvqpf.liftp_iff {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (p : Π ⦃i : fin2 n⦄, α i → Prop) (x : F α) : ∃ (a : (mvqpf.P F).A) (f : (mvqpf.P F).B a α), x = mvqpf.abs a, f⟩ ∀ (i : fin2 n) (j : (mvqpf.P F).B a i), p (f i j) theorem mvqpf.liftr_iff {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (r : Π ⦃i : fin2 n⦄, α iα i → Prop) (x y : F α) : y ∃ (a : (mvqpf.P F).A) (f₀ f₁ : (mvqpf.P F).B a α), x = mvqpf.abs a, f₀⟩ y = mvqpf.abs a, f₁⟩ ∀ (i : fin2 n) (j : (mvqpf.P F).B a i), r (f₀ i j) (f₁ i j) theorem mvqpf.mem_supp {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F α) (i : fin2 n) (u : α i) : u ∀ (a : (mvqpf.P F).A) (f : (mvqpf.P F).B a α), mvqpf.abs a, f⟩ = xu f i '' set.univ theorem mvqpf.supp_eq {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} {i : fin2 n} (x : F α) : = {u : α i | ∀ (a : (mvqpf.P F).A) (f : (mvqpf.P F).B a α), mvqpf.abs a, f⟩ = xu f i '' set.univ} theorem mvqpf.has_good_supp_iff {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F α) : (∀ (p : Π (i : fin2 n), α i → Prop), ∀ (i : fin2 n) (u : α i), u p i u) ∃ (a : (mvqpf.P F).A) (f : (mvqpf.P F).B a α), mvqpf.abs a, f⟩ = x ∀ (i : fin2 n) (a' : (mvqpf.P F).A) (f' : (mvqpf.P F).B a' α), mvqpf.abs a', f'⟩ = xf i '' set.univ f' i '' set.univ def mvqpf.is_uniform {n : } {F : Type u_1} [mvfunctor F] (q : mvqpf F) : Prop A qpf is said to be uniform if every polynomial functor representing a single value all have the same range. Equations def mvqpf.liftp_preservation {n : } {F : Type u_1} [mvfunctor F] (q : mvqpf F) : Prop does abs preserve liftp? Equations def mvqpf.supp_preservation {n : } {F : Type u_1} [mvfunctor F] (q : mvqpf F) : Prop does abs preserve supp? Equations theorem mvqpf.supp_eq_of_is_uniform {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] (h : q.is_uniform) {α : typevec n} (a : (mvqpf.P F).A) (f : (mvqpf.P F).B a α) (i : fin2 n) : theorem mvqpf.liftp_iff_of_is_uniform {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] (h : q.is_uniform) {α : typevec n} (x : F α) (p : Π (i : fin2 n), α i → Prop) : ∀ (i : fin2 n) (u : α i), u p i u theorem mvqpf.supp_map {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] (h : q.is_uniform) {α β : typevec n} (g : α β) (x : F α) (i : fin2 n) : mvfunctor.supp (g <$$> x) i = g i ''

theorem mvqpf.supp_preservation_iff_uniform {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] :

theorem mvqpf.supp_preservation_iff_liftp_preservation {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] :

theorem mvqpf.liftp_preservation_iff_uniform {n : } {F : Type u_1} [mvfunctor F] [q : mvqpf F] :