[Agda] Yet another questions about equality

[Dan Doel]

On Saturday 19 February 2011 10:06:36 AM Peter Hancock wrote:
> In the interest of restoring balance to the universe, I've changed my mind.
> Seriously, this presentation by T. Coquand:
> http://www.cse.chalmers.se/~coquand/bologna.pdf
> seems to suggest (see the end) that it may be possible to treat
> the identity types purely axiomatically, with no computation rules.
> (Nils Danielsson has had a hand in this too.)

If you're talking about him mentioning the connection with OTT, it was my 
impression that he was suggesting that the univalent foundations extend OTT 
such that there _is_ a proper computational interpretation of equality. 
Specifically, equality of sets is interpreted as isomorphism, instead of being 
true along the diagonal, and false otherwise.

> There is certainly something "fatuous" (I can't think of a better word)
> about the computation rule for J -- in the same way as there is something
> fatuous about the elimination rule for the singleton rule for N_1 (the
> standard singleton set).

I'm not exactly sure what your meaning is here. However, it's kind of 
interesting to note that type theorists would usually suggest that the J 
induction rule, and its computation, works because there is one canonical way 
of proving equality: refl. So when we write:

  J : P x refl -> P y eq, A : Type, x : A, P : (y : A) -> x = y -> Type

it must work because y must be x, and eq must be refl. Univalent foundations 
suggest that this needn't actually be the case when x and y are themselves 
sets. But we still have J. What does this mean? It means that predicates on 
sets P themselves hold only up to isomorphism on sets. So we are not justified 
because y must be x, and the proof must be refl, but because x and y are 
isomorphic, and there is a way to transport a proof of P x refl along the 
isomorphism to a proof of P y eq (and similar for higher-dimensional types).

At least, I think that's what's going on. I suppose what is also interesting 
is that we can work with the unique identity proofs in mind, with the trivial 
computation rule, and still get results that still work with the non-unique 
identity interpretation. That is, as long as we stick to J, and don't add K. 
Of course, the univalent foundations also suggest axioms to add that 
contradict the unique identity proof view. J and refl are the common ground.

Technically, all inductive definitions and eliminations are similarly under-
specified. The rules for the unit type don't really guarantee that there is 
only one inhabitant, just that there is at least one, and that if a predicate 
holds for that one, it holds for any other. Similar to how the induction 
schema in Peano arithmetic cannot rule out non-standard models. The univalent 
folks are suggesting that a 'non-standard' model of type theory might be a 
better one, though, I suppose.

-- Dan