Search: onr:"swepub:oai:DiVA.org:su-186353" >
Localic Categories ...
Localic Categories of Models and Categorical Aspects of Intuitionistic Ramified Type Theory
-
- Lindberg, Johan, 1985- (author)
- Stockholms universitet,Matematiska institutionen
-
- Palmgren, Erik, Professor (thesis advisor)
- Stockholms universitet,Matematiska institutionen
-
- LeFanu Lumsdaine, Peter, PhD (thesis advisor)
- Stockholms universitet,Matematiska institutionen
-
show more...
-
- Forssell, Henrik, PhD (thesis advisor)
- 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
-
show less...
-
(creator_code:org_t)
- ISBN 9789179113506
- Stockholm : Department of Mathematics, Stockholm University, 2020
- English 58 s.
- Related links:
-
https://su.diva-port... (primary) (Raw object)
-
show more...
-
https://su.diva-port... (Preview)
-
https://urn.kb.se/re...
-
show less...
Abstract
Subject headings
Close
- 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.
Subject headings
- NATURVETENSKAP -- Matematik -- Algebra och logik (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Algebra and Logic (hsv//eng)
Keyword
- Topos theory
- predicative topos theory
- ramified type theory
- type theory
- localic groupoids
- Mathematics
- matematik
Publication and Content Type
- vet (subject category)
- dok (subject category)
Find in a library
To the university's database