Quotients of Polynomial Functors

We assume the following:

P : a polynomial functor W : its W-type M : its M-type F : a functor

We define:

q : Qpf data, representing F as a quotient of P

The main goal is to construct:

Fix : the initial algebra with structure map F Fix → Fix. Cofix : the final coalgebra with structure map Cofix → F Cofix

We also show that the composition of qpfs is a qpf, and that the quotient of a qpf is a qpf.

The present theory focuses on the univariate case for qpfs

References

• [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]

class Qpf (F : Type u → Type u) [Functor F] : Type (u + 1)

• P : PFunctor
• abs : {α : Type u} → PFunctor.Obj (Qpf.P F) α → F α
• repr : {α : Type u} → F α → PFunctor.Obj (Qpf.P F) α
• abs_repr : ∀ {α : Type u} (x : F α), Qpf.abs (Qpf.repr x) = x
• abs_map : ∀ {α β : Type u} (f : α → β) (p : PFunctor.Obj (Qpf.P F) α), Qpf.abs (f <$> p) = f <$> Qpf.abs p

Quotients of polynomial functors.

Roughly speaking, saying that F is a quotient of a polynomial functor means that for each α, elements of F α are represented by pairs ⟨a, f⟩, where a is the shape of the object and f indexes the relevant elements of α, in a suitably natural manner.

theorem Qpf.id_map {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) : id <$> x = x

theorem Qpf.comp_map {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} {β : Type u} {γ : Type u} (f : α → β) (g : β → γ) (x : F α) : (g ∘ f) <$> x = g <$> f <$> x

theorem Qpf.lawfulFunctor {F : Type u → Type u} [Functor F] [q : Qpf F] (h : ∀ (α β : Type u), Functor.mapConst = Functor.map ∘ Function.const β) : LawfulFunctor F

