[Agda] Why is propositional equality "Set a" instead of just Set?
jleivent at comcast.net
Mon Aug 19 21:33:52 CEST 2013
On 08/19/2013 01:13 PM, Wolfram Kahl wrote:
> The next question then is:
> How does this come out as a special case from an appropriate general
> rule for parameterised and indexed inductive datatypes?
Can the question be broken into two parts - a practical and a
theoretical part? The practical part is: what safe but possibly
restrictive general rule can be adopted (and put into the type checker
as a default, maybe?) as an interim solution. The least (or lesser)
restrictive "appropriate general" rule would be the theoretical question.
More information about the Agda