# 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) [] :
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.

• abs : {α : Type u} → () αF α
• repr : {α : Type u} → F α() α
• abs_repr : ∀ {α : Type u} (x : F α), QPF.abs () = x
• abs_map : ∀ {α β : Type u} (f : αβ) (p : () α), QPF.abs (().map f p) = f <$> Instances theorem QPF.abs_repr {F : Type u → Type u} [] [self : QPF F] {α : Type u} (x : F α) : QPF.abs () = x theorem QPF.abs_map {F : Type u → Type u} [] [self : QPF F] {α : Type u} {β : Type u} (f : αβ) (p : () α) : QPF.abs (().map f p) = f <$>
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} {β : Type u} {γ : 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 ) :
theorem QPF.liftp_iff {F : Type u → Type u} [] [q : QPF F] {α : Type u} (p : αProp) (x : F α) :
∃ (a : ().A) (f : ().B aα), x = QPF.abs a, f ∀ (i : ().B a), p (f i)
theorem QPF.liftp_iff' {F : Type u → Type u} [] [q : QPF F] {α : Type u} (p : αProp) (x : F α) :
∃ (u : () α), = x ∀ (i : ().B u.fst), p (u.snd i)
theorem QPF.liftr_iff {F : Type u → Type u} [] [q : QPF F] {α : Type u} (r : ααProp) (x : F α) (y : F α) :
∃ (a : ().A) (f₀ : ().B aα) (f₁ : ().B aα), x = QPF.abs a, f₀ y = QPF.abs a, f₁ ∀ (i : ().B a), r (f₀ i) (f₁ i)
def QPF.recF {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : F αα) :
().Wα

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

Equations
Instances For
theorem QPF.recF_eq {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : F αα) (x : ().W) :
QPF.recF g x = g (QPF.abs (().map () x.dest))
theorem QPF.recF_eq' {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : F αα) (a : ().A) (f : ().B a().W) :
QPF.recF g (WType.mk a f) = g (QPF.abs (().map () a, f))
inductive QPF.Wequiv {F : Type u → Type u} [] [q : QPF F] :
().W().WProp

two trees are equivalent if their F-abstractions are

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

maps every element of the W type to a canonical representative

Equations
Instances For
theorem QPF.Wrepr_equiv {F : Type u → Type u} [] [q : QPF F] (x : ().W) :
def QPF.Wsetoid {F : Type u → Type u} [] [q : QPF F] :
Setoid ().W

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

Equations
• QPF.Wsetoid = { r := QPF.Wequiv, iseqv := }
Instances For
def QPF.Fix (F : Type u → Type u) [] [q : QPF F] :

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

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

recursor of a type defined by a qpf

Equations
Instances For
def QPF.fixToW {F : Type u → Type u} [] [q : QPF F] :
().W

access the underlying W-type of a fixpoint data type

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

constructor of a type defined by a qpf

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

destructor of a type defined by a qpf

