Return to search

Towards Theory and Applications of Generalized Categories to Areas of Type Theory and Categorical Logic

Motivated by potential applications to theoretical computer science, in particular those areas where the Curry-Howard correspondence plays an important role, as well as by the ongoing search in pure mathematics for feasible approaches to higher category theory, we undertake a detailed study of a new mathematical abstraction, the generalized category. It is a partially defined monoid equipped with endomorphism maps defining sources and targets on arbitrary elements, possibly allowing a proximal behavior with respect to composition. We first present a formal introduction to the theory of generalized categories. We describe functors, equivalences, natural transformations, adjoints, and limits in the generalized setting. Next we indicate how the theory of monads extends to generalized categories, and discuss applications to computer science. In particular we discuss implications for the functional programming paradigm, and discuss how to extend categorical semantics to the generalized setting. Next, we present a variant of the calculus of deductive systems developed in the work of Lambek, and give a generalization of the Curry-Howard-Lambek theorem giving an equivalence between the category of typed lambda-calculi and the category of cartesian closed categories and exponential-preserving morphisms that leverages the theory of generalized categories. Next, we develop elementary topos theory in the generalized setting of ideal toposes, by building upon the formalism we have previously developed for the extension of the Curry-Howard-Lambek theorem. In particular, we prove that ideal toposes possess the same Heyting algebra structure and squares of adjoints that ordinary toposes do. Finally, we develop generalized sheaves, and show that such categories form ideal toposes. We extend Lawvere and Tierney's theorem relating j-sheaves and sheaves in the sense of Grothendieck to the generalized setting.

Identiferoai:union.ndltd.org:LSU/oai:etd.lsu.edu:etd-01172017-032313
Date24 January 2017
CreatorsSchoenbaum, Lucius Traylor
ContributorsSarker, Bhaba R., Sage, Daniel S., Lawson, Jimmie D., Madden, James J., Yakimov, Milen
PublisherLSU
Source SetsLouisiana State University
LanguageEnglish
Detected LanguageEnglish
Typetext
Formatapplication/pdf
Sourcehttp://etd.lsu.edu/docs/available/etd-01172017-032313/
Rightsunrestricted, I hereby certify that, if appropriate, I have obtained and attached herein a written permission statement from the owner(s) of each third party copyrighted matter to be included in my thesis, dissertation, or project report, allowing distribution as specified below. I certify that the version I submitted is the same as that approved by my advisory committee. I hereby grant to LSU or its agents the non-exclusive license to archive and make accessible, under the conditions specified below and in appropriate University policies, my thesis, dissertation, or project report in whole or in part in all forms of media, now or hereafter known. I retain all other ownership rights to the copyright of the thesis, dissertation or project report. I also retain the right to use in future works (such as articles or books) all or part of this thesis, dissertation, or project report.

Page generated in 0.0024 seconds