<div dir="ltr"><div> Thank you for the links, they are very interesting discussions. At the end of the first one, you posed the following question:<br></div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">

<pre>I have a related issue. The following does not type check:

data _≡_ {a : Set1} (x : a) : a -&gt; Set where
  refl : x ≡ x

proj₁ : forall {a₁ b₁ a₂ b₂ : Set} -&gt;
        (a₁ -&gt; b₁) ≡ (a₂ -&gt; b₂) -&gt; a₁ ≡ a₂
proj₁ refl = refl

Agda complains about the pattern refl (a₁ != a₂). In light of your
recent patch, is there any reason not to allow also this function?</pre></blockquote><div>This seems to be very related to my problem, but unfortunately no answer was given. <br><br></div><div>Also in the same thread, Ulf mentioned that he added injectivity of type constructors, however the following code does not typecheck for me:<br>

<br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">module Test where<br><br>open import Data.Unit<br>open import Relation.Binary.PropositionalEquality<br>

<br>data I : Set → Set where<br>  i : I ⊤<br><br>I-inj : {A B : Set} → I A ≡ I B → A ≡ B<br>I-inj refl = refl</blockquote><div><br></div><div>Has this been removed again from Agda? (Maybe in light of the problems discussed in the second thread?) <br>

<br></div><div>An interesting remark by Conor was the following:<br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote"><pre>Back when I was mucking about with this type,
my answer was &quot;homogeneously&quot;! That&#39;s to say,
rather than interpreting heterogeneous equality
as &quot;the types are equal and the terms are equal&quot;,
it&#39;s &quot;if the types are equal, the terms are equal&quot;.</pre></blockquote><div>It seems I can prove that the types are equal from the heterogeneous equality: the type of the constructor refl (in my first post) tells us not just that the terms a and a&#39; are equal, but that the types A and A&#39; are equal as well. However, the following doesn&#39;t typecheck:<br>

<br></div><div><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">equal-types : ∀ {l} (A : Set l) (a : A) (A&#39; : Set l) (a&#39; : A) → a ≃ a&#39; → A ≃ A&#39;<br>

equal-types A a .A .a refl = {!!}<br><div><br>Failed to infer the value of dotted pattern<br>when checking that the pattern .A has type Set l <br></div></blockquote><div><br></div><div>So I guess I&#39;m missing something here.<br>

<br></div><div>From a more theoretical perspective, it seems to me quite unproblematic to add a rule that A1 = A2 and B1 = B2 whenever (x : A1) -&gt; B1 = (x : A2) -&gt; B2. Indeed, the definitional equality rule for Pi-types is as follows (from Goguen&#39;s PhD thesis):<br>

<br></div><div>Γ ⊢ A1 = A2        Γ , x : A1 ⊢ B1 = B2<br>---------------------------------------------------------<br>   Γ ⊢ (x : A1) -&gt; B1 = (x : A2) -&gt; B2<br><br></div><div>so the rule seems to follow by a basic inversion argument. On the other hand, it doesn&#39;t seem possible to prove the same thing for the <i>propositional</i> (homogeneous or heterogeneous) equality. Maybe someone could shed some light on this?<br>

<br></div><div>Thanks for your answers,<br></div><div><br></div><div>Jesper Cockx<br></div> <br></div><br></div></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Sep 19, 2013 at 4:43 PM, Nils Anders Danielsson <span dir="ltr">&lt;<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 2013-09-19 16:18, Jesper Cockx wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I guess the problem with the first definition is that Agda doesn&#39;t<br>
know how to unify the two types (x : A₁) → B₁ x and (x : A₁) → B₂ x.<br>
Would it be problematic add such a rule to the unification algorithm?<br>
</blockquote>
<br></div>
You may be interested in the following mailing list threads:<br>
<br>
  heterogeneous equality<br>
  <a href="https://lists.chalmers.se/pipermail/agda/2008/000153.html" target="_blank">https://lists.chalmers.se/<u></u>pipermail/agda/2008/000153.<u></u>html</a><br>
<br>
  Agda with the excluded middle is inconsistent ?<br>
  <a href="http://thread.gmane.org/gmane.science.mathematics.logic.coq.club/4322" target="_blank">http://thread.gmane.org/gmane.<u></u>science.mathematics.logic.coq.<u></u>club/4322</a><span class="HOEnZb"><font color="#888888"><br>


<br>
-- <br>
/NAD<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>