gistfile1.txt

record Category (k : Set → Set → Set) : Set₁ where
  infixr 8 _⇝_
  _⇝_ : Set → Set → Set
  _⇝_ = k
  field
    id : ∀ {x} → x ⇝ x
    _∘_ : ∀ {a b c : Set} → (b ⇝ c) → (a ⇝ b) → (a ⇝ c)
  
    unitalityˡ : ∀ {X Y} {f : X ⇝ Y} → id ∘ f ≡ f
    unitalityʳ : ∀ {X Y} {f : X ⇝ Y} → f ∘ id ≡ f

    associativity : ∀ {X Y Z W} {f : X ⇝ Y} {g : Y ⇝ Z} {h : Z ⇝ W}
                  → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f



module _ (_⇝_ : Set → Set → Set) (let infixl 5 _⇝_; _⇝_ = _⇝_) where
  record Category : Set₁ where
    field
      id : ∀ {x} → x ⇝ x
      _∘_ : ∀ {a b c : Set} → (b ⇝ c) → (a ⇝ b) → (a ⇝ c)
    
      unitalityˡ : ∀ {X Y} {f : X ⇝ Y} → id ∘ f ≡ f
      unitalityʳ : ∀ {X Y} {f : X ⇝ Y} → f ∘ id ≡ f

      associativity : ∀ {X Y Z W} {f : X ⇝ Y} {g : Y ⇝ Z} {h : Z ⇝ W}
                    → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f