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.Displayed.Total
open import Cat.Instances.Sets
open import Cat.Prelude

import Cat.Reasoning

module Cat.Instances.Poly where

open Functor
open Total-hom

Polynomial functors and lenses🔗

The category of polynomial functors is the free coproduct completion of ${\mathbf{Sets}}^{\mathrm{op}}\text{.}$ Equivalently, it is the total category of the family fibration of ${\mathbf{Sets}}^{\mathrm{op}}\text{.}$ More concretely, an object of $\mathbf{Poly}$ is given by a set $I$ and a family of sets $A:I\to \mathbf{Sets}\text{.}$ 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 $\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 (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 $\mathbf{Sets}\text{-valued}$ polynomials. In particular, given a polynomial $(I,A)\text{,}$ 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 )
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\text{,}$ i.e. $I{y}^1\text{.}$ If the family is constant at some other set, e.g. $B\text{,}$ we refer to the corresponding polynomial as a monomial, since it can be written $I{y}^B\text{.}$

Lenses🔗

We call the maps in $\mathbf{Poly}$ dependent lenses, or simply lenses, because in the case of maps between monomials $S{i}^T\to A{y}^B\text{,}$ 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\text{.}$ 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\text{,}$ but upon writing a $B$ to the same pointer, our $S$ changes to a $T$ instead.