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

[Conor McBride]

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