Простое кодирование категории множеств и функций в Agda - PullRequest
Новая
       25

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

0 голосов
/ 20 июня 2019

Это очень простой вопрос об Agda и теории категорий. Я хочу закодировать категорию, где объекты - это конечные множества, а стрелки - это функции между ними. Я использую agda / agda-category репо для определения 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

1 Ответ

1 голос
/ 20 июня 2019

Хорошо, я только что понял, что ответ может быть таким: мы хотим заявить, что уровни ℓ и 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-≈ = {!!}
    }
...