A note on Russell's paradox in locally cartesian closed categories

Studia Logica 48 (3):377 - 387 (1989)
  Copy   BIBTEX


Working in the fragment of Martin-Löfs extensional type theory [12] which has products (but not sums) of dependent types, we consider two additional assumptions: firstly, that there are (strong) equality types; and secondly, that there is a type which is universal in the sense that terms of that type name all types, up to isomorphism. For such a type theory, we give a version of Russell's paradox showing that each type possesses a closed term and (hence) that all terms of each type are provably equal. We consider the kind of category theoretic structure which corresponds to this kind of type theory and obtain a categorical version of the paradox. A special case of this result is the degeneracy of a locally cartesian closed category with a morphism which is generic in the sense that every other morphism in the category can be obtained from it via pullback.



    Upload a copy of this work     Papers currently archived: 89,378

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

52 (#268,753)

6 months
1 (#1,005,371)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Intuitionistic sets and ordinals.Paul Taylor - 1996 - Journal of Symbolic Logic 61 (3):705-744.

Add more citations

References found in this work

Generalised algebraic theories and contextual categories.John Cartmell - 1986 - Annals of Pure and Applied Logic 32:209-243.
Contextual Category and Generalized Algebraic Theories'.J. Cartmell - 1986 - Annals of Pure and Applied Logic 32.

Add more references