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

[Dan Licata]

I think this assignment of universe levels makes sense in HoTT as well.
It's definitely the case that *homogenous* equality at A should be in the
same universe as A (universes are closed under identity types): 

_==_ : {l}{A : Set l}(a : A) -> A -> Set l

Then, instantiating this with A = Set k and l = k+1, we have 

_==_ : (a : Set k) -> Set k -> Set (k + 1)

So A == B, for A B : Set k, looks like it lives in Set (k+1), because 
it is equality at a type that is in Set (k+1).  

However, univalence says that A == B is "really" (equivalent to) the
type of equivalences between A and B, which are tuples consisting of a
function from A to B, a function from B to A, with proofs that they
compose to the identity, etc.  If you define A <->B this way, then it
will be in Set k, not Set (k+1).  

So

 _~=_ : forall {k}{A B : Set k} -> A -> B -> Set k
 _~=_ {A}{B} a b = (Q : A <-> B) -> coerce Q a == b

will indeed live in Set k, as long as Q is an equivalence (or it's a
path, and we have some of the "resizing rules" that Voevodsky has
concerned).  

Also, when equality is proof-relevant, there's a difference between Sigma and
Pi for Q : A <-> B, and we tend to work with the type 
coerce Q a == b without the quantifier (a "path over a path").  

-Dan

On Aug22, Conor McBride wrote:
> Hi Nisse
> 
> On 22 Aug 2013, at 12:44, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 
> > On 2013-08-21 22:29, Jonathan Leivent wrote:
> >> Hetero equality is at level zero (in standard library 0.7):
> >> 
> >> -- Heterogeneous equality
> >> 
> >> infix 4 _≅_
> >> 
> >> data _≅_ {a} {A : Set a} (x : A) : ∀ {b} {B : Set b} → B → Set where
> >>   refl : x ≅ x
> >> 
> >> I guess this can't be correct - or, at least, isn't consistent with
> >> where type theory is headed these days.
> > 
> > Heterogeneous equality isn't very useful when --without-K is used.
> > Furthermore it's not quite clear to me how the definition should be
> > changed. The following, less universe-polymorphic definition seems
> > reasonable to me:
> > 
> >  data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set (suc ℓ) where
> >     refl : x ≅ x
> > 
> > If others agree, then I can switch to this definition.
> 
> I think it's fine to be less polymorphic (up to the usual whimpering
> about cumulativity). I'm troubled by the "suc". It's unpleasant for
> boring ordinary equations to be so large, for example, ruling out
> the "Henry Ford" translation of inductive families where
> 
> data Foo : (n : Nat)(xs : Vec n) -> Set where
>   con1 : Foo zero vnil
>   ...
> 
> becomes
> 
> data Foo (n : Nat)(xs : Vec n) : Set where
>   con1 : n ~= zero -> xs ~= vnil -> Foo n xs
>   ...
> 
> If (and I accept this is controversial), you can content yourselves with
> 
> data _<->_ {l}(A : Set l) : Set l -> Set l
>   Refl : A <-> A
> 
> coerce : forall {l}{A B : Set l} -> A <-> B -> A -> B 
> coerce Refl a = a
> 
> data _==_ {l}{A : Set l}(a : A) : A -> Set l
>   refl : a == a
> 
> then you may define
> 
> _~=_ : forall {l}{A B : Set l} -> A -> B -> Set l
> _~=_ {A}{B} a b = (Q : A <-> B) -> coerce Q a == b
> 
> And show that it is reflexive and homogeneously substitutive. (Or pick
> Sigma for that Pi, if you want to be able to match on equality proofs.)
> 
> I accept that _<->_ is defined with a large index, which is perhaps a
> dangerous thing, in general. However, when you define _<->_ instead by
> recursion on the structure of types (e.g., for an IR-encoded universe),
> you find it is indeed as small as claimed.
> 
> I should be profoundly grateful if we could factor out the definition
> of equality from the rules for datatype acceptability. I guess I mean
> have "Agda 1" datatypes, together with a choice of standalone
> presentations of equality. It might also make "without K" easier to
> implement in an obviously correct manner. "Agda 2" datatypes and
> pattern matching as we know it could be restored by adopting a
> K-friendly equality and sugaring away the equations. But perhaps it's
> too late.
> 
> Equality was never more diverse
> 
> Conor_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda