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

record Category {o m e} : Set ( suc ( o  ⊔  m ⊔ e )  ) where
  infix 4 _⇛_ _≡_
  infixr 9 _∘_
  field
    Obj : Set o
    _⇛_ : Rel Obj m
    _≡_ : ∀ {A B} -> Rel (A ⇛ B ) e
    id : ∀ {x} ->  x ⇛  x
    _∘_ : ∀ {a b c : Obj} -> (b ⇛ c) -> (a ⇛ b) -> (a ⇛ c )


data TrivMorph {o}  (obj : Set o) : obj -> obj -> Set (suc o) where
  idM : ∀ {x} -> TrivMorph obj x x

data TrivEquiv {i l} (obj : Set i) (morph : Rel obj l) {dom cod : obj}  : morph dom cod -> morph dom cod -> Set (i ⊔ suc l )  where
  idE : forall {x} -> TrivEquiv obj morph  x x

trivEqSimple :  ∀  {i l}  {obj : Set i}  {dom cod : obj} {morph : Rel obj l }  {f g  h : morph cod dom } -> TrivEquiv obj morph   f g
  -> TrivEquiv obj morph g h -> TrivEquiv obj morph f h
trivEqSimple   idE idE = idE

trivMorphSimpleComp : forall {o} {obj : Set o} {a b c : obj} -> TrivMorph obj b c -> TrivMorph obj a b -> TrivMorph obj a c
trivMorphSimpleComp  idM idM = idM


trivCat : forall {o }  (obj : Set o) -> Category {o}
trivCat obj = record  {Obj = obj
                   ; _⇛_ = TrivMorph obj
                   ; _≡_ = TrivEquiv obj (TrivMorph obj)
                   ; id = idM
                   ; _∘_ = trivMorphSimpleComp  }