Dear Thorsten, Robin, Now that the discussion has turned to setoids and observational type theory, I could not help myself from responding. (Thorsten and I had quite some off-line discussion about this).
I generally agree with Thorsten's description of observational type theory as internalizing the setoid construction. One clearly feels the need for such machinery when working with Coq. (Although this seems to have improved somewhat with the inclusion of the new setoid_rewrite tactic.) However, I would like to point out that there seems to be an important distinction between the category of setoids and the extensional type theory defined by observational type theory. Let me first say how they are similar. Both of these categories should have the structure of a "predicative topos". The search for the right definition of a predicative analogue of topos theory was started by Moerdijk and Palmgren. A topos is a model of higher-order intuitionistic logic. We should have topos pred. topos -------- == --------- iHOL ext type theory However, predicative toposes should also generalize toposes. Currently, the notion of a Pi W-pretopos seems to be a good candidate for the notion of "predicative topos". In any case, observational type theory should give rise to the internal type theory of a predicative topos. However, the predicative topos of setoids models the axiom of countable (dependent) choice. This implies that the Dedekind real numbers and the Dedekind real numbers coincide. For general (predicative) toposes the Dedekind construction of real numbers and the Cauchy definition of real numbers need not be the same. Since it is unlikely that observational type theory includes the axiom of countable choice we will have to take this into account when programming, say, the real numbers in epigram. To conclude, when using the setoid construction in intensional type theory we can use all the results from Bishop's constructive mathematics when programming/proving. This is no longer the case in observational type theory. Hopefully, it is possible to develop a good replacement. Bas PS: I know this may sound too theoretical to some, but it seems to have a real effect on programming, say, real numbers in epigram. ------------------------------------------------------- Research Group Foundations/ Institute for Computing and Information Sciences Radboud University Nijmegen www.cs.ru.nl/~spitters/