<p dir="ltr">Le 20 sept. 2013 20:37, "Andreas Abel" <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>> a écrit :<br>
> On 20.09.2013 12:14, Jesper Cockx wrote:<br>
>> On the other<br>
>> hand, it doesn't seem possible to prove the same thing for the<br>
>> /propositional/ (homogeneous or heterogeneous) equality. Maybe someone<br>
>><br>
>> could shed some light on this?<br>
><br>
><br>
> I guess the homotopy guys would not like this, since for them equality between types is really just isomorphism.</p>
<p dir="ltr">Indeed, with the univalence axiom you can find 24 propositional equalities between (Bool -> Bool) and (Unit -> (Bool + Bool)), given that they have both 4 elements, but we don't want Bool = Unit.</p>
<p dir="ltr">Guillaume</p>
<p dir="ltr">>> On Thu, Sep 19, 2013 at 4:43 PM, Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a><br>
>> <mailto:<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>>> wrote:<br>
>><br>
>> On 2013-09-19 16:18, Jesper Cockx wrote:<br>
>><br>
>> 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<br>
>> algorithm?<br>
>><br>
><br>
><br>
> -- <br>
> Andreas Abel <>< Du bist der geliebte Mensch.<br>
><br>
> Theoretical Computer Science, University of Munich<br>
> Oettingenstr. 67, D-80538 Munich, GERMANY<br>
><br>
> <a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>
> <a href="http://www2.tcs.ifi.lmu.de/~abel/">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
><br>
> _______________________________________________<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">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</p>