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)

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.

• 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 (PFunctor.map (QPF.P F) f p) = f <$> QPF.abs p

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 : (QPF.P F).A) (f : (QPF.P F).B a → α), x = QPF.abs { fst := a, snd := f } ∧ ∀ (i : (QPF.P F).B 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.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} [Functor F] [q : QPF F] {α : Type u} (r : α → α → Prop) (x : F α) (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 { fst := a, snd := f₀ } ∧ y = QPF.abs { fst := a, snd := f₁ } ∧ ∀ (i : (QPF.P F).B 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.P F).B a) => 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 (PFunctor.map (QPF.P F) (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 : (QPF.P F).B a → PFunctor.W (QPF.P F)) : QPF.recF g (WType.mk a f) = g (QPF.abs (PFunctor.map (QPF.P F) (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

two trees are equivalent if their F-abstractions are

• ind: ∀ {F : Type u → Type u} [inst : Functor F] [q : QPF F] (a : (QPF.P F).A) (f f' : (QPF.P F).B a → PFunctor.W (QPF.P F)), (∀ (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} [inst : Functor F] [q : QPF F] (a : (QPF.P F).A) (f : (QPF.P F).B a → PFunctor.W (QPF.P F)) (a' : (QPF.P F).A) (f' : (QPF.P F).B 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

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

Equations

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

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.

Equations

• QPF.Wsetoid = { r := QPF.Wequiv, iseqv := (_ : Equivalence QPF.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

Equations

• QPF.Fix F = Quotient QPF.Wsetoid

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

Equations

• QPF.Fix.rec g = Quot.lift (QPF.recF g) (_ : ∀ (x y : PFunctor.W (QPF.P F)), QPF.Wequiv x y → QPF.recF g x = QPF.recF g y)

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

Equations

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

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

Equations

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

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

Equations

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

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 : (QPF.P F).B a → PFunctor.W (QPF.P F)) : QPF.Fix.mk (QPF.abs { fst := a, snd := fun (x : (QPF.P F).B a) => ⟦f x⟧ }) = ⟦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 α

Equations

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

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) = PFunctor.map (QPF.P F) (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.

Equations

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

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.

Equations

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

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

Equations

• QPF.Cofix F = Quot QPF.Mcongr

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

Equations

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

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

Equations

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

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

Equations

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

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 : (QPF.P F).A) (f : (QPF.P F).B a → QPF.Cofix F) (f' : (QPF.P F).B a → QPF.Cofix F), QPF.Cofix.dest (u x) = QPF.abs { fst := a, snd := f } ∧ QPF.Cofix.dest (v x) = QPF.abs { fst := a, snd := 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} [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

Equations

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

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.

Equations

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

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 : (QPF.P F).B 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 : (QPF.P F).B 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 ∈ Functor.supp x, p u) ↔ ∃ (a : (QPF.P F).A) (f : (QPF.P F).B a → α), QPF.abs { fst := a, snd := f } = x ∧ ∀ (a' : (QPF.P F).A) (f' : (QPF.P F).B 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.

Equations

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

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

does abs preserve Liftp?

Equations

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

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

does abs preserve supp?

Equations

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

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 : (QPF.P F).B 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 ∈ 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