Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 36f21b41 authored by Noam Zeilberger's avatar Noam Zeilberger
Browse files

niyousha

parent 0d0fb2ec
Branches
No related tags found
No related merge requests found
Pipeline #1142288 failed
......@@ -26,7 +26,7 @@
speaker: Niyousha Najmaei
picture: https://niyoushanajmaei.github.io/images/nioosha.png
website: https://niyoushanajmaei.github.io/
lab: IRIF
lab: LIX
title: A Type Theory for Comprehension Categories with Applications to Subtyping
abstract: |
We develop a type theory that we show is an internal language for comprehension categories. This type theory is closely related to Martin-Löf type theory (MLTT). Indeed, semantics of MLTT are often given in comprehension categories, albeit usually only in discrete or full ones. As we explain, requiring a comprehension category to be full or discrete can be understood as removing one “dimension” of morphisms. Thus, in our syntax, we recover this extra dimension. We show that this extra dimension can be used to encode subtyping in a natural way. Important instances of non-full comprehension categories include ones used for constructive or univalent intensional models of MLTT and directed type theory, and so our syntax is a more faithful internal language for these than is MLTT.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment