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/
