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

[Dan Licata]

The impredicativity also shows up if you have function extensionality or
univalence.  E.g.

Set0 -> Set0 : Set1

so if equality is always in Set0, then

_==_{Set0 -> Set0} A B : Set0

But by function extensionality, A == B is equivalent to 

(X : Set0) -> A X =={Set0} B X

So now there is a type in Set0 equivalent to a Pi whose domain is Set0, 
which seems fishy on predicative grounds.  

With univalence, you could
smuggle any bijection at any size into Set0.  
But then equality is no longer a "proposition", so it's a different
setting than the original question asked about. 

-Dan

On Aug18, Andreas Abel wrote:
> 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?
>
>
>
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda