<p dir="ltr">Le 20 sept. 2013 20:37, &quot;Andreas Abel&quot; &lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt; a écrit :<br>
&gt; On 20.09.2013 12:14, Jesper Cockx wrote:<br>
&gt;&gt; On the other<br>
&gt;&gt; hand, it doesn&#39;t seem possible to prove the same thing for the<br>
&gt;&gt; /propositional/ (homogeneous or heterogeneous) equality. Maybe someone<br>
&gt;&gt;<br>
&gt;&gt; could shed some light on this?<br>
&gt;<br>
&gt;<br>
&gt; 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 -&gt; Bool) and (Unit -&gt; (Bool + Bool)), given that they have both 4 elements, but we don&#39;t want Bool = Unit.</p>

<p dir="ltr">Guillaume</p>
<p dir="ltr">&gt;&gt; On Thu, Sep 19, 2013 at 4:43 PM, Nils Anders Danielsson &lt;<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a><br>
&gt;&gt; &lt;mailto:<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>&gt;&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt;     On 2013-09-19 16:18, Jesper Cockx wrote:<br>
&gt;&gt;<br>
&gt;&gt;         I guess the problem with the first definition is that Agda doesn&#39;t<br>
&gt;&gt;         know how to unify the two types (x : A₁) → B₁ x and (x : A₁) → B₂ x.<br>
&gt;&gt;         Would it be problematic add such a rule to the unification<br>
&gt;&gt;         algorithm?<br>
&gt;&gt;<br>
&gt;<br>
&gt;<br>
&gt; -- <br>
&gt; Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
&gt;<br>
&gt; Theoretical Computer Science, University of Munich<br>
&gt; Oettingenstr. 67, D-80538 Munich, GERMANY<br>
&gt;<br>
&gt; <a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br>
&gt; <a href="http://www2.tcs.ifi.lmu.de/~abel/">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</p>