Categories in Agda

Category.agda

open import Level
module Category {o ℓ e : Level}  where

open import Relation.Binary using (Rel; IsEquivalence; module IsEquivalence; Reflexive; Symmetric; Transitive) renaming (_⇒_ to _⊆_)


-- Definition of a category.
-- From https://github.com/copumpkin/categories/blob/master/Categories/Category.agda
record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where

  infix  4 _≡_
  infix  5 _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ  -- Rel is in Relation.Binary.Core
    {_≡_} : ∀ {A B} → Rel (A ⇒ B) e

    {id}  : ∀ {A} → (A ⇒ A)
    {_∘_} : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    .{assoc}     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
    .{identityˡ} : ∀ {A B} {f : A ⇒ B} → id ∘ f ≡ f
    .{identityʳ} : ∀ {A B} {f : A ⇒ B} → f ∘ id ≡ f
    .{equiv}     : ∀ {A B} → IsEquivalence (_≡_ {A} {B})
    .{∘-resp-≡}  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≡ h → g ≡ i → f ∘ g ≡ h ∘ i


-- Examples

-- Category with one object.

-- From https://github.com/copumpkin/categories/blob/master/Categories/Terminal.agda
-- A set with one element.
{-
XXX: Why not define it as data?
-}
record Unit {x : _} : Set x where
  constructor unit

OneC : Category o ℓ e
OneC = record
  { Obj       = Obj        -- Unit
  ; _⇒_       = _⇒_        -- λ _ _ → Unit
  ; _≡_       = _≡_        -- λ _ _ → Unit
  ; id        = id         -- unit
  ; _∘_       = _∘_        -- λ _ _ → unit
  ; assoc     = assoc      -- unit
  ; identityˡ = identityˡ  -- unit
  ; identityʳ = unit
  ; equiv = record
    { refl  = unit
    ; sym   = λ _ → unit
    ; trans = λ _ _ → unit
    }
  ; ∘-resp-≡ = λ _ _ → unit
  }
  where
    infix  4 _≡_
    infix  5 _⇒_
    infixr 9 _∘_

    Obj : Set _
    Obj = Unit

    _⇒_ : Obj → Obj → Set _  -- Rel Obj ℓ
    unit ⇒ unit = Unit

    _≡_ : Rel (unit ⇒ unit) e
    unit ≡ unit = Unit

    id : unit ⇒ unit
    id = unit

    _∘_ : (unit ⇒ unit) → (unit ⇒ unit) → (unit ⇒ unit)
    unit ∘ unit = unit

    -- XXX
    assoc : ((unit ⇒ unit) ∘ (unit ⇒ unit)) ∘ (unit ⇒ unit)
          ≡ (unit ⇒ unit) ∘ ((unit ⇒ unit) ∘ (unit ⇒ unit))
    assoc = unit

    -- XXX
    identityˡ : id ∘ (unit ⇒ unit) ≡ (unit ⇒ unit)
    identityˡ = unit


-- Category with two objects.
-- A set with two elements.
data Bool {x : _} : Set x where
  true false : Bool

data ⊥ {x : _} : Set x where

-- XXX: Try to express TwoC as TwoC OneC_1 OneC_2.
{-
TwoC : Category o ℓ e
TwoC = record
  { Obj = Obj
  -- Basic Relations
  -- https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Base.agda
  ; _⇒_ = _⇒_
  ; _≡_ =  {! !}
  ; _∘_ = {! !}
  ; id =  {! !}
  ; assoc = {! !}
  ; identityˡ = {! !}
  ; identityʳ =  {! !}
  ; equiv = record
    { refl =  {! !}
    ; sym =  {! !}
    ; trans =  {! !}
    }
  ; ∘-resp-≡ =  {! !}
  }
  where
    Obj : Set _
    Obj = Bool

    _⇒_ : Obj → Obj → Set _
    true  ⇒ false = Unit  -- there's a single arrow from true to false
    true  ⇒ true  = Unit  -- identity arrows
    false ⇒ false = Unit
    _     ⇒ _     = ⊥     -- there are no other arrows
-}