[Agda] Unification of function types
guillaume.brunerie at gmail.com
Fri Sep 20 21:54:04 CEST 2013
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.
>> 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
>> know how to unify the two types (x : A₁) → B₁ x and (x : A₁) →
>> Would it be problematic add such a rule to the unification
> 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
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda