open import Level
open import Algebra.Bundles using (Magma)
open import Relation.Binary using (Rel)
open import Function.Equality using (_⟶_) renaming (id to ⟶-id)

record Cat (o ℓ : Level) : Set (suc (o ⊔ ℓ)) where
  infix  4 _⇒_
  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    id  : ∀ {A} → A ⇒ A
    -- ...

M : Cat _ _
M = record { Obj = Magma 0ℓ 0ℓ
           ; _⇒_ = λ A B → Magma.setoid A ⟶ Magma.setoid B
           ; id  = ⟶-id
           -- ...
           } 

open Cat M

_ : ∀ {A : Magma 0ℓ 0ℓ} → A ⇒ A
_ = id   -- nope

-- __∙__27 : Algebra.Core.Op₂ (Magma.Carrier A)  [ at /Users/conal/Agda/cat-linear/src/T8.agda:24,5-7 ]
-- _∙-cong_30
--   : Algebra.Definitions.Congruent₂ (λ z z₁ → (A Magma.≈ z) z₁)
--     __∙__27  [ at /Users/conal/Agda/cat-linear/src/T8.agda:24,5-7 ]