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 Equivalently, it is the total category of the family fibration of More concretely, an object of is given by a set and a family of sets The idea is that these data corresponds to the polynomial (set-valued, with set coefficients) given by

Poly : βˆ€ β„“ β„“' β†’ Precategory (lsuc β„“ βŠ” lsuc β„“') (β„“ βŠ” β„“')
Poly β„“ β„“' = ∫ (Family (Sets β„“' ^op) {β„“ = β„“})

module Poly where
  module _ β„“ β„“' where
    open Precategory (Poly β„“ β„“') using (Ob) public

  module _ {β„“ β„“'} where
    open Cat.Reasoning (Poly β„“ β„“') hiding (Ob) public

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 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 : Poly.Ob β„“ β„“'}
  β†’ 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 morphisms using regularity:

poly-map-path
  : βˆ€ {β„“ β„“'} {A B : Poly.Ob β„“ β„“'} {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 polynomials. In particular, given a polynomial it should be possible to evaluate it at a set 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 as linear, since these are those of the form i.e. If the family is constant at some other set, e.g.Β  we refer to the corresponding polynomial as a monomial, since it can be written

LensesπŸ”—

We call the maps in dependent lenses, or simply lenses, because in the case of maps between monomials 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 together with an update function 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 value given an but upon writing a to the same pointer, our changes to a instead.