Agda 中集合和函数类别的简单编码

Question

这是一个关于 Agda 和范畴论的非常基础的问题。我想编码一个类别，其中对象是有限集，箭头是它们之间的函数。我正在为 Category 定义使用 agda/agda-categories 存储库。我在关卡方面遇到了麻烦。这是当前的 WIP 代码：

-- | 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-≈ = {!!}
    }

我在 0 洞中的 Goal/Have 不匹配是这个：

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

一定是我在关卡方面做的不对，或者可能是对应该如何编码等式的完全误解。

带有我的 WIP 代码的 Repo 在这里：https://github.com/k-bx/category-theory-exercises/blob/master/agda/ex02_noninjective_functions.agda

Answer 1

好吧，我刚刚意识到答案可能是我们想声明级别 ℓ 和 e 对这个类别来说是相等的，所以这个有效：

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-≈ = {!!}
    }

Agda 中集合和函数类别的简单编码

Simple encoding of category of sets and functions in Agda

agda

category-theory