Equality on Types [Re: [Agda] Is this a bug?]

[Thorsten Altenkirch]

On 5 May 2011, at 12:54, Conor McBride wrote:

> I see the conceptual distinctions between the usage of types and the
> structural distinctions in the arrangement of their values as of
> considerable significance.

Yes, so do I. However, I also consider the difference between bubble-sort and quick-sort of considerable importance. However, the idea of a function abstracts (hides) this important difference. If we want to talk about it, we talk about programs or function codes and not functions. Similarily, if we talk about types then we abstract from intensional differences (like the arrangement of their values). If we are interested in those differences we use type codes instead - coveniently definable as a universe using induction recursion.

I think both these concepts are important, in different situations. We could also go the other way, if we have appropriate mechanisms of quotienting. But proof-relevant quotients (to get types upto isomorphism) are enother headf***.

Cheers,
Thorsten