module Cat.Instances.Poly where

# Polynomial functors and lensesπ

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

$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 spaces applies here:

Poly-is-category : β {β} β is-category (Poly β) Poly-is-category = is-category-total _ Sets-is-category $ is-category-fibrewiseβ² _ Sets-is-category (Ξ» x β Families-are-categories _ x (opposite-is-category Sets-is-category))

It is entirely mechanical to calculate that morphisms in
$\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 $\mathbf{Poly}$ morphisms using regularity:

poly-map-path : β {β 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 (funext Ξ» a β funext Ξ» 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
$\mathbf{Sets}$-valued
polynomials. In particular, given a polynomial
$(I, A)$,
it should be possible to evaluate it at a set
$X$
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 \mapsto 1$
as *linear*, since these are those of the form
$\sum_{i : I} y^1$,
i.e.
$Iy^1$.
If the family is constant at some *other* set,
e.g.Β $B$,
we refer to the corresponding polynomial as a *monomial*, since
it can be written
$Iy^B$.

## Lensesπ

We call the maps in
$\mathbf{Poly}$
*dependent lenses*, or simply *lenses*, because in the
case of maps between monomials
$Si^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 \to A$
together with an *update* function
$S \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
$A$
value given an
$S$,
but upon writing a
$B$
to the same pointer, our
$S$
changes to a
$T$
instead.