drop the Function.Equality requirement from GetTypes
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 9 Jun 2015 14:09:37 +0000 (16:09 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Tue, 9 Jun 2015 14:09:37 +0000 (16:09 +0200)
commitdbad09a8a5843e91f862657c3011ec7f63ea819b
tree4e94ce24ca4b9dcaad1378576d1352caf8209de7
parent94f6fbed8b04e95446c38d6ea89dcc9c3a64304b
drop the Function.Equality requirement from GetTypes

We never used the equality property. Thus a simple function is
sufficient here. We always fulfilled the property using ≡-to-Π anyway.
BFFPlug.agda
Examples.agda
FreeTheorems.agda
GetTypes.agda