```{-# 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 6 _~>_
infix 2 _≈_

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 2 _[_≈_]
_[_≈_] : (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 5 _[_,_]
_[_,_] : (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 5 _[_∘_]
_[_∘_] : (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 5 _[_>>_]
_[_>>_] : (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

```