[Agda] formalization of category theory

[Vag Vagoff]

 > record Cat (l : Level) : Set (S l) where
 >  field
 >   Ob     : Set l
 >   Arrow  : Ob → Ob → Set l
 >   id     : ∀ {o1} → (Arrow o1 o1)
 >   comp   : ∀ {o1 o2 o3} → (Arrow o2 o3) → (Arrow o1 o2) → (Arrow o1 o3)

It is more convenient to define category without mentioning objects:

record CategoryWO (Ar : Set) : Set where
     field
         _∘_ : Ar → Ar → Maybe Ar
     infix 90 _∘_
     field
         idR : ∀ f → ∃ λ g → f ∘ g ≡ just f
         idL : ∀ f → ∃ λ g → g ∘ f ≡ just f
         identity : ∀ {f g} → Ex f ∘ g → un∃ (idL g) ≡ un∃ (idR f)
         composition : ∀ {f g h} → Ex f ∘ g → Ex g ∘ h → Ex f ∘ h
         associativity : ∀ {f g h fg gh} → f ∘ g ≡ just fg → g ∘ h ≡ just gh → fg ∘ h ≡ f ∘ gh

-- or --

record CategoryWO' (Ar : Set) : Set where
     field
         _∘_ : Maybe Ar → Maybe Ar → Maybe Ar
         undefR : ∀ {f} → f ∘ nothing ≡ nothing
         undefL : ∀ {f} → nothing ∘ f ≡ nothing
     infix 90 _∘_
     field
         idR : ∀ f → ∃ λ g → f ∘ g ≡ f
         idL : ∀ f → ∃ λ g → g ∘ f ≡ f
         identity : ∀ {f g} → Ex f ∘ g → un∃ (idL g) ≡ un∃ (idR f)
         composition : ∀ {f g h} → Ex f ∘ g → Ex g ∘ h → Ex f ∘ h
         associativity : ∀ {f g h} → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)


Isn't it?
-------------- next part --------------
module Pub where

infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡· : a ≡ a
infixr 13 _⨉_ ; infixr 13 _⋕_ ; data _⨉_ (A : Set) (B : Set) : Set where _⋕_ : A → B → A ⨉ B
data ∃_ {A : Set} (P : A → Set) : Set where ∃· : ∀ {a} → P a → ∃ P
un∃ : ∀ {A} {P : A → Set} → ∃ P → A ; un∃ (∃· {a} _) = a
data Maybe (A : Set) : Set where just : A → Maybe A ; nothing : Maybe A
infix 3 Ex_ ; Ex_ : {A : Set} → Maybe A → Set ; Ex a = ∃ λ b → a ≡ just b

record CategoryWO (Ar : Set) : Set where
    field
        _∘_ : Ar → Ar → Maybe Ar
    infix 90 _∘_
    field
        idR : ∀ f → ∃ λ g → f ∘ g ≡ just f
        idL : ∀ f → ∃ λ g → g ∘ f ≡ just f
        identity : ∀ {f g} → Ex f ∘ g → un∃ (idL g) ≡ un∃ (idR f)
        composition : ∀ {f g h} → Ex f ∘ g → Ex g ∘ h → Ex f ∘ h
        associativity : ∀ {f g h fg gh} → f ∘ g ≡ just fg → g ∘ h ≡ just gh → fg ∘ h ≡ f ∘ gh

-- или --

record CategoryWO' (Ar : Set) : Set where
    field
        _∘_ : Maybe Ar → Maybe Ar → Maybe Ar
        undefR : ∀ {f} → f ∘ nothing ≡ nothing
        undefL : ∀ {f} → nothing ∘ f ≡ nothing
    infix 90 _∘_
    field
        idR : ∀ f → ∃ λ g → f ∘ g ≡ f
        idL : ∀ f → ∃ λ g → g ∘ f ≡ f
        identity : ∀ {f g} → Ex f ∘ g → un∃ (idL g) ≡ un∃ (idR f)
        composition : ∀ {f g h} → Ex f ∘ g → Ex g ∘ h → Ex f ∘ h
        associativity : ∀ {f g h} → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)