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 Setsop\mathbf{Sets}^{\mathrm{op}}. Equivalently, it is the total category of the family fibration of Setsop\mathbf{Sets}^{\mathrm{op}}. More concretely, an object of Poly\mathbf{Poly} is given by a set II and a family of sets A:I→SetsA : I \to \mathbf{Sets}. The idea is that these data corresponds to the polynomial (set-valued, with set coefficients) given by

p(y)=βˆ‘i:IyAi 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 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\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 Poly\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 Sets\mathbf{Sets}-valued polynomials. In particular, given a polynomial (I,A)(I, A), it should be possible to evaluate it at a set XX 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↦1x \mapsto 1 as linear, since these are those of the form βˆ‘i:Iy1\sum_{i : I} y^1, i.e. Iy1Iy^1. If the family is constant at some other set, e.g.Β BB, we refer to the corresponding polynomial as a monomial, since it can be written IyBIy^B.

LensesπŸ”—

We call the maps in Poly\mathbf{Poly} dependent lenses, or simply lenses, because in the case of maps between monomials SiT→AyBSi^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β†’AS \to A together with an update function Sβ†’Bβ†’TS \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 AA value given an SS, but upon writing a BB to the same pointer, our SS changes to a TT instead.