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 v) extends Functor F : Type (max (max (u + 1) (u' + 1)) v)

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.

• map {α β : Type u} : (α → β) → F α → F β
• mapConst {α β : Type u} : α → F β → F α
• P : PFunctor.{u, u'}
• abs {α : Type u} : ↑(P F) α → F α
• repr {α : Type u} : F α → ↑(P F) α
• abs_repr {α : Type u} (x : F α) : abs (repr x) = x
• abs_map {α β : Type u} (f : α → β) (p : ↑(P F) α) : abs ((P F).map f p) = f <$> abs p

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

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

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

theorem QPF.liftp_iff {F : Type u → Type v} [q : QPF F] {α : Type u} (p : α → Prop) (x : F α) : Functor.Liftp p x ↔ ∃ (a : (P F).A) (f : (P F).B a → α), x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

theorem QPF.liftp_iff' {F : Type u → Type v} [q : QPF F] {α : Type u} (p : α → Prop) (x : F α) : Functor.Liftp p x ↔ ∃ (u : ↑(P F) α), abs u = x ∧ ∀ (i : (P F).B u.fst), p (u.snd i)

theorem QPF.liftr_iff {F : Type u → Type v} [q : QPF F] {α : Type u} (r : α → α → Prop) (x y : F α) : Functor.Liftr r x y ↔ ∃ (a : (P F).A) (f₀ : (P F).B a → α) (f₁ : (P F).B a → α), x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

def QPF.recF {F : Type u → Type v} [q : QPF F] {α : Type u} (g : F α → α) : (P F).W → α

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

theorem QPF.recF_eq {F : Type u → Type v} [q : QPF F] {α : Type u} (g : F α → α) (x : (P F).W) : recF g x = g (abs ((P F).map (recF g) x.dest))

theorem QPF.recF_eq' {F : Type u → Type v} [q : QPF F] {α : Type u} (g : F α → α) (a : (P F).A) (f : (P F).B a → (P F).W) : recF g (WType.mk a f) = g (abs ((P F).map (recF g) ⟨a, f⟩))

inductive QPF.Wequiv {F : Type u → Type v} [q : QPF F] : (P F).W → (P F).W → Prop

two trees are equivalent if their F-abstractions are

• ind {F : Type u → Type v} [q : QPF F] (a : (P F).A) (f f' : (P F).B a → (P F).W) : (∀ (x : (P F).B a), Wequiv (f x) (f' x)) → Wequiv (WType.mk a f) (WType.mk a f')
• abs {F : Type u → Type v} [q : QPF F] (a : (P F).A) (f : (P F).B a → (P F).W) (a' : (P F).A) (f' : (P F).B a' → (P F).W) : QPF.abs ⟨a, f⟩ = QPF.abs ⟨a', f'⟩ → Wequiv (WType.mk a f) (WType.mk a' f')
• trans {F : Type u → Type v} [q : QPF F] (u v w : (P F).W) : Wequiv u v → Wequiv v w → Wequiv u w

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

recF is insensitive to the representation

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

theorem QPF.Wequiv.refl {F : Type u → Type v} [q : QPF F] (x : (P F).W) : Wequiv x x

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

def QPF.Wrepr {F : Type u → Type v} [q : QPF F] : (P F).W → (P F).W

maps every element of the W type to a canonical representative

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

@[implicit_reducible]

def QPF.Wsetoid {F : Type u → Type v} [q : QPF F] : Setoid (P F).W

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

def QPF.Fix (F : Type u → Type u) [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} [q : QPF F] {α : Type u} (g : F α → α) : Fix F → α

recursor of a type defined by a qpf

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

access the underlying W-type of a fixpoint data type

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

constructor of a type defined by a qpf

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

destructor of a type defined by a qpf

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

theorem QPF.Fix.ind_aux {F : Type u → Type u} [q : QPF F] (a : (P F).A) (f : (P F).B a → (P F).W) : mk (abs ⟨a, fun (x : (P F).B a) => ⟦f x⟧⟩) = ⟦WType.mk a f⟧

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

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

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

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

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

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

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

theorem QPF.corecF_eq {F : Type u → Type u} [q : QPF F] {α : Type u} (g : α → F α) (x : α) : (corecF g x).dest = (P F).map (corecF g) (repr (g x))

def QPF.IsPrecongr {F : Type u → Type u} [q : QPF F] (r : (P F).M → (P F).M → 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} [q : QPF F] : (P F).M → (P F).M → Prop

The maximal congruence on q.P.M.

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

coinductive type defined as the final coalgebra of a qpf

@[implicit_reducible]

instance QPF.instInhabitedCofixOfAP {F : Type u → Type u} [q : QPF F] [Inhabited (P F).A] : Inhabited (Cofix F)

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

corecursor for type defined by Cofix

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

destructor for type defined by Cofix

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

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

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

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

@[implicit_reducible]

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

composition of qpfs gives another qpf

@[implicit_reducible]

def QPF.quotientQPF {F : Type u → Type u} [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} [q : QPF F] {α : Type u} (x : F α) (u : α) : u ∈ Functor.supp x ↔ ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' Set.univ

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

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

def QPF.IsUniform {F : Type u → Type u} [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} [q : QPF F] : Prop

does abs preserve Liftp?

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

does abs preserve supp?

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

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

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

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

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

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