圏

module category-theory.category where

open import foundations.universe
open import foundations.identity-type
open import foundations.set

データと条件を分けて定義した方がなにかと都合がよい。

record CategoryData o h : Type (lsuc o ⊔ lsuc h) where
  field
    Ob : Type o
    Hom : ∀ (A B : Ob) → Type h

    id : ∀ A → Hom A A
    _∘_ : ∀ {A B C : Ob} → (g : Hom B C) → (f : Hom A B) → Hom A C

  infix  _∘_

record isCategory {o h} (𝒞 : CategoryData o h) : Type (o ⊔ h) where
  open CategoryData 𝒞

  field
    identˡ : ∀ {A B} (f : Hom A B) → id B ∘ f ＝ f
    identʳ : ∀ {A B} (f : Hom A B) → f ∘ id A ＝ f
    ident² : ∀ A → id A ∘ id A ＝ id A

    assoc : ∀ {A B C D} {f : Hom A B} {g} {h : Hom C D}
      → (h ∘ g) ∘ f ＝ h ∘ (g ∘ f)
    sym-assoc : ∀ {A B C D} {f : Hom A B} {g} {h : Hom C D}
      → h ∘ (g ∘ f) ＝ (h ∘ g) ∘ f

    is-set-hom : ∀ {A B} → isSet (Hom A B)

record Category o h : Type (lsuc o ⊔ lsuc h) where
  field
    𝒞 : CategoryData o h
    is-category : isCategory 𝒞

  open CategoryData 𝒞 public
  open isCategory is-category public

private variable o h : Level

oppositeCat : Category o h → Category o h
oppositeCat 𝒞 = record
  { 𝒞 = record
    { Ob = Ob
    ; Hom = λ A B → Hom B A
    ; id = id
    ; _∘_ = λ g f → f ∘ g
    }
  ; is-category = record
    { identˡ = identʳ
    ; identʳ = identˡ
    ; ident² = ident²
    ; assoc = sym-assoc
    ; sym-assoc = assoc
    ; is-set-hom = is-set-hom
    }
  }
  where
    open Category 𝒞

反対圏の反対圏は、元々の圏と定義的に等しい。

private variable 𝒞 : Category o h

_ : oppositeCat (oppositeCat 𝒞) ＝ 𝒞
_ = refl