CODEWITHSUNDEEP
agdacategory-theory
Kostia R
Kostia R

Reputation: 2565

Simple encoding of category of sets and functions in Agda

This is a very basic question on Agda and Category Theory. I want to encode a category where objects are finite sets and arrows are functions between them. I'm using the agda/agda-categories repo for Category definition. I'm having trouble with levels. Here's the current WIP code:

-- | Category Theory by Steve Awodey
--
-- Page 6. Book mentions injective functions, but just to clarify we
-- will confirm that non-injective functions work just as well.
--

open import Algebra
open import Function using (_∘_)
open import Algebra.Structures
open import Categories.Category
open import Level
open import Relation.Binary.Core
open import Agda.Builtin.Equality

data FiniteSet (o : Level) : Set o where
  MkFiniteSet1 : FiniteSet o
  MkFiniteSet2 : FiniteSet o

record AnyFiniteSetFunc (ℓ : Level) : Set ℓ where
  constructor MkAnyFiniteSetFunc
  field
    func : (FiniteSet ℓ → FiniteSet ℓ)

noninjCat : {o ℓ e : Level} → Category o ℓ e
noninjCat {o} {ℓ} {e} =
  record
    { Obj = FiniteSet o
    ; _⇒_ = λ _ _ → AnyFiniteSetFunc ℓ
    ; _≈_ = λ x₂ x₁ → {!(_≡_) x₁ x₂!}
    ; id = MkAnyFiniteSetFunc (\(el : FiniteSet ℓ) → el)
    ; _∘_ = λ f1 f2 →
            MkAnyFiniteSetFunc
              ( AnyFiniteSetFunc.func f1
              ∘ AnyFiniteSetFunc.func f2
              )
    ; assoc = λ {A} {B} {C} {D} {f} {g} {h} → {!!}
    ; identityˡ = {!!}
    ; identityʳ = {!!}
    ; equiv = {!!}
    ; ∘-resp-≈ = {!!}
    }

The Goal/Have mismatch I have in hole 0 is this one:

Goal: Set e
Have: Set ℓ
————————————————————————————————————————————————————————————
x₁ : AnyFiniteSetFunc ℓ
x₂ : AnyFiniteSetFunc ℓ
B  : FiniteSet o  (not in scope)
A  : FiniteSet o  (not in scope)
e  : Level
ℓ  : Level
o  : Level

There must be something I'm not doing right with levels there, or maybe a complete mis-conception of how the equality should be encoded.

Repo with my WIP code is here: https://github.com/k-bx/category-theory-exercises/blob/master/agda/ex02_noninjective_functions.agda

Upvotes: 1

Views: 181

Answers (1)

Kostia R
Kostia R

Reputation: 2565

Ok, I've just realized the answer might be that we want to state that levels ℓ and e are equal for this category, so this worked:

noninjCat : {o ℓ : Level} → Category o ℓ ℓ
noninjCat {o} {ℓ} =
  record
    { Obj = FiniteSet o
    ; _⇒_ = λ _ _ → AnyFiniteSetFunc ℓ
    ; _≈_ = λ {A} {B} x₂ x₁ → x₁ ≡ x₂
    ; id = MkAnyFiniteSetFunc (\(el : FiniteSet ℓ) → el)
    ; _∘_ = λ f1 f2 →
            MkAnyFiniteSetFunc
              ( AnyFiniteSetFunc.func f1
              ∘ AnyFiniteSetFunc.func f2
              )
    ; assoc = λ {A} {B} {C} {D} {f} {g} {h} → {!!}
    ; identityˡ = {!!}
    ; identityʳ = {!!}
    ; equiv = {!!}
    ; ∘-resp-≈ = {!!}
    }

Upvotes: 2

Related Questions