Categories.agda

module Categories where

open import Level

open import Function hiding (id; _∘_)

open import Data.List
open import Data.Bool
open import Data.Product

open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality

record category
  {ℓ⁰ ℓ¹ ℓ² : Level}
  (v⁰ : Set ℓ⁰)
  (v¹ : Rel v⁰ ℓ¹)
  (v² : ∀ {x y : v⁰} → Rel (v¹ x y) ℓ²)
  : Set (suc (ℓ⁰ ⊔ ℓ¹ ⊔ ℓ²))

record equivalence
  {ℓ⁰ ℓ¹ ℓ²}
  {* : Set ℓ⁰}
  {_⇒¹_ : Rel * ℓ¹}
  {_⇒²_ : ∀ {x y : *} → Rel (x ⇒¹ y) ℓ²}
  (c : category {ℓ⁰} {ℓ¹} {ℓ²} * (_⇒¹_) (_⇒²_))
  (x y : *)
  : Set (suc (ℓ⁰ ⊔ ℓ¹ ⊔ ℓ²))

_⟪_⟫_ : ∀
  {ℓ⁰ ℓ¹ ℓ²}
  {v⁰ : Set ℓ⁰}
  {v¹ : Rel v⁰ ℓ¹}
  {v² : ∀ {x y : v⁰} → Rel (v¹ x y) ℓ²}
  → v⁰
  → category {ℓ⁰} {ℓ¹} {ℓ²} v⁰ v¹ v²
  → v⁰
  → Set (suc (ℓ⁰ ⊔ ℓ¹ ⊔ ℓ²))
f ⟪ c ⟫ g = equivalence c f g

record category {ℓ⁰} {ℓ¹} {ℓ²} v⁰ v¹ v²
  where
  coinductive

  infix 4 _⇒_ _⇒¹_ _⇒²_
  infixr 9 _∘_

  * : Set ℓ⁰
  * = v⁰

  _⇒¹_ : Rel * ℓ¹
  _⇒¹_ = v¹

  _⇒_ : Rel * ℓ¹
  _⇒_ = v¹

  _⇒²_ : ∀ {x y : *} → Rel (x ⇒ y) ℓ²
  _⇒²_ = v²

  field
    id : ∀ {x} → x ⇒ x
    _∘_ : ∀ {x y z} → y ⇒ z → x ⇒ y → x ⇒ z

  field
    _⇒³_ : ∀ {x y : *} {f g : x ⇒ y} → Rel (f ⇒² g) ℓ²
    -- TODO:                         Should this be ℓ³ here instead?
    --     | What would the requisite change to (suc (ℓ⁰ ⊔ ℓ¹ ⊔ ℓ²)) be?
    depths : ∀ {x y : *} →
      (category (x ⇒ y) (_⇒²_) (_⇒³_))

  field
    law-idˡ : ∀ {x y} {f : x ⇒ y} → (id ∘ f) ⟪ depths ⟫ f
    law-idʳ : ∀ {x y} {f : x ⇒ y} → (f ∘ id) ⟪ depths ⟫ f
    law-assoc : ∀ {a b c d} {f : c ⇒ d} {g : b ⇒ c} {h : a ⇒ b} → ((f ∘ g) ∘ h) ⟪ depths ⟫ (f ∘ g ∘ h)

record equivalence {ℓ⁰} {ℓ¹} {ℓ²} c x y
  where
  coinductive

  module C = category c
  open C
  field
    f : x ⇒¹ y
    g : y ⇒¹ x
    equivˡ : (f ∘ g) ⟪ depths ⟫ id
    equivʳ : (g ∘ f) ⟪ depths ⟫ id

instance
  {-# TERMINATING #-}
  ≡-category : ∀ {a : Set} → category a (_≡_) (_≡_)
  ≡-category = record
    { id = refl
    ; _∘_ = λ { refl refl → refl }
    ; _⇒³_ = _≡_
    ; depths = ≡-category
    ; law-idˡ = record
      { f = {!   !}
      ; g = {!   !}
      ; equivˡ = {!   !}
      ; equivʳ = {!   !}
      }
    ; law-idʳ = record
      { f = {!   !}
      ; g = {!   !}
      ; equivˡ = {!   !}
      ; equivʳ = {!   !}
      }
    ; law-assoc = record
      { f = {!   !}
      ; g = {!   !}
      ; equivˡ = {!   !}
      ; equivʳ = {!   !}
      }
    }