module Cat.Instances.Poly where

Polynomial functors and lensesπŸ”—

The category of polynomial functors is the free coproduct completion of Setsop\mathbf{Sets}^{\mathrm{op}}. Equivalently, it is the total category of the family fibration of Setsop\mathbf{Sets}^{\mathrm{op}}. More concretely, an object of Poly\mathbf{Poly} is given by a set II and a family of sets A:I→SetsA : I \to \mathbf{Sets}. The idea is that these data corresponds to the polynomial (set-valued, with set coefficients) given by

p(y)=βˆ‘i:IyAi p(y) = \sum_{i : I} y^{A_i}

Poly : βˆ€ β„“ β†’ Precategory (lsuc β„“) β„“
Poly β„“ = ∫ {β„“ = β„“} (Family (Sets β„“ ^op))

module Poly {β„“} = Cat.Reasoning (Poly β„“)

Our standard toolkit for showing univalence of total categories applies here:

Poly-is-category : βˆ€ {β„“} β†’ is-category (Poly β„“)
Poly-is-category =
  is-category-total _ Sets-is-category $
    is-category-fibrewise' _
      (Ξ» x β†’ Families-are-categories _ x (opposite-is-category Sets-is-category))

It is entirely mechanical to calculate that morphisms in Poly\mathbf{Poly} are given by pairs of a reindexing together with a contravariant action on the families. It is so mechanical that we can do it automatically:

poly-maps : βˆ€ {β„“} {A B} β†’ Iso
  (Poly.Hom {β„“} A B)
  (Ξ£[ f ∈ (⌞ A ⌟ β†’ ⌞ B ⌟) ] βˆ€ x β†’ ∣ B .snd (f x) ∣ β†’ ∣ A .snd x ∣)
unquoteDef poly-maps = define-record-iso poly-maps (quote Total-hom)

We also derive a convenient characterisation of paths between Poly\mathbf{Poly} morphisms using regularity:

  : βˆ€ {β„“ A B} {f g : Poly.Hom {β„“} A B}
  β†’ (hom≑ : f .hom ≑ g .hom)
  β†’ (pre≑ : βˆ€ a b β†’ f .preserves a (subst (Ξ» hom β†’ ∣ B .snd (hom a) ∣) (sym hom≑) b)
                  ≑ g .preserves a b)
  β†’ f ≑ g
poly-map-path hom≑ pre≑ = total-hom-path _ hom≑
  (to-pathp (ext Ξ» a b β†’ Regularity.precise! (pre≑ a b)))

Polynomials as functorsπŸ”—

We commented above that polynomials, i.e.Β terms of the type Poly, should correspond to particular Sets\mathbf{Sets}-valued polynomials. In particular, given a polynomial (I,A)(I, A), it should be possible to evaluate it at a set XX and get back a set. We take the interpretation above literally:

Polynomial-functor : βˆ€ {β„“} β†’ Poly.Ob {β„“} β†’ Functor (Sets β„“) (Sets β„“)
Polynomial-functor (I , A) .Fβ‚€ X = el! (Ξ£[ i ∈ ∣ I ∣ ] (∣ A i ∣ β†’ ∣ X ∣))
Polynomial-functor (I , A) .F₁ f (a , g) = a , Ξ» z β†’ f (g z)
Polynomial-functor (I , A) .F-id = refl
Polynomial-functor (I , A) .F-∘ f g = refl

Correspondingly, we refer to a polynomial whose family is x↦1x \mapsto 1 as linear, since these are those of the form βˆ‘i:Iy1\sum_{i : I} y^1, i.e. Iy1Iy^1. If the family is constant at some other set, e.g.Β BB, we refer to the corresponding polynomial as a monomial, since it can be written IyBIy^B.


We call the maps in Poly\mathbf{Poly} dependent lenses, or simply lenses, because in the case of maps between monomials SiT→AyBSi^T \to Ay^B, we recover the usual definition of the Haskell type Lens s t a b:

Lens : βˆ€ {β„“} (S T A B : Set β„“) β†’ Type β„“
Lens S T A B = Poly.Hom (S , Ξ» _ β†’ T) (A , Ξ» _ β†’ B)

_ : βˆ€ {β„“} {S T A B : Set β„“} β†’ Iso
  (Lens S T A B)
  ((∣ S ∣ β†’ ∣ A ∣) Γ— (∣ S ∣ β†’ ∣ B ∣ β†’ ∣ T ∣))
_ = poly-maps

We have a view function Sβ†’AS \to A together with an update function Sβ†’Bβ†’TS \to B \to T. The view and update functions are allowed to change the type of the container: the idea is that a lens represents a β€œlabel” or β€œpointer” from which one can read off an AA value given an SS, but upon writing a BB to the same pointer, our SS changes to a TT instead.