Простое кодирование категории наборов и функций в Agda

Это очень простой вопрос по Agda и теории категорий. Я хочу закодировать категорию, в которой объекты представляют собой конечные множества, а стрелки - функции между ними. Я использую репозиторий agda / agda-Categories для определения Category. У меня проблемы с уровнями. Вот текущий код 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: 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 находится здесь: https://github.com/k-bx/category-theory-exercises/blob/master/agda/ex02_noninjective_functions.agda


category-theory agda
person Konstantine Rybnikov    schedule 20.06.2019    source источник
comment
В вашем понимании стрелок полностью игнорируются исходный и целевой типы. Наверное, это неправильно.   -  person gallais    schedule 20.06.2019
comment
@gallais, что плохого в том, чтобы их игнорировать? В этом примере все стрелки относятся к одним и тем же типам констант, иногда это даже более тривиально, например, когда я заключил моноид как категорию k-bx.github.io/articles/boring-monoid-category.html Или я здесь не прав?   -  person Konstantine Rybnikov    schedule 20.06.2019
comment
Вообще-то, извините, я понимаю вашу точку зрения. AnyFiniteSetFunc может потребоваться дополнительная параметризация, мы подумаем об этом.   -  person Konstantine Rybnikov    schedule 20.06.2019

Ответы (1)


arrow_upward
2
arrow_downward

Хорошо, я только что понял, что ответ может заключаться в том, что мы хотим заявить, что уровни ℓ и 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-≈ = {!!}
    }
person Konstantine Rybnikov    schedule 20.06.2019