A formal logic for formal category theory
From MaRDI portal
Publication:6091184
DOI10.1007/978-3-031-30829-1_6arXiv2210.08663MaRDI QIDQ6091184
Publication date: 24 November 2023
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2210.08663
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Notions of computation and monads
- Generalized algebraic theories and contextual categories
- Cartesian bicategories. I
- Yoneda structures on 2-categories
- Fixed-point constructions in order-enriched categories
- A linear logical framework
- Towards a directed homotopy type theory
- The univalence axiom in cubical sets
- Categories with families and first-order logic with dependent sorts
- Integrating Linear and Dependent Types
- Iris
- Enriched indexed categories
- A Categorical Semantics for Linear Logical Frameworks
- A type theory for synthetic $\infty$-categories
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Locally cartesian closed categories and type theory
- Elements of ∞-Category Theory
- (Co)end Calculus
- Homotopy theoretic models of identity types
- Framed bicategories and monoidal fibrations
- Categorical combinators
- Adjointness in Foundations
- Contravariance through enrichment
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Introduction to bicategories
- Internal type theory
- Call-by-name Gradual Type Theory
- Syntax and models of Cartesian cubical type theory
- [https://portal.mardi4nfdi.de/wiki/Publication:5040431 A Synthetic Perspective on $(\infty,1)$-Category Theory: Fibrational and Semantic Aspects]
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- A Constructive Model of Directed Univalence in Bicubical Sets
- Indexed type theories
- A unified framework for generalized multicategories
- A Core Quantitative Coeffect Calculus
- Generalized enrichment of categories
This page was built for publication: A formal logic for formal category theory
