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 . Equivalently, it is the total space 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 β) β 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 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 -valued 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 β£)) 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.