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

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}
• abs : {α : Type u} → ↑(QPF.P F) α → F α
• repr : {α : Type u} → F α → ↑(QPF.P F) α
• abs_repr : ∀ {α : Type u} (x : F α), QPF.abs (QPF.repr x) = x
• abs_map : ∀ {α β : Type u} (f : α → β) (p : ↑(QPF.P F) α), QPF.abs ((QPF.P F).map f p) = f <$> QPF.abs p

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

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

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

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

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

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

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

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

Equations

• QPF.recF g (WType.mk a f) = g (QPF.abs ⟨a, fun (x : (QPF.P F).B a) => QPF.recF g (f x)⟩)

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

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

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

two trees are equivalent if their F-abstractions are

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

theorem QPF.recF_eq_of_Wequiv {F : Type u → Type u} [q : QPF F] {α : Type u} (u : F α → α) (x y : (QPF.P F).W) : 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} [q : QPF F] (x y : (QPF.P F).W) (h : QPF.abs x.dest = QPF.abs y.dest) : QPF.Wequiv x y

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

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

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

maps every element of the W type to a canonical representative

Equations

• QPF.Wrepr = QPF.recF (PFunctor.W.mk ∘ QPF.repr)

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

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

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

Equations

• QPF.Wsetoid = { r := QPF.Wequiv, iseqv := ⋯ }

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

Equations

• QPF.Fix F = Quotient QPF.Wsetoid

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

recursor of a type defined by a qpf

Equations

• QPF.Fix.rec g = Quot.lift (QPF.recF g) ⋯

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

access the underlying W-type of a fixpoint data type

Equations

• QPF.fixToW = Quotient.lift QPF.Wrepr ⋯

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

constructor of a type defined by a qpf

Equations

• QPF.Fix.mk x = Quot.mk (⇑QPF.Wsetoid) (PFunctor.W.mk ((QPF.P F).map QPF.fixToW (QPF.repr x)))

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

destructor of a type defined by a qpf

Equations

• QPF.Fix.dest = QPF.Fix.rec (Functor.map QPF.Fix.mk)

theorem QPF.Fix.rec_eq {F : Type u → Type u} [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} [q : QPF F] (a : (QPF.P F).A) (f : (QPF.P F).B a → (QPF.P F).W) : QPF.Fix.mk (QPF.abs ⟨a, fun (x : (QPF.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₂ : 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} [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} [q : QPF F] (x : QPF.Fix F) : QPF.Fix.mk x.dest = x

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

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

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

Equations

• QPF.corecF g = PFunctor.M.corec fun (x : α) => QPF.repr (g x)

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

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

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

Equations

• QPF.IsPrecongr r = ∀ ⦃x y : (QPF.P F).M⦄, r x y → QPF.abs ((QPF.P F).map (Quot.mk r) x.dest) = QPF.abs ((QPF.P F).map (Quot.mk r) y.dest)

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

The maximal congruence on q.P.M.

Equations

• QPF.Mcongr x y = ∃ (r : (QPF.P F).M → (QPF.P F).M → Prop), QPF.IsPrecongr r ∧ r x y

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

coinductive type defined as the final coalgebra of a qpf

Equations

• QPF.Cofix F = Quot QPF.Mcongr

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

Equations

• QPF.instInhabitedCofixOfAP = { default := Quot.mk QPF.Mcongr default }

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

corecursor for type defined by Cofix

Equations

• QPF.Cofix.corec g x = Quot.mk QPF.Mcongr (QPF.corecF g x)

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

destructor for type defined by Cofix

Equations

• QPF.Cofix.dest = Quot.lift (fun (x : (QPF.P F).M) => Quot.mk QPF.Mcongr <$> QPF.abs x.dest) ⋯

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

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

theorem QPF.Cofix.bisim {F : Type u → Type u} [q : QPF F] (r : QPF.Cofix F → QPF.Cofix F → Prop) (h : ∀ (x y : QPF.Cofix F), r x y → Functor.Liftr r x.dest y.dest) (x y : QPF.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 : α → QPF.Cofix F) (h : ∀ (x : α), Q x → ∃ (a : (QPF.P F).A) (f : (QPF.P F).B a → QPF.Cofix F) (f' : (QPF.P F).B a → QPF.Cofix F), (u x).dest = QPF.abs ⟨a, f⟩ ∧ (v x).dest = QPF.abs ⟨a, f'⟩ ∧ ∀ (i : (QPF.P F).B 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} [q₂ : QPF F₂] {F₁ : Type u → Type u} [q₁ : QPF F₁] : QPF (Functor.Comp F₂ F₁)

composition of qpfs gives another qpf

Equations

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

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.

Equations

• QPF.quotientQPF FG_abs_repr FG_abs_map = QPF.mk (QPF.P F) (fun {x : Type ?u.88} (p : ↑(QPF.P F) x) => FG_abs (QPF.abs p)) (fun {x : Type ?u.88} (x_1 : G x) => QPF.repr (FG_repr x_1)) ⋯ ⋯

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

Equations

• QPF.IsUniform = ∀ ⦃α : Type ?u.26⦄ (a a' : (QPF.P F).A) (f : (QPF.P F).B a → α) (f' : (QPF.P F).B a' → α), QPF.abs ⟨a, f⟩ = QPF.abs ⟨a', f'⟩ → f '' Set.univ = f' '' Set.univ

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

does abs preserve Liftp?

Equations

• QPF.LiftpPreservation = ∀ ⦃α : Type ?u.4⦄ (p : α → Prop) (x : ↑(QPF.P F) α), Functor.Liftp p (QPF.abs x) ↔ Functor.Liftp p x

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

does abs preserve supp?

Equations

• QPF.SuppPreservation = ∀ ⦃α : Type ?u.18⦄ (x : ↑(QPF.P F) α), Functor.supp (QPF.abs x) = Functor.supp x

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

theorem QPF.liftp_iff_of_isUniform {F : Type u → Type u} [q : QPF F] (h : QPF.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 : QPF.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] : QPF.SuppPreservation ↔ QPF.IsUniform

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

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