theorem Qpf.liftp_iff {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (p : α → Prop) (x : F α) : Functor.Liftp p x ↔ ∃ a f, x = Qpf.abs { fst := a, snd := f } ∧ ((i : PFunctor.B (Qpf.P F) a) → p (f i))

theorem Qpf.liftp_iff' {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (p : α → Prop) (x : F α) : Functor.Liftp p x ↔ ∃ u, Qpf.abs u = x ∧ ((i : PFunctor.B (Qpf.P F) u.fst) → p (Sigma.snd (Qpf.P F).A (fun x => PFunctor.B (Qpf.P F) x → α) u i))

theorem Qpf.liftr_iff {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (r : α → α → Prop) (x : F α) (y : F α) : Functor.Liftr r x y ↔ ∃ a f₀ f₁, x = Qpf.abs { fst := a, snd := f₀ } ∧ y = Qpf.abs { fst := a, snd := f₁ } ∧ ((i : PFunctor.B (Qpf.P F) a) → r (f₀ i) (f₁ i))

def Qpf.recF {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F α → α) : PFunctor.W (Qpf.P F) → α

does recursion on q.P.W using g : F α → α rather than g : P α → α

Equations

• Qpf.recF g (WType.mk a f) = g (Qpf.abs { fst := a, snd := fun x => Qpf.recF g (f x) })

theorem Qpf.recF_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F α → α) (x : PFunctor.W (Qpf.P F)) : Qpf.recF g x = g (Qpf.abs (Qpf.recF g <$> PFunctor.W.dest x))

theorem Qpf.recF_eq' {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F α → α) (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) a → PFunctor.W (Qpf.P F)) : Qpf.recF g (WType.mk a f) = g (Qpf.abs (Qpf.recF g <$> { fst := a, snd := f }))

inductive Qpf.Wequiv {F : Type u → Type u} [Functor F] [q : Qpf F] : PFunctor.W (Qpf.P F) → PFunctor.W (Qpf.P F) → Prop

• ind: ∀ {F : Type u → Type u} [inst : Functor F] [q : Qpf F] (a : (Qpf.P F).A) (f f' : PFunctor.B (Qpf.P F) a → PFunctor.W (Qpf.P F)), (∀ (x : PFunctor.B (Qpf.P F) a), Qpf.Wequiv (f x) (f' x)) → Qpf.Wequiv (WType.mk a f) (WType.mk a f')
• abs: ∀ {F : Type u → Type u} [inst : Functor F] [q : Qpf F] (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) a → PFunctor.W (Qpf.P F)) (a' : (Qpf.P F).A) (f' : PFunctor.B (Qpf.P F) a' → PFunctor.W (Qpf.P F)), Qpf.abs { fst := a, snd := f } = Qpf.abs { fst := a', snd := f' } → Qpf.Wequiv (WType.mk a f) (WType.mk a' f')
• trans: ∀ {F : Type u → Type u} [inst : Functor F] [q : Qpf F] (u v w : PFunctor.W (Qpf.P F)), Qpf.Wequiv u v → Qpf.Wequiv v w → Qpf.Wequiv u w

two trees are equivalent if their F-abstractions are

theorem Qpf.recF_eq_of_Wequiv {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (u : F α → α) (x : PFunctor.W (Qpf.P F)) (y : PFunctor.W (Qpf.P F)) : Qpf.Wequiv x y → Qpf.recF u x = Qpf.recF u y

recF is insensitive to the representation

theorem Qpf.Wequiv.abs' {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) (y : PFunctor.W (Qpf.P F)) (h : Qpf.abs (PFunctor.W.dest x) = Qpf.abs (PFunctor.W.dest y)) : Qpf.Wequiv x y

theorem Qpf.Wequiv.refl {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) : Qpf.Wequiv x x

theorem Qpf.Wequiv.symm {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) (y : PFunctor.W (Qpf.P F)) : Qpf.Wequiv x y → Qpf.Wequiv y x

def Qpf.Wrepr {F : Type u → Type u} [Functor F] [q : Qpf F] : PFunctor.W (Qpf.P F) → PFunctor.W (Qpf.P F)

maps every element of the W type to a canonical representative

theorem Qpf.Wrepr_equiv {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) : Qpf.Wequiv (Qpf.Wrepr x) x

def Qpf.Wsetoid {F : Type u → Type u} [Functor F] [q : Qpf F] : Setoid (PFunctor.W (Qpf.P F))

Define the fixed point as the quotient of trees under the equivalence relation Wequiv.

def Qpf.Fix (F : Type u → Type u) [Functor F] [q : Qpf F] : Type u

inductive type defined as initial algebra of a Quotient of Polynomial Functor

def Qpf.Fix.rec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F α → α) : Qpf.Fix F → α

recursor of a type defined by a qpf

def Qpf.fixToW {F : Type u → Type u} [Functor F] [q : Qpf F] : Qpf.Fix F → PFunctor.W (Qpf.P F)

access the underlying W-type of a fixpoint data type

def Qpf.Fix.mk {F : Type u → Type u} [Functor F] [q : Qpf F] (x : F (Qpf.Fix F)) : Qpf.Fix F

constructor of a type defined by a qpf

def Qpf.Fix.dest {F : Type u → Type u} [Functor F] [q : Qpf F] : Qpf.Fix F → F (Qpf.Fix F)

destructor of a type defined by a qpf

theorem Qpf.Fix.rec_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F α → α) (x : F (Qpf.Fix F)) : Qpf.Fix.rec g (Qpf.Fix.mk x) = g (Qpf.Fix.rec g <$> x)

theorem Qpf.Fix.ind_aux {F : Type u → Type u} [Functor F] [q : Qpf F] (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) a → PFunctor.W (Qpf.P F)) : Qpf.Fix.mk (Qpf.abs { fst := a, snd := fun x => Quotient.mk Qpf.Wsetoid (f x) }) = Quotient.mk Qpf.Wsetoid (WType.mk a f)

theorem Qpf.Fix.ind_rec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g₁ : Qpf.Fix F → α) (g₂ : Qpf.Fix F → α) (h : ∀ (x : F (Qpf.Fix F)), g₁ <$> x = g₂ <$> x → g₁ (Qpf.Fix.mk x) = g₂ (Qpf.Fix.mk x)) (x : Qpf.Fix F) : g₁ x = g₂ x

