Generalized algebraic theories and contextual categories

DOI10.1016/0168-0072(86)90053-9zbMath0634.18003OpenAlexW2006941708MaRDI QIDQ1096716

Publication date: 1986

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

Full work available at URL: https://doi.org/10.1016/0168-0072(86)90053-9

zbMATH Keywords

syntax categorical notion of `theory'contextual category doctrine functorial semantics

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Related Items

Structured theory presentations and logic representations, Categorical structures for type theory in univalent foundations, Modeling Martin-Löf type theory in categories, On the implementation of abstract data types by programming language constructs, A note on the proof theory of the \(\lambda \Pi\)-calculus, Generalized algebraic theories and contextual categories, Theory Presentation Combinators, Hom weak ω-categories of a weak ω-category, Game semantics for dependent types, A higher-order calculus and theory abstraction, Unnamed Item, On generalized algebraic theories and categories with families, Logic representation in LF, Detecting isomorphisms of modular specifications with diagrams, Dependently Sorted Logic, Finitary type theories with and without contexts, A formal logic for formal category theory, The Local Universes Model, The Interpretation Lifting Theorem for C-Systems, Martin-Löf identity types in C-systems, C-system of a module over a \(Jf\)-relative monad, Semantical analysis of contextual types, Parametrization for order-sorted algebraic specification, Induction-recursion and initial algebras., A note on Russell's paradox in locally Cartesian closed categories, Unnamed Item, Unnamed Item, Unnamed Item, Nominal Lawvere theories: a category theoretic account of equational theories with names, Unnamed Item, Unnamed Item, A logical framework combining model and proof theory, The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, Categories for computation in context and unified logic, Internal type theory, For Finitary Induction-Induction, Induction is Enough, Unnamed Item, The identity type weak factorisation system, A dependent type theory with abstractable names, Combinatorial structure of type dependency, Comprehension categories and the semantics of type dependency, The biequivalence of locally cartesian closed categories and Martin-Löf type theories, Univalence for inverse diagrams and homotopy canonicity, Unnamed Item, Unnamed Item, Unnamed Item, The simplicial model of univalent foundations (after Voevodsky), Semantics of higher inductive types, Lawvere theories and C-systems, Model structures on categories of models of type theories, A meaning explanation for HoTT, Categorical and algebraic aspects of Martin-Löf type theory, Pointers in Recursion: Exploring the Tropics, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance, Weak ω-Categories from Intensional Type Theory, Kripke Semantics for Martin-Löf’s Extensional Type Theory, Structures definable in polymorphism, Two-dimensional models of type theory, From signatures to monads in \textsf{UniMath}, Proof-search in type-theoretic languages: An introduction, Categories with families and first-order logic with dependent sorts, C-systems defined by universe categories: presheaves, The (Pi,lambda)-structures on the C-systems defined by universe categories, Detecting equivalence of modular specifications with categorical diagrams, Unnamed Item, Type Theory and Homotopy, Categories with Families: Unityped, Simply Typed, and Dependently Typed, Univalence and completeness of Segal objects, A natural semantics of first-order type dependency

Cites Work