Categorical models of subtyping

DOI10.4230/LIPICS.TYPES.2023.3MaRDI QIDQ6865660zbMATH OpenFDO

Authors Greta Coraglia, Jacopo Emmenegger

Publication date 30 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2023.3

zbMATH Keywords

categorical semanticscategories with familiescoercive subtypingdependent typesmonadsubtyping

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites work

• 2-Dimensional Directed Type Theory
• A 2-categorical analysis of context comprehension
• A comonad for Grothendieck fibrations
• Categorical logic and type theory
• Coercive subtyping
• Coercive subtyping: theory and implementation
• Colimit completions and the effective topos
• Comprehension categories and the semantics of type dependency
• scientific article; zbMATH DE number 2125670 (Why is no real title available?)
• scientific article; zbMATH DE number 3825806 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 626734 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 3370546 (Why is no real title available?)
• scientific article; zbMATH DE number 3423547 (Why is no real title available?)
• Internal type theory
• Natural models of homotopy type theory
• Quotient completion for the foundation of constructive mathematics
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
• Types and programing languages
• Types are weak -groupoids

This page was built for publication: Categorical models of subtyping

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6865660)