Definition of a category as an Agda record: level polymorphic in the objects and arrows

Category.agda

module Category where

open import Agda.Primitive public
  using (Level ; _⊔_ ; lzero ; lsuc)

open import Agda.Builtin.Equality public
  using (_≡_ ; refl)


record Category ℓ ℓ′ : Set (lsuc (ℓ ⊔ ℓ′)) where
  field
    World   : Set ℓ
    _►_     : World → World → Set ℓ′
    ►-refl  : ∀ {w} → w ► w
    ►-trans : ∀ {w w′ w″} → w″ ► w′ → w′ ► w → w″ ► w
    ►-id₁   : ∀ {w w′} → (a : w′ ► w) → ►-trans ►-refl a ≡ a
    ►-id₂   : ∀ {w w′} → (a : w′ ► w) → ►-trans a ►-refl ≡ a
    ►-assoc : ∀ {w w′ w″ w‴} → (a″ : w‴ ► w″) (a′ : w″ ► w′) (a : w′ ► w) →
                ►-trans a″ (►-trans a′ a) ≡ ►-trans (►-trans a″ a′) a

  id : ∀ {w} → w ► w
  id = ►-refl

  infixr 9 _∘_
  _∘_ : ∀ {w w′ w″} → w′ ► w → w″ ► w′ → w″ ► w
  f ∘ g = ►-trans g f

open Category {{…}} public


instance
  cat-Set-→ : ∀ {ℓ} → Category (lsuc ℓ) ℓ
  cat-Set-→ {ℓ} = record
    { World   = Set ℓ
    ; _►_     = λ X Y → X → Y
    ; ►-refl  = λ x → x
    ; ►-trans = λ f g x → g (f x)
    ; ►-id₁   = λ f → refl
    ; ►-id₂   = λ f → refl
    ; ►-assoc = λ f g h → refl
    }


infixl 5 _,_
record Σ {ℓ ℓ′} (X : Set ℓ) (P : X → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  instance
    constructor _,_
  field
    π₁ : X
    π₂ : P π₁

infixl 2 _∧_
_∧_ : ∀ {ℓ ℓ′} → Set ℓ → Set ℓ′ → Set (ℓ ⊔ ℓ′)
X ∧ Y = Σ X (λ x → Y)

infix 3 _↔_
_↔_ : ∀ {ℓ ℓ′} → (X : Set ℓ) (Y : Set ℓ′) → Set (ℓ ⊔ ℓ′)
X ↔ Y = (X → Y) ∧ (Y → X)

cong² : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} {x y x′ y′} →
          (f : X → Y → Z) → x ≡ x′ → y ≡ y′ →
          f x y ≡ f x′ y′
cong² f refl refl = refl

instance
  cat-Set-↔ : ∀ {ℓ} → Category (lsuc ℓ) ℓ
  cat-Set-↔ {ℓ} = record
    { World   = Set ℓ
    ; _►_     = _↔_
    ; ►-refl  = ►-refl , ►-refl
    ; ►-trans = λ { (f , f⁻¹) (g , g⁻¹) → ►-trans f g , ►-trans g⁻¹ f⁻¹ }
    ; ►-id₁   = λ { (f , f⁻¹) → cong² _,_ refl refl }
    ; ►-id₂   = λ { (f , f⁻¹) → cong² _,_ refl refl }
    ; ►-assoc = λ { (f , f⁻¹) (g , g⁻¹) (h , h⁻¹) → cong² _,_ refl refl }
    }