Sökning: onr:"swepub:oai:DiVA.org:su-186353" >
Localic Categories ...
Localic Categories of Models and Categorical Aspects of Intuitionistic Ramified Type Theory
-
- Lindberg, Johan, 1985- (författare)
- Stockholms universitet,Matematiska institutionen
-
- Palmgren, Erik, Professor (preses)
- Stockholms universitet,Matematiska institutionen
-
- LeFanu Lumsdaine, Peter, PhD (preses)
- Stockholms universitet,Matematiska institutionen
-
visa fler...
-
- Forssell, Henrik, PhD (preses)
- Department of Mathematics and Science Education, University of South-Eastern Norway, Norway
-
- van den Berg, Benno, PhD (opponent)
- Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, The Netherlands
-
visa färre...
-
(creator_code:org_t)
- ISBN 9789179113506
- Stockholm : Department of Mathematics, Stockholm University, 2020
- Engelska 58 s.
- Relaterad länk:
-
https://su.diva-port... (primary) (Raw object)
-
visa fler...
-
https://su.diva-port... (Preview)
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- This thesis contains three papers, all in the general area of categorical logic, together with an introductory part with some minor results and proofs of known results which does not appear to be (easily) available in the literature.In Papers I and II we investigate the formal system Intuitionistic Ramified Type Theory (IRTT), introduced by Erik Palmgren, as an approach to predicative topos theory. In Paper I we construct and study the category of "local sets" in IRTT, including an extension with inductive definitions. We there also give a model of IRTT in univalent type theory using h-sets. In Paper II we adapt triposes and hyperdoctrines to the ramified setting. These give a categorical semantics for certain formal languages ramified in the same way as IRTT.Paper III, which is part of a joint project with Henrik Forssell, concerns logical aspects of the localic groupoid/category representations of Grothendieck toposes that originate from the work of Joyal and Tierney. Working constructively, we give explicit logical descriptions of locales and localic categories used for representing classifying toposes of geometric theories. Aspects of these descriptions are related to work by Coquand, Sambin et al in formal topology, and we show how parts of their work can be captured and extended in our framework.
Ämnesord
- NATURVETENSKAP -- Matematik -- Algebra och logik (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Algebra and Logic (hsv//eng)
Nyckelord
- Topos theory
- predicative topos theory
- ramified type theory
- type theory
- localic groupoids
- Mathematics
- matematik
Publikations- och innehållstyp
- vet (ämneskategori)
- dok (ämneskategori)
Hitta via bibliotek
Till lärosätets databas