{-# OPTIONS --type-in-type #-}

module Categories where

open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as SetoidR

record Category : Set where
  infix  _~>_
  infix  _≈_

  field
    -- Objects and arrows in the category
    Obj : Set
    _~>_ : (A B : Obj) → Set

    -- The meaning of equality of morphisms
    _≈_
      : {A B : Obj}
      → A ~> B
      → A ~> B
      → Set

    -- _≈_ forms a equivalence relationship
    ≈-equiv : {A B : Obj} → IsEquivalence (_≈_ {A} {B})

    -- Id and composition
    id : {A : Obj} → A ~> A
    _∘_ : {A B C : Obj} → B ~> C → A ~> B → A ~> C

    ∘-cong
        : ∀ {A B C} {g g' : B ~> C} {f f' : A ~> B}
        → g ≈ g'
        → f ≈ f'
        → g ∘ f ≈ g' ∘ f'

    -- Laws
    id-r : {A B : Obj} (f : A ~> B) → f ∘ id ≈ f
    id-l : {A B : Obj} (f : A ~> B) → id ∘ f ≈ f
    ∘-assoc
      : {A B C D : Obj}
      → (h : C ~> D)
      → (g : B ~> C)
      → (f : A ~> B)
      → h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f

  -- "Forward" composition
  _>>_ : {A B C : Obj} → A ~> B → B ~> C → A ~> C
  _>>_ f g = g ∘ f

  >>-assoc
      : {A B C D : Obj}
      → (f : A ~> B)
      → (g : B ~> C)
      → (h : C ~> D)
      → f >> (g >> h) ≈ (f >> g) >> h
  >>-assoc f g h = IsEquivalence.sym ≈-equiv (∘-assoc h g f)

  setoid : {X Y : Obj} → Setoid _ _
  Setoid.Carrier (setoid {X} {Y}) = X ~> Y
  Setoid._≈_ setoid  = _≈_
  Setoid.isEquivalence setoid = ≈-equiv

  module HomReasoning {A B : Obj} where
    open SetoidR (setoid {A} {B}) public
    open IsEquivalence (≈-equiv {A} {B}) public

module _ where
  open Category


  infix  _[_≈_]
  _[_≈_] : (r : Category) {A B : Obj r} → (r ~> A) B → (r ~> A) B → Set
  _[_≈_] = _≈_

  -- Notational convenience for arrows in a category. Helpful when dealing with
  -- multiple categories at once.
  -- eg we can talk about a set arrow via `SET [ Bool , Int ]`
  infix  _[_,_]
  _[_,_] : (C : Category) -> Obj C -> Obj C -> Set
  C [ X , Y ] = _~>_ C X Y

  -- Notational convenience for composition.
  -- eg we can talk about a set composition `SET [ show ∘ length ] : SET [ List A , String ]`
  infix  _[_∘_]
  _[_∘_] : (C : Category) -> {X Y Z : Obj C} -> C [ Y , Z ] -> C [ X , Y ] -> C [ X , Z ]
  _[_∘_] = _∘_

  -- Notational convenience for "forward" composition.
  -- eg we can talk about a set composition `SET [ length >> show ] : SET [ List A , String ]`
  infix  _[_>>_]
  _[_>>_] : (C : Category) -> {X Y Z : Obj C} -> C [ X , Y ] -> C [ Y , Z ] -> C [ X , Z ]
  _[_>>_] = _>>_

module _ (C : Category) where
  open Category C
  record HasTerminal : Set where
    field
      terminal : Obj
      term-arr
          : (A : Obj)
          → A ~> terminal
      term-unique
          : {A : Obj}
          → (f : A ~> terminal)
          → f ≈ term-arr A