Editing Type theory (section)

===Research areas===

==== Category theory ====

Although the initial motivation for [[category theory]] was far removed from foundationalism, the two fields turned out to have deep connections. As [[John Lane Bell]] writes: "In fact categories can ''themselves'' be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or ''sorts'' <ref>{{Cite journal|last=Barendregt|first=Henk|date=1991|title=Introduction to generalized type systems|journal=[[Journal of Functional Programming]]|volume=1|issue=2|pages=125–154|doi=10.1017/s0956796800020025|issn=0956-7968|hdl=2066/17240|s2cid=44757552 |hdl-access=free}}</ref>), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:<ref name="Sets and Extensions in the Twentieth Century">{{cite book|series=Handbook of the History of Logic|volume=6|title=Sets and Extensions in the Twentieth Century|year=2012|publisher=Elsevier|isbn=978-0-08-093066-4|first=John L.|last=Bell|chapter=Types, Sets and Categories|chapter-url=http://publish.uwo.ca/~jbell/types.pdf|editor-first=Akihiro|editor-last=Kanamory|access-date=2012-11-03|archive-date=2018-04-17|archive-url=https://web.archive.org/web/20180417105624/http://publish.uwo.ca/~jbell/types.pdf|url-status=live}}</ref>
* [[Cartesian closed category|cartesian closed categories]] correspond to the typed λ-calculus ([[Lambek]], 1970);
* [[C-monoid]]s (categories with products and exponentials and one non-terminal object) correspond to the untyped λ-calculus (observed independently by Lambek and [[Dana Scott]] around 1980);
* [[Locally cartesian closed category|locally cartesian closed categories]] correspond to [[Martin-Löf type theory|Martin-Löf type theories]] (Seely, 1984).

The interplay, known as [[categorical logic]], has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.

==== Homotopy type theory ====
[[Homotopy type theory]] attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types. [[Homotopy type theory]] differs from [[intuitionistic type theory]] mostly by its handling of the equality type. In 2016, [[cubical type theory]] was proposed, which is a homotopy type theory with normalization.<ref>{{Cite book |last1=Sterling |first1=Jonathan |title=2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |last2=Angiuli |first2=Carlo |date=2021-06-29 |publisher=IEEE |isbn=978-1-6654-4895-6 |location=Rome, Italy |pages=1–15 |chapter=Normalization for Cubical Type Theory |doi=10.1109/LICS52264.2021.9470719 |access-date=2022-06-21 |chapter-url=https://ieeexplore.ieee.org/document/9470719 |archive-url=https://web.archive.org/web/20230813170127/https://ieeexplore.ieee.org/document/9470719 |archive-date=2023-08-13 |url-status=live |arxiv=2101.11479 |s2cid=231719089}}</ref><ref name=":0" />