[Agda] RFC: R.B.HeterogeneousEquality + i-cong

Helmut Grohne grohne at cs.uni-bonn.de
Wed Feb 5 08:59:55 CET 2014


On Wed, Feb 05, 2014 at 08:24:23AM +0100, Ulf Norell wrote:
> I would make X and Y implicit. That's in line with the other cong functions
> and as you say, they can often be inferred.

I'm sorry, but that doesn't work. At the very least X must be explicit
(like P is explicit for subst). The question was only about Y.

Helmut


More information about the Agda mailing list