From 36f21b4173a0e3a144e544dbdac3ce75e5d0a432 Mon Sep 17 00:00:00 2001
From: Noam Zeilberger <noam.zeilberger@gmail.com>
Date: Fri, 21 Mar 2025 16:39:23 +0100
Subject: [PATCH] niyousha

---
 _data/seminar.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/_data/seminar.yml b/_data/seminar.yml
index 3a6e971..dc2a145 100644
--- a/_data/seminar.yml
+++ b/_data/seminar.yml
@@ -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.
-- 
GitLab