<div dir="ltr">I guess that you are referring to the 'John Major' equality in Conor McBride's thesis here? <a href="http://strictlypositive.org/thesis.pdf" target="_blank">http://strictlypositive.org/th<wbr>esis.pdf</a><div><br></div><div>In section 5.1.3 (page 120), there is the following note:</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Observe that eqElim is not the elimination rule which one would expect if ≃ was
inductively defined.
The ‘usual’ rule eliminates over all the
formable equations, and it is quite useless...</blockquote><div><div><br></div><div>Even if the usual rule is useless, it is what we will have in Agda for an inductively defined heterogeneous equality :).</div><div><br></div></div><div>It is trivial using the 'useless' rule to give an equivalence between (a <span style="font-size:12.8px">≅ b) and (A , a) ≡ (B , b), where _≡_ is the usual homogeneous equality. So then _</span><span style="font-size:12.8px">≅_ will be related to your </span><span style="font-size:12.8px">_≡[_]_ as total space to fiber.</span></div><div><span style="font-size:12.8px"><br></span></div><div class="gmail_extra"><div class="gmail_quote">On Thu, Oct 27, 2016 at 3:49 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"><span class="m_9132739466224187225m_-860527742531438575gmail-m_6399745163396262538gmail-"><br>
<br>
On 27/10/16 23:00, Tom Jack wrote:<br>
> Does the elimination rule for heterogeneous equality really imply K?<br>
<br>
</span>If I am not mistaken, this was proved by the very person who introduced<br>
heterogeneous equality in the first place, in his PhD thesis.<br>
<br>
But I am open to be corrected.<br>
<br>
Martin<br>
<span class="m_9132739466224187225m_-860527742531438575gmail-m_6399745163396262538gmail-"><br>
<br>
><br>
> Take the type as defined in agda stdlib<br>
> Relation.Binary.HeterogeneousE<wbr>quality:<br>
><br>
> data _≅_ {i} {A : Set i} (x : A) : {B : Set i} → B → Set i where<br>
> refl : x ≅ x<br>
><br>
> This is the eliminator, right?<br>
><br>
> elim-≅ : ∀ {i j} {A : Set i} {x : A}<br>
> (C : {B : Set i} {y : B} → x ≅ y → Set j)<br>
> → C refl<br>
> → {B : Set i} {y : B} (p : x ≅ y) → C p<br>
> elim-≅ C c refl = c<br>
><br>
> This does not imply K, does it?<br>
><br>
> On Thu, Oct 27, 2016 at 2:30 PM, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a><br>
</span><div><div class="m_9132739466224187225m_-860527742531438575gmail-m_6399745163396262538gmail-h5">> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.u<wbr>k</a>>> wrote:<br>
><br>
><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<br>
> 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<br>
> 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>
> <<a href="http://www.cs.bham.ac.uk/~mhe/agda/VecConcatAssoc.html" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mh<wbr>e/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>
</div></div>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><wbr>><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a><br>
<div class="m_9132739466224187225m_-860527742531438575gmail-m_6399745163396262538gmail-HOEnZb"><div class="m_9132739466224187225m_-860527742531438575gmail-m_6399745163396262538gmail-h5">> <<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/ma<wbr>ilman/listinfo/agda</a>><br>
><br>
><br>
<br>
--<br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
</div></div></blockquote></div><br></div></div>