[Agda] Unification of function types

[Guillaume Brunerie]

Le 20 sept. 2013 20:37, "Andreas Abel" <andreas.abel at ifi.lmu.de> a écrit :
> On 20.09.2013 12:14, Jesper Cockx wrote:
>> On the other
>> hand, it doesn't seem possible to prove the same thing for the
>> /propositional/ (homogeneous or heterogeneous) equality. Maybe someone
>>
>> could shed some light on this?
>
>
> I guess the homotopy guys would not like this, since for them equality
between types is really just isomorphism.

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.

Guillaume

>> On Thu, Sep 19, 2013 at 4:43 PM, Nils Anders Danielsson <nad at cse.gu.se
>> <mailto:nad at cse.gu.se>> wrote:
>>
>>     On 2013-09-19 16:18, Jesper Cockx wrote:
>>
>>         I guess the problem with the first definition is that Agda
doesn't
>>         know how to unify the two types (x : A₁) → B₁ x and (x : A₁) →
B₂ x.
>>         Would it be problematic add such a rule to the unification
>>         algorithm?
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130920/6a501a65/attachment.html