2 Search Results for "Larrea, Martin L."

Document
DOI: 10.4230/LIPIcs.CSL.2026.38
The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Authors: Daniël Otten and Matteo Spadetto

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 𝟙-types, and Σ-types are biequivalent to finitely complete categories, while adding Π-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 𝟙- and Σ-types are biequivalent to certain path categories, while adding axiomatic Π-types yields dependent homotopy exponents. This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 𝟙-, Σ-, and Π-types.
Cite as

Daniël Otten and Matteo Spadetto. The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 38:1-38:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{otten_et_al:LIPIcs.CSL.2026.38,
  author =	{Otten, Dani\"{e}l and Spadetto, Matteo},
  title =	{{The Biequivalence of Path Categories and Axiomatic Martin-L\"{o}f Type Theories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{38:1--38:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.38},
  URN =		{urn:nbn:de:0030-drops-254633},
  doi =		{10.4230/LIPIcs.CSL.2026.38},
  annote =	{Keywords: Axiomatic type theory, cubical type theory, propositional equality, biequivalence, display map categories, path categories, homotopy theory, coherence}
}
Document
DOI: 10.4230/DFU.Vol2.SciViz.2011.92
Integrating Semantics into the Visualization Process

Authors: Sebastian Escarza, Martin L. Larrea, Dana K. Urribarri, Silvia M. Castro, and Sergio R. Martig

Published in: Dagstuhl Follow-Ups, Volume 2, Scientific Visualization: Interactions, Features, Metaphors (2011)

Abstract
Most of today's visualization systems give the user considerable control over the visualization process. Many parameters might be changed until the obtention of a satisfactory visualization. The visualization process is a very complex exploration activity and, even for skilled users, it can be difficult to arrive at an effective visualization. We propose the construction of a visualization prototype to assist users and designers throughout the stages of the visualization process, and the integration of such process with a reasoning procedure that allows the configuration of the visualization, based on the entailed conclusions. We are working on a formal representation of the Visualization field. We aim to establish a common visualization vocabulary, include the underlying semantics, and enable the definition of visualization specifications that can be executed by a visualization engine with ontological support. An ontological description of a visualization should be enough to specify the visualization and, thus, to generate a runtime environment that is able to bring that visualization to life. The visualization ontology defines the vocabulary. With the addition of inference rules to the system, we can derive conclusions about visualization properties that allow to enhance the visualization, and guide the user throughout the entire process toward an effective result.
Cite as

Sebastian Escarza, Martin L. Larrea, Dana K. Urribarri, Silvia M. Castro, and Sergio R. Martig. Integrating Semantics into the Visualization Process. In Scientific Visualization: Interactions, Features, Metaphors. Dagstuhl Follow-Ups, Volume 2, pp. 92-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InCollection{escarza_et_al:DFU.Vol2.SciViz.2011.92,
  author =	{Escarza, Sebastian and Larrea, Martin L. and Urribarri, Dana K. and Castro, Silvia M. and Martig, Sergio R.},
  title =	{{Integrating Semantics into the Visualization Process}},
  booktitle =	{Scientific Visualization: Interactions, Features, Metaphors},
  pages =	{92--102},
  series =	{Dagstuhl Follow-Ups},
  ISBN =	{978-3-939897-26-2},
  ISSN =	{1868-8977},
  year =	{2011},
  volume =	{2},
  editor =	{Hagen, Hans},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DFU.Vol2.SciViz.2011.92},
  URN =		{urn:nbn:de:0030-drops-33044},
  doi =		{10.4230/DFU.Vol2.SciViz.2011.92},
  annote =	{Keywords: semantic driven visualization, ontology, visualization, knowledge representation}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2011

  • Refine by Author
  • 1 Castro, Silvia M.
  • 1 Escarza, Sebastian
  • 1 Larrea, Martin L.
  • 1 Martig, Sergio R.
  • 1 Otten, Daniël
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 DFU

  • Refine by Classification
  • 1 Mathematics of computing → Topology
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Axiomatic type theory
  • 1 biequivalence
  • 1 coherence
  • 1 cubical type theory
  • 1 display map categories
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact