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

class MvQPF {n : ℕ} (F : TypeVec.{u} n → Type u_1) extends MvFunctor F : Type (max (u + 1) u_1)

Multivariate quotients of polynomial functors.

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

Show that every MvQPF is a lawful MvFunctor.

theorem MvQPF.id_map {n : ℕ} {F : TypeVec.{u} n → Type u_1} [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} [q : MvQPF F] {α β γ : TypeVec.{u} n} (f : α.Arrow β) (g : β.Arrow γ) (x : F α) : MvFunctor.map (TypeVec.comp g f) x = MvFunctor.map g (MvFunctor.map f x)

@[instance 100]

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

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

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

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

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

theorem MvQPF.has_good_supp_iff {n : ℕ} {F : TypeVec.{u} n → Type u_1} [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 : (P F).A) (f : ((P F).B a).Arrow α), abs ⟨a, f⟩ = x ∧ ∀ (i : Fin2 n) (a' : (P F).A) (f' : ((P F).B a').Arrow α), abs ⟨a', f'⟩ = x → f i '' Set.univ ⊆ f' i '' Set.univ

def MvQPF.IsUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [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} [q : MvQPF F] : Prop

does abs preserve liftp?

Equations

• MvQPF.LiftPPreservation = ∀ ⦃α : TypeVec.{?u.6} 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} [q : MvQPF F] : Prop

does abs preserve supp?

Equations

• MvQPF.SuppPreservation = ∀ ⦃α : TypeVec.{?u.19} 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} [q : MvQPF F] (h : IsUniform) {α : TypeVec.{u} n} (a : (P F).A) (f : ((P F).B a).Arrow α) (i : Fin2 n) : MvFunctor.supp (abs ⟨a, f⟩) i = f i '' Set.univ

theorem MvQPF.liftP_iff_of_isUniform {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] (h : 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} [q : MvQPF F] (h : IsUniform) {α β : TypeVec.{u} n} (g : α.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} [q : MvQPF F] : SuppPreservation ↔ IsUniform

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

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

def MvQPF.ofEquiv {n : ℕ} {F : TypeVec.{u} n → Type u_2} {F' : TypeVec.{u} n → Type u_3} [q : MvQPF F'] [MvFunctor F] (eqv : (α : TypeVec.{u} n) → F α ≃ F' α) (map_eq : ∀ (α β : TypeVec.{u} n) (f : α.Arrow β) (a : F α), MvFunctor.map f a = (eqv β).symm (MvFunctor.map f ((eqv α) a)) := by intros; rfl) : 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

• P.instMvQPFObj = { toMvFunctor := P.instMvFunctorObj, P := P, abs := fun {α : TypeVec.{?u.12} n} => id, repr := fun {α : TypeVec.{?u.12} n} => id, abs_repr := ⋯, abs_map := ⋯ }