↑ Top


Functors

This is the 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:

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),

{-# OPTIONS --without-K --exact-split --safe #-}

module Categories.Functors where

-- Imports from Agda and the Agda Standard Library  ---------------------------------------
open import Agda.Primitive using ( _⊔_ ; lsuc ; Level ) renaming ( Set to Type ; lzero to ℓ₀ )
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

private variable
 α β : Level

infixl 6 _⊕_
infixr 7 _⊗_
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.Categories.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. (Since such an element doesn’t always exist, we first define the Option type.)

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 


↑ Categories Complexity →