[Agda] Why is propositional equality "Set a" instead of just Set?

[Andreas Abel]

Putting propositional equality in a lower universe than the type it 
speaks about is at least problematic when you want to construct a PER 
model of type theory predicatively.

Usually you have a rule like

   a = b : A
   -----------------------
   refl : _==_ {A = A} a b

thus, you need to know the semantics of A before you can define the 
semantics of _==_ {A = A}, i.e., before you can define the proofs of 
equality of elements of type A.

Now if you allow equality to be in a lower universe than the type it 
refers to, say

   A : Set 1
   -----------------------
   _==_ {A = A} : Set 0

then I do not see a direct way to define the universes Set n by 
induction on n (since you need to know Set 1 before you can define Set 
0, and vice versa).

Frankly, I have not encountered a model of type theory that would allow 
generalized _==_; if you find one, let me know, I'd like to study it.

Best,
Andreas

On 18.08.13 4:49 PM, Jonathan Leivent wrote:
> On 08/17/2013 11:56 PM, Wolfram Kahl wrote:
>> We define a fully |Level|-polymorphic variant of propositional equality
>> in order to be able to define fully |Level|-polymorphic identity
>> relations.
>> (Thorsten Altenkirch%
>> \footnote{at AIM XIII, April 2011}
>>   and others
>>   have expressed reservations whether such a definition
>>   at levels |k| lower than |a| should be legal.)
>>
>> \begin{code}
>>    data _≡≡_  {k a : Level} {A : Set a} (x : A) : A → Set k where
>>      ≡≡-refl : x ≡≡ x
>> \end{code}
>> ----------------------------------------------------------------------------

>
> I didn't expect a controversial aspect of type theory to turn up in such
> a ubiquitous case.  I was just basing my level assignments on the
> constraints that the type checker finds.
>
> Is there some expectation as to what legal behavior Agda would
> eventually adopt?  Would every definition have to have a level at least
> as high as all of its parameters/indexes?


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/