theorem Qpf.Fix.rec_unique {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F α → α) (h : Qpf.Fix F → α) (hyp : ∀ (x : F (Qpf.Fix F)), h (Qpf.Fix.mk x) = g (h <$> x)) : Qpf.Fix.rec g = h

theorem Qpf.Fix.mk_dest {F : Type u → Type u} [Functor F] [q : Qpf F] (x : Qpf.Fix F) : Qpf.Fix.mk (Qpf.Fix.dest x) = x

theorem Qpf.Fix.dest_mk {F : Type u → Type u} [Functor F] [q : Qpf F] (x : F (Qpf.Fix F)) : Qpf.Fix.dest (Qpf.Fix.mk x) = x

theorem Qpf.Fix.ind {F : Type u → Type u} [Functor F] [q : Qpf F] (p : Qpf.Fix F → Prop) (h : (x : F (Qpf.Fix F)) → Functor.Liftp p x → p (Qpf.Fix.mk x)) (x : Qpf.Fix F) : p x

def Qpf.corecF {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : α → F α) : α → PFunctor.M (Qpf.P F)

does recursion on q.P.M using g : α → F α rather than g : α → P α

theorem Qpf.corecF_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : α → F α) (x : α) : PFunctor.M.dest (Qpf.corecF g x) = Qpf.corecF g <$> Qpf.repr (g x)

def Qpf.IsPrecongr {F : Type u → Type u} [Functor F] [q : Qpf F] (r : PFunctor.M (Qpf.P F) → PFunctor.M (Qpf.P F) → Prop) : Prop

A pre-congruence on q.P.M viewed as an F-coalgebra. Not necessarily symmetric.

def Qpf.Mcongr {F : Type u → Type u} [Functor F] [q : Qpf F] : PFunctor.M (Qpf.P F) → PFunctor.M (Qpf.P F) → Prop

The maximal congruence on q.P.M.

def Qpf.Cofix (F : Type u → Type u) [Functor F] [q : Qpf F] : Type u

coinductive type defined as the final coalgebra of a qpf

instance Qpf.instInhabitedCofix {F : Type u → Type u} [Functor F] [q : Qpf F] [Inhabited (Qpf.P F).A] : Inhabited (Qpf.Cofix F)

def Qpf.Cofix.corec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : α → F α) (x : α) : Qpf.Cofix F

corecursor for type defined by Cofix

def Qpf.Cofix.dest {F : Type u → Type u} [Functor F] [q : Qpf F] : Qpf.Cofix F → F (Qpf.Cofix F)

destructor for type defined by Cofix

theorem Qpf.Cofix.dest_corec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : α → F α) (x : α) : Qpf.Cofix.dest (Qpf.Cofix.corec g x) = Qpf.Cofix.corec g <$> g x

theorem Qpf.Cofix.bisim_rel {F : Type u → Type u} [Functor F] [q : Qpf F] (r : Qpf.Cofix F → Qpf.Cofix F → Prop) (h : ∀ (x y : Qpf.Cofix F), r x y → Quot.mk r <$> Qpf.Cofix.dest x = Quot.mk r <$> Qpf.Cofix.dest y) (x : Qpf.Cofix F) (y : Qpf.Cofix F) : r x y → x = y

theorem Qpf.Cofix.bisim {F : Type u → Type u} [Functor F] [q : Qpf F] (r : Qpf.Cofix F → Qpf.Cofix F → Prop) (h : ∀ (x y : Qpf.Cofix F), r x y → Functor.Liftr r (Qpf.Cofix.dest x) (Qpf.Cofix.dest y)) (x : Qpf.Cofix F) (y : Qpf.Cofix F) : r x y → x = y

