9 lines
194 B
Plaintext
9 lines
194 B
Plaintext
record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
|
||
infixl 7 _∙_
|
||
infix 4 _≈_
|
||
field
|
||
Carrier : Set c
|
||
_≈_ : Rel Carrier ℓ
|
||
_b_ : Op Carrier
|
||
a : Carrier
|