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.