Switch to: References

Citations of:

Contextual Category and Generalized Algebraic Theories'

Annals of Pure and Applied Logic 32 (1986)

Add citations

You must login to add citations.

A note on Russell's paradox in locally cartesian closed categories.Andrew M. Pitts & Paul Taylor - 1989 - Studia Logica 48 (3):377 - 387.details 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 (...) Download Export citation Bookmark 2 citations
Categorical and algebraic aspects of Martin-löf type theory.Adam Obtułowicz - 1989 - Studia Logica 48 (3):299 - 317.details In the paper there are introduced and discussed the concepts of an indexed category with quantifications and a higher level indexed category to present an algebraic characterization of some version of Martin-Löf Type Theory. This characterization is given by specifying an additional equational structure of those indexed categories which are models of Martin-Löf Type Theory. One can consider the presented characterization as an essentially algebraic theory of categorical models of Martin-Löf Type Theory. The paper contains a construction of an indexed (...) Download Export citation Bookmark 2 citations

1