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.


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

Reply via email to