[Agda] Lightweight free theorems

[Andrea Vezzosi]

The wiki doesn't explain how to handle types one inherits from the
surrounding scope.
e.g. suppose there's a (A : Set) in scope, how should we define [A] :
[Set] A A? It seems consistent to assume [A] <-> _≡_ but I'm not sure.

Similarly for (F : Set -> Set) i'd tend to assume [F] _≡_ <-> _≡_.

On Fri, May 7, 2010 at 3:48 PM, Jean-Philippe Bernardy
<bernardy at chalmers.se> wrote:
> Now uploaded to (and linked from) the wiki:
>
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems
>
>
> -- JP.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda