[Agda] heterogeneous equality

[Conor McBride]

Hi Dan

On 3 Mar 2008, at 20:47, Dan Licata wrote:
>

[..]

> Last night, the workaround I came up with was to take in a proof p of
> index equality and to prove that e is (homogeneously) equal to
> (subst e' p).  E.g.
>
> waha : {X : Set}{m n : Nat}
>        {xs : Vec X m}{ys : Vec X n}{x : X} ->
>        (p : Id m n) (sp : Id (suc m) (suc n))
>      -> Id (subst (\i -> Vec X i) xs p) ys
>      -> Id (subst (\i -> Vec X i) (cons x xs) sp) (cons x ys)

This gives me serious flashbacks to 1998. That was
when I gave my first coding of dependent pattern matching
via elimination rules, hence working with hypothetical
sequences of equations over a telescope, but trying to use
homogeneous equality. Inevitably, the nth equation (counting
from zero) looked like

   q_n : Id (subst_n (\ x_0 .. x_{n-1}. T_n) q_0 .. q_{n-1}
             s_n)
            t_n

To get anywhere with these things, you need dependent
elimination of equations. Constructor injectivity is a
barrel of laughs. Getting rid of x=x requires Axiom K.
And it was all up and running by Types 1998: I think
I made Lego do vectorized addition, or something.

It was only when I was writing my thesis that I figured
out this...

>
> The heterogeneous version then seems like a simple twist that saves  
> you
> from manually commuting-converting the subst in and out of contexts

...and felt like a complete idiot.

> ---as
> you said, I can work with a telescope, rather than coercing everything
> to the same type at each step.

Yes, as the intensional gap between the types gets
wider and wider, further along the telescope, but
heterogeneous equality is suitably elastic. As long
as you maintain the telescope invariant, the first
equation will always be homogeneous. Solving earlier
equations pulls the types in later equations closer
together.

> The conjunctive interpretation, which post-darcs-pull Agda moves
> towards, feels a little impredicative: it makes me nervous to have a
> set of equality of sets, since this set "talks" about itself.

I'm less worried about the general idea of a set
equality in set. How about...?

record SetEq (A B : Set) : Set where
   field
     coerce  : A -> B
     ecreoc  : B -> A
     noop    : (a : A) -> HId a (coerce a)
     poon    : (b : B) -> HId (ecreoc b) b

open module HocusPocus {A B : Set} = SetEq {A}{B}

Refl : {X : Set} -> SetEq X X
Refl = record {
   coerce = \x -> x ;
   noop = \x -> HRefl ;
   ecreoc = \x -> x ;
   poon = \x -> HRefl }

Resp : {X : Set}(P : X -> Set)
        {x x' : X} -> HId x x' -> SetEq (P x) (P x')
Resp P HRefl = Refl

That's quite a reasonable notion of equality on sets
and it's small if equality on elements is small.
Pre-pull, it's still not strong enough to derive
"type constructors injective".

>   Are there
> dangers lurking under this tarpeian rock?

Of course, when it comes to equality in type theory,
like most issues only more so, the biggest danger
is to be too entrenched in one's own point of view.

I don't see anything paradoxical about set equality
in set, or even about type constructors being
injective. We managed to have both in the OTT
construction. See

http://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/OTT/ObsEq.agda

or in your own copy.

But it's very definitely a choice which rules out
some models and places really quite an intensional
interpretation on what it is for sets to be equal.
I'm happy with it, but for pragmatic rather than
philosophical reasons. If you allow more set
equations than the structural ones, then it can
really take work to transport elements between
equal sets, so you need to keep the proofs around,
even if you never compute under a binder.

But it's one thing to guarantee that good behaviour
for the machine, and another thing to expose it as
a reasoning principle. One might well argue that
any proofs based on type constructor reasoning
can and should be shifted to the data level, by
means of a universe. I say yes, and it's a nice
universe, and I'm happy just to live there.

All the best

Conor