Mercurial > hg > Members > kono > Proof > category
comparison monoid-monad.agda @ 781:340708e8d54f
fix for 2.5.4.2
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 08 Mar 2019 17:46:59 +0900 |
parents | 60942538dc41 |
children | bded2347efa4 |
comparison
equal
deleted
inserted
replaced
780:b44c1c6ce646 | 781:340708e8d54f |
---|---|
12 open import Relation.Binary.Core | 12 open import Relation.Binary.Core |
13 open import Relation.Binary | 13 open import Relation.Binary |
14 | 14 |
15 -- open Monoid | 15 -- open Monoid |
16 open import Algebra.FunctionProperties using (Op₁; Op₂) | 16 open import Algebra.FunctionProperties using (Op₁; Op₂) |
17 | |
18 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) | |
17 | 19 |
18 | 20 |
19 record ≡-Monoid c : Set (suc c) where | 21 record ≡-Monoid c : Set (suc c) where |
20 infixl 7 _∙_ | 22 infixl 7 _∙_ |
21 field | 23 field |