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 ℓ₀