<div dir="ltr">Does the elimination rule for heterogeneous equality really imply K?<div><br></div><div>Take the type as defined in agda stdlib Relation.Binary.HeterogeneousEquality:</div><div><br></div><div><div> data _≅_ {i} {A : Set i} (x : A) : {B : Set i} → B → Set i where</div><div> refl : x ≅ x</div><div><br></div><div>This is the eliminator, right?</div><div><br></div><div> elim-≅ : ∀ {i j} {A : Set i} {x : A}</div><div> (C : {B : Set i} {y : B} → x ≅ y → Set j)</div><div> → C refl</div><div> → {B : Set i} {y : B} (p : x ≅ y) → C p</div><div> elim-≅ C c refl = c</div></div><div><br></div><div>This does not imply K, does it?</div><div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Oct 27, 2016 at 2:30 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
Often people mention the formulation and proof of associativity of<br>
vector concatenation as something tricky.<br>
<br>
The problem, of course, is that for vectors xs, ys, and zs, the<br>
concatenations<br>
<br>
xs ++ (ys ++ zs) of length l + (m + n)<br>
<br>
and<br>
<br>
(xs ++ ys) ++ zs of length (l + m) + n<br>
<br>
belong to the different (but isomorphic) types<br>
<br>
Vec X (l + (m + n)) and Vec X ((l + m) + n).<br>
<br>
One approach considers heterogeneous equality, which is a notion of<br>
equality that allows to compare elements of different types. A<br>
limitation of this equality is that its elimination rule implies the K<br>
axiom (any two proofs of equality are equal), which is incompatible<br>
with univalent type theory as in the HoTT Book or as in Cubical Type<br>
Theory, which are type theories some people wish to either use or at<br>
least be compatible with.<br>
<br>
Not only can we be compatible with univalent type theory, but also<br>
we can learn from it (even without using univalence or other features that<br>
don't belong to Martin-Loef Type Theory as represented by Agda).<br>
<br>
I would like to advertise this here, as the ideas are of general use,<br>
even if one is not interested in HoTT, and hopefully intuitive and<br>
natural too.<br>
<br>
Given a type X and a type family F:X->Set, suppose we have x,y:X,<br>
p:x≡y and a : F x and b : F y. Even though x and y are equal, the<br>
types F x and F y are not the same (they are equal under univalence,<br>
but we don't want to use this). So can't compare a and b for equality.<br>
<br>
But we can define a notion of equality between the types F x and F y,<br>
dependent on p:x≡y,<br>
<br>
a ≡[ p ] b,<br>
<br>
by<br>
<br>
a ≡[ refl ] b = a ≡ b.<br>
<br>
In particular, we get<br>
<br>
_≡[_]_ : ∀ {X} {m n} → Vec X m → m ≡ n → Vec X n → Set<br>
xs ≡[ refl ] ys = xs ≡ ys<br>
<br>
Then vector associativity becomes<br>
<br>
++-assoc : ∀ {X : Set} l m n (xs : Vec X l) (ys : Vec X m) (zs : Vec X n)<br>
→ xs ++ (ys ++ zs) ≡[ +-assoc l m n ] (xs ++ ys) ++ zs<br>
<br>
where<br>
<br>
+-assoc : ∀ l m n → l + (m + n) ≡ (l + m) + n.<br>
<br>
Its proof is the same as that of associativity of list concatenation<br>
(where the problem discussed in this message doesn't arise), but<br>
taking care of the extra subscript p for dependent equality, in a way<br>
that doesn't become disruptive or require new ideas, as shown here:<br>
<br>
<a href="http://www.cs.bham.ac.uk/~mhe/agda/VecConcatAssoc.html" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/<wbr>agda/VecConcatAssoc.html</a><br>
<br>
The idea is very similar to using heterogeneous equality, as you will<br>
see.<br>
<br>
Anyway, I wanted to advertise this idea coming from univalent type<br>
theory, and try to convince you of its simplicity and naturality and<br>
usefulness.<br>
<br>
Martin<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div></div>