# Documentation

Mathlib.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 ListShape (a b : Type)
| nil : ListShape
| cons : a -> b -> ListShape


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 ListShape 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.

• 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 MvQPF {n : } (F : Type u_1) [] :
Type (max (u + 1) u_1)
• P :
• abs : {α : } → F α
• repr : {α : } → F α
• abs_repr : ∀ {α : } (x : F α), = x
• abs_map : ∀ {α β : } (f : ) (p : ), MvQPF.abs () =

Multivariate quotients of polynomial functors.

Instances

### Show that every MvQPF is a lawful MvFunctor. #

theorem MvQPF.id_map {n : } {F : Type u_1} [] [q : ] {α : } (x : F α) :
MvFunctor.map TypeVec.id x = x
@[simp]
theorem MvQPF.comp_map {n : } {F : Type u_1} [] [q : ] {α : } {β : } {γ : } (f : ) (g : ) (x : F α) :
instance MvQPF.lawfulMvFunctor {n : } {F : Type u_1} [] [q : ] :
theorem MvQPF.liftP_iff {n : } {F : Type u_1} [] [q : ] {α : } (p : i : Fin2 n⦄ → α iProp) (x : F α) :
a f, x = MvQPF.abs { fst := a, snd := f } ((i : Fin2 n) → (j : MvPFunctor.B () a i) → p i (f i j))
theorem MvQPF.liftR_iff {n : } {F : Type u_1} [] [q : ] {α : } (r : {i : Fin2 n} → α iα iProp) (x : F α) (y : F α) :
MvFunctor.LiftR (fun {i} => r i) x y a f₀ f₁, x = MvQPF.abs { fst := a, snd := f₀ } y = MvQPF.abs { fst := a, snd := f₁ } ((i : Fin2 n) → (j : MvPFunctor.B () a i) → r i (f₀ i j) (f₁ i j))
theorem MvQPF.mem_supp {n : } {F : Type u_1} [] [q : ] {α : } (x : F α) (i : Fin2 n) (u : α i) :
u ∀ (a : ().A) (f : TypeVec.Arrow (MvPFunctor.B () a) α), MvQPF.abs { fst := a, snd := f } = xu f i '' Set.univ
theorem MvQPF.supp_eq {n : } {F : Type u_1} [] [q : ] {α : } {i : Fin2 n} (x : F α) :
= {u | ∀ (a : ().A) (f : TypeVec.Arrow (MvPFunctor.B () a) α), MvQPF.abs { fst := a, snd := f } = xu f i '' Set.univ}
theorem MvQPF.has_good_supp_iff {n : } {F : Type u_1} [] [q : ] {α : } (x : F α) :
(∀ (p : (i : Fin2 n) → α iProp), ∀ (i : Fin2 n) (u : α i), u p i u) a f, MvQPF.abs { fst := a, snd := f } = x ∀ (i : Fin2 n) (a' : ().A) (f' : TypeVec.Arrow (MvPFunctor.B () a') α), MvQPF.abs { fst := a', snd := f' } = xf i '' Set.univ f' i '' Set.univ
def MvQPF.IsUniform {n : } {F : Type u_1} [] [q : ] :

A qpf is said to be uniform if every polynomial functor representing a single value all have the same range.

Instances For
def MvQPF.LiftPPreservation {n : } {F : Type u_1} [] [q : ] :

does abs preserve liftp?

Instances For
def MvQPF.SuppPreservation {n : } {F : Type u_1} [] [q : ] :

does abs preserve supp?

Instances For
theorem MvQPF.supp_eq_of_isUniform {n : } {F : Type u_1} [] [q : ] (h : MvQPF.IsUniform) {α : } (a : ().A) (f : TypeVec.Arrow (MvPFunctor.B () a) α) (i : Fin2 n) :
MvFunctor.supp (MvQPF.abs { fst := a, snd := f }) i = f i '' Set.univ
theorem MvQPF.liftP_iff_of_isUniform {n : } {F : Type u_1} [] [q : ] (h : MvQPF.IsUniform) {α : } (x : F α) (p : (i : Fin2 n) → α iProp) :
(i : Fin2 n) → (u : α i) → u p i u
theorem MvQPF.supp_map {n : } {F : Type u_1} [] [q : ] (h : MvQPF.IsUniform) {α : } {β : } (g : ) (x : F α) (i : Fin2 n) :
MvFunctor.supp () i = g i ''
theorem MvQPF.suppPreservation_iff_isUniform {n : } {F : Type u_1} [] [q : ] :
MvQPF.SuppPreservation MvQPF.IsUniform
theorem MvQPF.suppPreservation_iff_liftpPreservation {n : } {F : Type u_1} [] [q : ] :
MvQPF.SuppPreservation MvQPF.LiftPPreservation
theorem MvQPF.liftpPreservation_iff_uniform {n : } {F : Type u_1} [] [q : ] :
MvQPF.LiftPPreservation MvQPF.IsUniform