Mercurial > hg > Members > kono > Proof > category

diff applicative.agda @ 783:bded2347efa4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CCC by equation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 17 Apr 2019 12:03:45 +0900
parents 06388660995b
children dca4b29553cb
line wrap: on
line diff
--- a/applicative.agda	Fri Mar 08 18:09:11 2019 +0900
+++ b/applicative.agda	Wed Apr 17 12:03:45 2019 +0900
@@ -9,6 +9,7 @@
 open import Relation.Binary.Core
 open import Relation.Binary
 open import monoidal
+open import Relation.Binary.PropositionalEquality  hiding ( [_] )
 
 -----
 --