<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 -> Set where
refl : x ≡ x
proj₁ : forall {a₁ b₁ a₂ b₂ : Set} ->
(a₁ -> b₁) ≡ (a₂ -> b₂) -> 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 "homogeneously"! That's to say,
rather than interpreting heterogeneous equality
as "the types are equal and the terms are equal",
it's "if the types are equal, the terms are equal".</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' are equal, but that the types A and A' are equal as well. However, the following doesn'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' : Set l) (a' : A) → a ≃ a' → A ≃ A'<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'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) -> B1 = (x : A2) -> B2. Indeed, the definitional equality rule for Pi-types is as follows (from Goguen's PhD thesis):<br>
<br></div><div>Γ ⊢ A1 = A2 Γ , x : A1 ⊢ B1 = B2<br>---------------------------------------------------------<br> Γ ⊢ (x : A1) -> B1 = (x : A2) -> B2<br><br></div><div>so the rule seems to follow by a basic inversion argument. On the other hand, it doesn'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"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></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'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>