# 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) extends :
Type (max (u + 1) u_1)

Multivariate quotients of polynomial functors.

• map : {α β : } → α.Arrow βF αF β
• P :
• abs : {α : } → () αF α
• repr : {α : } → F α() α
• abs_repr : ∀ {α : } (x : F α), = x
• abs_map : ∀ {α β : } (f : α.Arrow β) (p : () α), MvQPF.abs () =
Instances
theorem MvQPF.abs_repr {n : } {F : Type u_1} [self : ] {α : } (x : F α) :
= x
theorem MvQPF.abs_map {n : } {F : Type u_1} [self : ] {α : } {β : } (f : α.Arrow β) (p : () α) :

### 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 : α.Arrow β) (g : β.Arrow γ) (x : F α) :
@[instance 100]
instance MvQPF.lawfulMvFunctor {n : } {F : Type u_1} [q : ] :
Equations
• =
theorem MvQPF.liftP_iff {n : } {F : Type u_1} [q : ] {α : } (p : i : Fin2 n⦄ → α iProp) (x : F α) :
∃ (a : ().A) (f : (().B a).Arrow α), x = MvQPF.abs a, f ∀ (i : Fin2 n) (j : ().B a i), p (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 : Fin2 n} => r) x y ∃ (a : ().A) (f₀ : (().B a).Arrow α) (f₁ : (().B a).Arrow α), x = MvQPF.abs a, f₀ y = MvQPF.abs a, f₁ ∀ (i : Fin2 n) (j : ().B a i), r (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 : (().B a).Arrow α), MvQPF.abs a, f = xu f i '' Set.univ
theorem MvQPF.supp_eq {n : } {F : Type u_1} [q : ] {α : } {i : Fin2 n} (x : F α) :
= {u : α i | ∀ (a : ().A) (f : (().B a).Arrow α), MvQPF.abs a, 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, p i u) ∃ (a : ().A) (f : (().B a).Arrow α), MvQPF.abs a, f = x ∀ (i : Fin2 n) (a' : ().A) (f' : (().B a').Arrow α), MvQPF.abs a', 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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MvQPF.LiftPPreservation {n : } {F : Type u_1} [q : ] :

does abs preserve liftp?

Equations
• MvQPF.LiftPPreservation = ∀ ⦃α : ⦄ (p : i : Fin2 n⦄ → α iProp) (x : () α),
Instances For
def MvQPF.SuppPreservation {n : } {F : Type u_1} [q : ] :

does abs preserve supp?

Equations
• MvQPF.SuppPreservation = ∀ ⦃α : ⦄ (x : () α),
Instances For
theorem MvQPF.supp_eq_of_isUniform {n : } {F : Type u_1} [q : ] (h : MvQPF.IsUniform) {α : } (a : ().A) (f : (().B a).Arrow α) (i : Fin2 n) :
MvFunctor.supp (MvQPF.abs a, 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, p i u
theorem MvQPF.supp_map {n : } {F : Type u_1} [q : ] (h : MvQPF.IsUniform) {α : } {β : } (g : α.Arrow β) (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
def MvQPF.ofEquiv {n : } {F : Type u_2} {F' : Type u_3} [q : MvQPF F'] [] (eqv : (α : ) → F α F' α) (map_eq : autoParam (∀ (α β : ) (f : α.Arrow β) (a : F α), = (eqv β).symm (MvFunctor.map f ((eqv α) a))) _auto✝) :

Any type function F that is (extensionally) equivalent to a QPF, is itself a QPF, assuming that the functorial map of F behaves similar to MvFunctor.ofEquiv eqv

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance MvPFunctor.instMvQPFObj {n : } (P : ) :
MvQPF P

Every polynomial functor is a (trivial) QPF

Equations
• P.instMvQPFObj = MvQPF.mk P (fun {α : } => id) (fun {α : } => id)