Equations
Instances For
theorem QPF.Fix.rec_eq {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : F αα) (x : F ()) :
= g ()
theorem QPF.Fix.ind_aux {F : Type u → Type u} [] [q : QPF F] (a : ().A) (f : ().B a().W) :
QPF.Fix.mk (QPF.abs a, fun (x : ().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₂ : α) (h : ∀ (x : F ()), g₁ <$> x = g₂ <$> xg₁ () = g₂ ()) (x : ) :
g₁ x = g₂ x
theorem QPF.Fix.rec_unique {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : F αα) (h : α) (hyp : ∀ (x : F ()), h () = g (h <$> x)) : = h theorem QPF.Fix.mk_dest {F : Type u → Type u} [] [q : QPF F] (x : ) : QPF.Fix.mk x.dest = x theorem QPF.Fix.dest_mk {F : Type u → Type u} [] [q : QPF F] (x : F ()) : ().dest = x theorem QPF.Fix.ind {F : Type u → Type u} [] [q : QPF F] (p : Prop) (h : ∀ (x : F ()), p ()) (x : ) : p x def QPF.corecF {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : αF α) : α().M does recursion on q.P.M using g : α → F α rather than g : α → P α Equations Instances For theorem QPF.corecF_eq {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : αF α) (x : α) : ().dest = ().map () (QPF.repr (g x)) def QPF.IsPrecongr {F : Type u → Type u} [] [q : QPF F] (r : ().M().MProp) : A pre-congruence on q.P.M viewed as an F-coalgebra. Not necessarily symmetric. Equations • = ∀ ⦃x y : ().M⦄, r x yQPF.abs (().map () x.dest) = QPF.abs (().map () y.dest) Instances For def QPF.Mcongr {F : Type u → Type u} [] [q : QPF F] : ().M().MProp The maximal congruence on q.P.M. Equations • = ∃ (r : ().M().MProp), r x y Instances For def QPF.Cofix (F : Type u → Type u) [] [q : QPF F] : coinductive type defined as the final coalgebra of a qpf Equations Instances For instance QPF.instInhabitedCofixOfAP {F : Type u → Type u} [] [q : QPF F] [Inhabited ().A] : 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 : α) : corecursor for type defined by Cofix Equations Instances For def QPF.Cofix.dest {F : Type u → Type u} [] [q : QPF F] : F () destructor for type defined by Cofix Equations Instances For theorem QPF.Cofix.dest_corec {F : Type u → Type u} [] [q : QPF F] {α : Type u} (g : αF α) (x : α) : ().dest = <$> g x
theorem QPF.Cofix.bisim_rel {F : Type u → Type u} [] [q : QPF F] (r : Prop) (h : ∀ (x y : ), r x y <$> x.dest = <$> y.dest) (x : ) (y : ) :
r x yx = y
theorem QPF.Cofix.bisim {F : Type u → Type u} [] [q : QPF F] (r : Prop) (h : ∀ (x y : ), r x yFunctor.Liftr r x.dest y.dest) (x : ) (y : ) :
r x yx = y
theorem QPF.Cofix.bisim' {F : Type u → Type u} [] [q : QPF F] {α : Type u_1} (Q : αProp) (u : α) (v : α) (h : ∀ (x : α), Q x∃ (a : ().A) (f : ().B a) (f' : ().B a), (u x).dest = QPF.abs a, f (v x).dest = QPF.abs a, f' ∀ (i : ().B a), ∃ (x' : α), Q x' f i = u x' f' i = v x') (x : α) :
Q xu 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.
Instances For
def QPF.quotientQPF {F : Type u → Type u} [] [q : QPF F] {G : Type u → Type u} [] {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.
Instances For
theorem QPF.mem_supp {F : Type u → Type u} [] [q : QPF F] {α : Type u} (x : F α) (u : α) :
∀ (a : ().A) (f : ().B aα), QPF.abs a, f = xu f '' Set.univ
theorem QPF.supp_eq {F : Type u → Type u} [] [q : QPF F] {α : Type u} (x : F α) :
= {u : α | ∀ (a : ().A) (f : ().B aα), QPF.abs a, f = xu f '' Set.univ}
theorem QPF.has_good_supp_iff {F : Type u → Type u} [] [q : QPF F] {α : Type u} (x : F α) :
(∀ (p : αProp), u, p u) ∃ (a : ().A) (f : ().B aα), QPF.abs a, f = x ∀ (a' : ().A) (f' : ().B a'α), QPF.abs a', f' = xf '' Set.univ f' '' Set.univ
def QPF.IsUniform {F : Type u → Type u} [] [q : QPF F] :

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⦄ (a a' : ().A) (f : ().B aα) (f' : ().B a'α), QPF.abs a, f = QPF.abs a', f'f '' Set.univ = f' '' Set.univ
Instances For
def QPF.LiftpPreservation {F : Type u → Type u} [] [q : QPF F] :

does abs preserve Liftp?

Equations
Instances For
def QPF.SuppPreservation {F : Type u → Type u} [] [q : QPF F] :

does abs preserve supp?

Equations
• QPF.SuppPreservation = ∀ ⦃α : Type u⦄ (x : () α),
Instances For
theorem QPF.supp_eq_of_isUniform {F : Type u → Type u} [] [q : QPF F] (h : QPF.IsUniform) {α : Type u} (a : ().A) (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) :
u, p u
theorem QPF.supp_map {F : Type u → Type u} [] [q : QPF F] (h : QPF.IsUniform) {α : Type u} {β : Type u} (g : αβ) (x : F α) :
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