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.

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

Multivariate quotients of polynomial functors.

• P : MvPFunctor.{u} n
• abs : {α : TypeVec.{u} n} → ↑(MvQPF.P F) α → F α
• repr : {α : TypeVec.{u} n} → F α → ↑(MvQPF.P F) α
• abs_repr : ∀ {α : TypeVec.{u} n} (x : F α), MvQPF.abs (MvQPF.repr x) = x
• abs_map : ∀ {α β : TypeVec.{u} n} (f : TypeVec.Arrow α β) (p : ↑(MvQPF.P F) α), MvQPF.abs (MvFunctor.map f p) = MvFunctor.map f (MvQPF.abs p)

Show that every MvQPF is a lawful MvFunctor.

theorem MvQPF.id_map {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) : MvFunctor.map TypeVec.id x = x

@[simp]

theorem MvQPF.comp_map {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {β : TypeVec.{u} n} {γ : TypeVec.{u} n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow β γ) (x : F α) : MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)

instance MvQPF.lawfulMvFunctor {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] : LawfulMvFunctor F

Equations

• ⋯ = ⋯

theorem MvQPF.liftP_iff {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : F α) : MvFunctor.LiftP p x ↔ ∃ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), x = MvQPF.abs { fst := a, snd := f } ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), p (f i j)

theorem MvQPF.liftR_iff {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (r : {i : Fin2 n} → α i → α i → Prop) (x : F α) (y : F α) : MvFunctor.LiftR (fun {i : Fin2 n} => r) x y ↔ ∃ (a : (MvQPF.P F).A) (f₀ : TypeVec.Arrow ((MvQPF.P F).B a) α) (f₁ : TypeVec.Arrow ((MvQPF.P F).B a) α), x = MvQPF.abs { fst := a, snd := f₀ } ∧ y = MvQPF.abs { fst := a, snd := f₁ } ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), r (f₀ i j) (f₁ i j)

theorem MvQPF.mem_supp {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) (i : Fin2 n) (u : α i) : u ∈ MvFunctor.supp x i ↔ ∀ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), MvQPF.abs { fst := a, snd := f } = x → u ∈ f i '' Set.univ

theorem MvQPF.supp_eq {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {i : Fin2 n} (x : F α) : MvFunctor.supp x i = {u : α i | ∀ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), MvQPF.abs { fst := a, snd := f } = x → u ∈ f i '' Set.univ}

theorem MvQPF.has_good_supp_iff {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} (x : F α) : (∀ (p : (i : Fin2 n) → α i → Prop), MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u) ↔ ∃ (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).B a) α), MvQPF.abs { fst := a, snd := f } = x ∧ ∀ (i : Fin2 n) (a' : (MvQPF.P F).A) (f' : TypeVec.Arrow ((MvQPF.P F).B a') α), MvQPF.abs { fst := a', snd := f' } = x → f i '' Set.univ ⊆ f' i '' Set.univ

def MvQPF.IsUniform {n : ℕ} {F : TypeVec.{u} n → 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

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

def MvQPF.LiftPPreservation {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] : Prop

does abs preserve liftp?

Equations

• MvQPF.LiftPPreservation = ∀ ⦃α : TypeVec.{u} n⦄ (p : ⦃i : Fin2 n⦄ → α i → Prop) (x : ↑(MvQPF.P F) α), MvFunctor.LiftP p (MvQPF.abs x) ↔ MvFunctor.LiftP p x

def MvQPF.SuppPreservation {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] : Prop

does abs preserve supp?

Equations

• MvQPF.SuppPreservation = ∀ ⦃α : TypeVec.{u} n⦄ (x : ↑(MvQPF.P F) α), MvFunctor.supp (MvQPF.abs x) = MvFunctor.supp x

theorem MvQPF.supp_eq_of_isUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} (a : (MvQPF.P F).A) (f : TypeVec.Arrow ((MvQPF.P F).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 : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} (x : F α) (p : (i : Fin2 n) → α i → Prop) : MvFunctor.LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ MvFunctor.supp x i, p i u

theorem MvQPF.supp_map {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] (h : MvQPF.IsUniform) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : TypeVec.Arrow α β) (x : F α) (i : Fin2 n) : MvFunctor.supp (MvFunctor.map g x) i = g i '' MvFunctor.supp x i

theorem MvQPF.suppPreservation_iff_isUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] : MvQPF.SuppPreservation ↔ MvQPF.IsUniform

theorem MvQPF.suppPreservation_iff_liftpPreservation {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] : MvQPF.SuppPreservation ↔ MvQPF.LiftPPreservation

theorem MvQPF.liftpPreservation_iff_uniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [MvFunctor F] [q : MvQPF F] : MvQPF.LiftPPreservation ↔ MvQPF.IsUniform

def MvQPF.ofEquiv {n : ℕ} {F : TypeVec.{u} n → Type u_2} {F' : TypeVec.{u} n → Type u_3} [MvFunctor F'] [q : MvQPF F'] [MvFunctor F] (eqv : (α : TypeVec.{u} n) → F α ≃ F' α) (map_eq : autoParam (∀ (α β : TypeVec.{u} n) (f : TypeVec.Arrow α β) (a : F α), MvFunctor.map f a = (eqv β).symm (MvFunctor.map f ((eqv α) a))) _auto✝) : MvQPF F

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.

instance MvPFunctor.instMvQPFObj {n : ℕ} (P : MvPFunctor.{u_1} n) : MvQPF ↑P

Every polynomial functor is a (trivial) QPF

Equations

• MvPFunctor.instMvQPFObj P = { P := P, abs := fun {α : TypeVec.{u_1} n} => id, repr := fun {α : TypeVec.{u_1} n} => id, abs_repr := ⋯, abs_map := ⋯ }