DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2025.9

Kleisli Categories with Display Maps

Authors: Moana Jubert

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract

In this paper, we show that the Kleisli category C_T for a monad T : C → C is sometimes a structured display map category, meaning that it provides a minimal categorical setting for dependent type theory. If the underlying category C is itself a (structured) display map category, we prove that under mild conditions the canonical functor F_T : C → C_T induces a bijection between the contexts, types, and terms of both C and C_T, thus establishing a kind of "collapsing" result. Finally, we provide several examples and nonexamples, most notably showing that Δ^op equipped with the class of surjective maps is a (structured) display map category.

Cite as

Moana Jubert. Kleisli Categories with Display Maps. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{jubert:LIPIcs.TYPES.2025.9,
  author =	{Jubert, Moana},
  title =	{{Kleisli Categories with Display Maps}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.9},
  URN =		{urn:nbn:de:0030-drops-270276},
  doi =		{10.4230/LIPIcs.TYPES.2025.9},
  annote =	{Keywords: Kleisli categories, Structured display map categories, Dependent type theory}
}

Search Results

Documents authored by Jubert, Moana

Kleisli Categories with Display Maps

Abstract

Cite as

Thanks for your feedback!

Could not send message