open import 1Lab.Reflection.Record open import Cat.Univalent.Instances.Opposite open import Cat.Displayed.Instances.Family open import Cat.Displayed.Univalence open import Cat.Instances.Discrete open import Cat.Instances.Functor open import Cat.Displayed.Fibre open import Cat.Displayed.Total open import Cat.Displayed.Base open import Cat.Instances.Sets open import Cat.Prelude import Cat.Reasoning 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 .fst β£ β β£ B .fst β£) ] β x β β£ B .snd (f x) β£ β β£ A .snd x β£) unquoteDef poly-maps = define-record-iso poly-maps (quote Total-hom)

## 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.