Categories with families and first-order logic with dependent sorts

DOI10.1016/J.APAL.2019.102715zbMath1458.18003arXiv1605.01586OpenAlexW2955445504WikidataQ127577540 ScholiaQ127577540MaRDI QIDQ2326422

Erik Palmgren

Publication date: 7 October 2019

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1605.01586

zbMATH Keywords

categorical logicdependent typesintuitionistic first-order logicmodels of type theory

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10) Metamathematics of constructive systems (03F50)

Related Items (2)

A formal logic for formal category theory ⋮ Homotopical inverse diagrams in categories with attributes

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
• Proof-relevance of families of setoids and identity in type theory
• A minimalist two-level foundation for constructive mathematics
• Generalized algebraic theories and contextual categories
• Categorical logic and type theory
• Dependently Sorted Logic
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Internal type theory
• The generalised type-theoretic interpretation of constructive set theory
• AN ELEMENTARY THEORY OF THE CATEGORY OF SETS
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories

This page was built for publication: Categories with families and first-order logic with dependent sorts