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

[Conor McBride]

Hi

I don't know what the real boundaries are, but I can at least report the
situation in Observational Type Theory.

On 18 Aug 2013, at 15:49, Jonathan Leivent <jleivent at comcast.net> wrote:

> On 08/17/2013 11:56 PM, Wolfram Kahl wrote:
>> (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?
> 
> -- Jonathan


Equality of values is effectively defined by recursion on types and values,
so you can look at it and see how big it is. It's heterogeneous, so we have

Eq : (A : Set k)(a : A)(B : Set k)(b : B) -> Prop ?

where Prop n is the proof irrelevant sub-universe of Set n. We have this case
for two functions.

Eq (Pi S T) f (Pi S' T') f' =
  (s : S)(s' : S') -> Eq S s S' s' -> Eq (T s) (f s) (T' s') (f' s')

Consequently, ? must be at least k. When you complete the definition, you
find ? can indeed be k.

Meanwhile, we also have equality of sets, indicating that an isomorphism
connects them which amounts to the identity at closed-run time.

EQ : Set k -> Set k -> Prop ?'

and if you write out the rules, which are mostly structural, you get things
like

EQ (PI S T) (PI S' T') =
  EQ S' T' * (s' : S')(s : S) -> Eq S' s' S s -> EQ (T s) (T' s')

which allows ?' to be k, also.

Cumulativity would allow

Eq (Set k) S (Set k) T = EQ S T

So we might be able to do slightly better (at making things as small as
possible) than

  _==_ : (X : Set k)(x y : X) -> Set k

in that small-indexed families of Set k's might be comparable in Set k,
rather than Set (k+1).

So, er, um, yeah. Think about the models.

All the best

Conor