↑ Top


Examples of Functors

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


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

module Examples.Categories.Functors where

open import Agda.Primitive using ( lsuc ) 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 Level
open import Data.Unit      using () renaming ( tt to 𝟎 )
open import Relation.Binary.PropositionalEquality  using ( _≡_ ; refl ; _≢_ )

open import Base.Categories.Functors using ( List ; list ; _⟦_⟧ ; _[_] ; μ_ ; Option )

open μ_
open list

-- Examples
-- 1. Empty list
L₀ : List 
L₀ = inn (inl (Level.lift 𝟎))

l₀ : list 
l₀ = []


-- 2. One-element list, (3)
L₁ : List 
L₁ = inn (inr (3 , L₀))

l₁ : list 
l₁ = 3  l₀



-- 2. Three-element list, (1, 2, 3)
L₃ : List 
L₃ = inn (inr (1 , (inn (inr (2 , L₀)))))

l₃ : list 
l₃ = 1  (2  l₁)

open Option

L₀≡none :  {n}  (L₀ [ n ])  none
L₀≡none = refl

l₀≡none :  {n}  (l₀  n )  none
l₀≡none = refl


L₁[0]≡some3 : L₁ [ 0 ]  some 3
L₁[0]≡some3 = refl

l₁⟦0⟧≡some3 : l₁  0   some 3
l₁⟦0⟧≡some3 = refl


L₁[n>0]≡none :  n  n > 0  L₁ [ n ]  none
L₁[n>0]≡none (suc n) _ = refl

l₁⟦n>0⟧≡none :  n  n > 0  l₁  n   none
l₁⟦n>0⟧≡none (suc n) _ = refl


L₃[0]≡some1 : L₃ [ 0 ]  some 1
L₃[0]≡some1 = refl

l₃⟦0⟧≡some1 : l₃  0   some 1
l₃⟦0⟧≡some1 = refl


L₃[0]≢some2 : L₃ [ 0 ]  some 2
L₃[0]≢some2 = λ ()

l₃[0]≢some2 : l₃  0   some 2
l₃[0]≢some2 = λ ()

ℓ₁ : Level
ℓ₁ = lsuc ℓ₀