module T where

open import Agda.Primitive
open import Agda.Builtin.Equality

record Category : Set (lsuc lzero) where
  field
    Object : Set
    Arrow  : Object → Object → Set
    𝟙      : {o : Object} → Arrow o o
    _⊕_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c

record Functor (ℂ : Category) (𝔻 : Category) : Set where
  open Category
  field
    func* : ℂ .Object → 𝔻 .Object
    func→ : {dom cod : ℂ .Object}
      → ℂ .Arrow dom cod → 𝔻 .Arrow (func* dom) (func* cod)
    distrib : {A B C : ℂ .Object} {g : ℂ .Arrow B C} {f : ℂ .Arrow A B}
      → func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)