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