theorem Qpf.Cofix.bisim' {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u_1} (Q : α → Prop) (u : α → Qpf.Cofix F) (v : α → Qpf.Cofix F) (h : ∀ (x : α), Q x → ∃ a f f', Qpf.Cofix.dest (u x) = Qpf.abs { fst := a, snd := f } ∧ Qpf.Cofix.dest (v x) = Qpf.abs { fst := a, snd := f' } ∧ ∀ (i : PFunctor.B (Qpf.P F) a), ∃ x', Q x' ∧ f i = u x' ∧ f' i = v x') (x : α) : Q x → u x = v x

def Qpf.comp {F₂ : Type u → Type u} [Functor F₂] [q₂ : Qpf F₂] {F₁ : Type u → Type u} [Functor F₁] [q₁ : Qpf F₁] : Qpf (Functor.Comp F₂ F₁)

composition of qpfs gives another qpf

def Qpf.quotientQpf {F : Type u → Type u} [Functor F] [q : Qpf F] {G : Type u → Type u} [Functor G] {FG_abs : {α : Type u} → F α → G α} {FG_repr : {α : Type u} → G α → F α} (FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs α (FG_repr α x) = x) (FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs β (f <$> x) = f <$> FG_abs α x) : Qpf G

Given a qpf F and a well-behaved surjection FG_abs from F α to functor G α, G is a qpf. We can consider G a quotient on F where elements x y : F α are in the same equivalence class if FG_abs x = FG_abs y.

theorem Qpf.mem_supp {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) (u : α) : u ∈ Functor.supp x ↔ ∀ (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) a → α), Qpf.abs { fst := a, snd := f } = x → u ∈ f '' Set.univ

theorem Qpf.supp_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) : Functor.supp x = {u | ∀ (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) a → α), Qpf.abs { fst := a, snd := f } = x → u ∈ f '' Set.univ}

theorem Qpf.has_good_supp_iff {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) : (∀ (p : α → Prop), Functor.Liftp p x ↔ ∀ (u : α), u ∈ Functor.supp x → p u) ↔ ∃ a f, Qpf.abs { fst := a, snd := f } = x ∧ ∀ (a' : (Qpf.P F).A) (f' : PFunctor.B (Qpf.P F) a' → α), Qpf.abs { fst := a', snd := f' } = x → f '' Set.univ ⊆ f' '' Set.univ

def Qpf.IsUniform {F : Type u → Type u} [Functor F] [q : Qpf F] : Prop

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

def Qpf.LiftpPreservation {F : Type u → Type u} [Functor F] [q : Qpf F] : Prop

does abs preserve Liftp?

def Qpf.SuppPreservation {F : Type u → Type u} [Functor F] [q : Qpf F] : Prop

does abs preserve supp?

theorem Qpf.supp_eq_of_isUniform {F : Type u → Type u} [Functor F] [q : Qpf F] (h : Qpf.IsUniform) {α : Type u} (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) a → α) : Functor.supp (Qpf.abs { fst := a, snd := f }) = f '' Set.univ

theorem Qpf.liftp_iff_of_isUniform {F : Type u → Type u} [Functor F] [q : Qpf F] (h : Qpf.IsUniform) {α : Type u} (x : F α) (p : α → Prop) : Functor.Liftp p x ↔ (u : α) → u ∈ Functor.supp x → p u

theorem Qpf.supp_map {F : Type u → Type u} [Functor F] [q : Qpf F] (h : Qpf.IsUniform) {α : Type u} {β : Type u} (g : α → β) (x : F α) : Functor.supp (g <$> x) = g '' Functor.supp x

theorem Qpf.suppPreservation_iff_uniform {F : Type u → Type u} [Functor F] [q : Qpf F] : Qpf.SuppPreservation ↔ Qpf.IsUniform

theorem Qpf.suppPreservation_iff_liftpPreservation {F : Type u → Type u} [Functor F] [q : Qpf F] : Qpf.SuppPreservation ↔ Qpf.LiftpPreservation

theorem Qpf.liftpPreservation_iff_uniform {F : Type u → Type u} [Functor F] [q : Qpf F] : Qpf.LiftpPreservation ↔ Qpf.IsUniform