Legacy.Base.Categories.Functors

Functors

This is the Legacy.Base.Categories.Functors module of the Agda Universal Algebra Library.

Recall, a functor F is a function that maps the objects and morphisms of one category 𝒞 to the objects and morphisms of a category 𝒟 in such a way that the following functor laws are satisfied:

• ∀ f g, F(f ∘ g) = F(f) ∘ F(g)
• ∀ A, F(id A) = id (F A) (where id X denotes the identity morphism on X)

Polynomial functors

The main reference for this section is Modular Type-Safety Proofs in Agda by Schwaab and Siek (PLPV '07).

An important class of functors for our domain is the class of so called polynomial functors. These are functors that are built up using the constant, identity, sum, and product functors. To be precise, the actions of the latter on objects are as follows: ∀ A B (objects), ∀ F G (functors),

• const B A = B
• Id A = A
• (F + G) A = F A + G A
• (F × G) A = F A × G A

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.Categories.Functors where

-- Imports from Agda and the Agda Standard Library  ---------------------------------------
open import Agda.Primitive                         using () renaming ( Set to Type )
open import Data.Nat                               using ( ℕ ; zero ; suc ; _>_ )
open import Data.Sum.Base                          using ( _⊎_ ) renaming ( inj₁ to inl ;  inj₂ to inr )
open import Data.Product                           using ( Σ-syntax ; _,_ ; _×_ )
open import Data.Unit                              using ( tt ) renaming ( ⊤ to ⊤₀ )
open import Data.Unit.Polymorphic                  using ( ⊤ )
open import Relation.Binary.PropositionalEquality  using ( _≡_ ; refl ; _≢_ )
open import Level                                  using ( _⊔_ ; Level ) renaming (suc to lsuc ; 0ℓ to ℓ₀ )

private variable α β : Level

infixl  _⊕_
infixr  _⊗_

data Functor₀ : Type (lsuc ℓ₀) where
 Id : Functor₀
 Const : Type → Functor₀
 _⊕_ : Functor₀ → Functor₀ → Functor₀
 _⊗_ : Functor₀ → Functor₀ → Functor₀

[_]₀ : Functor₀ → Type → Type
[ Id ]₀ B = B
[ Const C ]₀ B = C
[ F ⊕ G ]₀ B = [ F ]₀ B ⊎ [ G ]₀ B
[ F ⊗ G ]₀ B = [ F ]₀ B × [ G ]₀ B

data Functor {ℓ : Level} : Type (lsuc ℓ) where
 Id : Functor
 Const : Type ℓ → Functor
 _⊕_ : Functor{ℓ} → Functor{ℓ} → Functor
 _⊗_ : Functor{ℓ} → Functor{ℓ} → Functor

[_]_ : Functor → Type α → Type α
[ Id ] B = B
[ Const C ] B = C
[ F ⊕ G ] B = [ F ] B ⊎ [ G ] B
[ F ⊗ G ] B = [ F ] B × [ G ] B

{- from Mimram's talk (MFPS 2021):
record Poly (I J : Type) : Type (lsuc ℓ₀) where
 field
  Op : J → Type
  Pm : (i : I) → {j : J} → Op j → Type
-}

The least fixed point of a polynomial function can then be defined in Agda with the following datatype declaration.

data μ_ (F : Functor) : Type where
 inn : [ F ] (μ F) → μ F

An important example is the polymorphic list datatype. The standard way to define this in Agda is as follows:

data list (A : Type) : Type ℓ₀ where
 [] : list A
 _∷_ : A → list A → list A

We could instead define a List datatype by applying μ to a polynomial functor L as follows:

L : {ℓ : Level}(A : Type ℓ) → Functor{ℓ}
L A = Const ⊤ ⊕ (Const A ⊗ Id)

List : (A : Type) → Type ℓ₀
List A = μ (L A)

To see some examples demonstrating that both formulations of the polymorphic list type give what we expect, see the Examples.PolynomialFunctors.Functors module. The examples will use "getter" functions, which take a list l and a natural number n and return the element of l at index n.

data Option (A : Type) : Type where
 some : A → Option A
 none : Option A

_[_] : {A : Type} → List A → ℕ → Option A
inn (inl x) [ n ] = none
inn (inr (x , xs)) [ zero ] = some x
inn (inr (x , xs)) [ suc n ] = xs [ n ]

_⟦_⟧ : {A : Type} → list A → ℕ → Option A
[] ⟦ n ⟧ = none
(x ∷ l) ⟦ zero ⟧ = some x
(x ∷ l) ⟦ suc n ⟧ = l ⟦ n ⟧

{-# WARNING_ON_USAGE Functor₀ "Use Examples.PolynomialFunctors.Functors.Functor₀ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE [_]₀     "Use Examples.PolynomialFunctors.Functors.[_]₀ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Functor  "Use Examples.PolynomialFunctors.Functors.Functor instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE [_]_     "Use Examples.PolynomialFunctors.Functors.[_]_ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE μ_       "Use Examples.PolynomialFunctors.Functors.μ_ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE L        "Use Examples.PolynomialFunctors.Functors.L instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE List     "Use Examples.PolynomialFunctors.Functors.List instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE list     "Use Examples.PolynomialFunctors.Functors.list instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Option   "Use Examples.PolynomialFunctors.Functors.Option instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE _[_]     "Use Examples.PolynomialFunctors.Functors._[_] instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE _⟦_⟧    "Use Examples.PolynomialFunctors.Functors._⟦_⟧ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Id     "Use Examples.PolynomialFunctors.Functors.Id instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Const  "Use Examples.PolynomialFunctors.Functors.Const instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE _⊕_    "Use Examples.PolynomialFunctors.Functors._⊕_ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE _⊗_    "Use Examples.PolynomialFunctors.Functors._⊗_ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE inn    "Use Examples.PolynomialFunctors.Functors.inn instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE []     "Use Examples.PolynomialFunctors.Functors.[] instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE _∷_    "Use Examples.PolynomialFunctors.Functors._∷_ instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE some   "Use Examples.PolynomialFunctors.Functors.some instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE none   "Use Examples.PolynomialFunctors.Functors.none instead.  Reclassified under #306 as illustrative content.  Removal planned one minor cycle later." #-}

---