[Agda] Lightweight free theorems

[Jean-Philippe Bernardy]

On Fri, Dec 23, 2011 at 6:27 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> 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?

Following the published theory, if A is abstracted over, so should be [A].
In a forthcoming paper we define a calculus with a primitive [_] operation;
but I'm not sure this would help you.

> It seems consistent to assume [A] <-> _≡_ but I'm not sure.

I think you'll run into problems if you "look" at the proofs of equality, then.
Still, making [A] substitutive, for any abstract A, would is be nice.
Thinking about it is my favourite way to lose sleep.

Cheers,
JP.