module Cat.Instances.Poly where

# Polynomial functors and lensesπ

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

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' _ Sets-is-category (Ξ» x β Families-are-categories _ x (opposite-is-category Sets-is-category))

It is entirely mechanical to calculate that morphisms in
$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$ 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 (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-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 β)) (hlevel 2) 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β¦1$
as *linear*, since these are those of the form
$β_{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
$Poly$
*dependent lenses*, or simply *lenses*, because in the
case of maps between monomials
$Si_{T}β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βA$
together with an *update* function
$SβBβ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.