First-order homotopical logic

DOI10.1017/JSL.2023.68MaRDI QIDQ6953431zbMATH OpenFDO

Authors Joseph Helfer

Publication date 24 July 2025

Published in The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/JSL.2023.68

zbMATH Keywords

2-categoriescategorical logicGrothendieck fibrationshomotopy type theoryintuitionistic logicmodel categories

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Fibered categories (18D30) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Cites work

• A categorical version of the BrouwerHeytingKolmogorov interpretation
• Adjointness in foundations
• Avoiding the axiom of choice in general category theory
• Categorical logic and type theory
• Constructivism in mathematics. An introduction. Volume II
• Generalized sketches as a framework for completeness theorems. I-III
• Homotopical algebra
• Homotopies in Grothendieck fibrations
• Homotopy invariant algebraic structures on topological spaces
• Homotopy theoretic models of identity types
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 53544 (Why is no real title available?)
• scientific article; zbMATH DE number 1226952 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• scientific article; zbMATH DE number 3342819 (Why is no real title available?)
• scientific article; zbMATH DE number 3370546 (Why is no real title available?)
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Lambek's categorical proof theory and Läuchli's abstract realizability
• Locally cartesian closed categories and type theory
• More concise algebraic topology. Localization, completion, and model categories
• On a Topological Topos
• Semantics of higher inductive types
• Some algebraic problems in the context of functorial semantics of algebraic theories
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
• The simplicial model of univalent foundations (after Voevodsky)
• Two-dimensional monad theory

This page was built for publication: First-order homotopical logic

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