Mercurial > hg > Members > kono > Proof > category
diff 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 |
line wrap: on
line diff
--- a/monoid-monad.agda Mon Oct 08 16:48:27 2018 +0900 +++ b/monoid-monad.agda Fri Mar 08 17:46:59 2019 +0900 @@ -15,6 +15,8 @@ -- open Monoid open import Algebra.FunctionProperties using (Op₁; Op₂) +open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) + record ≡-Monoid c : Set (suc c) where infixl 7 _∙_