[Agda] Size of propositional equality?

[Alan Jeffrey]

On 12/17/2010 02:33 AM, Nils Anders Danielsson wrote:
> On 2010-12-16 19:23, Alan Jeffrey wrote:
>> I'm sure there's a good reason for this change, any hints what it
>> might be?
>
> The small variant of _≡_ is accepted by Agda, but perhaps it shouldn't
> be—several persons are sceptical about this. Propositional equality is a
> rather important type, so I decided to switch to a more conservative
> definition.

Is the skepticism a general one about sets being indexed by a set from a 
larger universe, or is it specific to propositional equality?

I've patched my code essentially by reintroducing the small version of 
_≡_, which is a bit annoying as it means I have two propositional 
equalities in scope, a large one supporting equational reasoning, 
rewrite, etc, and a small one just for cardinality reasons.

A.