Pages that link to "Item:Q1096716"

The following pages link to Generalized algebraic theories and contextual categories (Q1096716):

Displaying 50 items.

• Modeling Martin-Löf type theory in categories (Q280835) (← links)
• A dependent type theory with abstractable names (Q530845) (← links)
• Categories for computation in context and unified logic (Q678833) (← links)
• Categorical and algebraic aspects of Martin-Löf type theory (Q750438) (← links)
• Parametrization for order-sorted algebraic specification (Q909448) (← links)
• A note on Russell's paradox in locally Cartesian closed categories (Q914668) (← links)
• The identity type weak factorisation system (Q959823) (← links)
• On the implementation of abstract data types by programming language constructs (Q1089793) (← links)
• Generalized algebraic theories and contextual categories (Q1096716) (← links)
• Comprehension categories and the semantics of type dependency (Q1208414) (← links)
• Structures definable in polymorphism (Q1273075) (← links)
• A natural semantics of first-order type dependency (Q1314402) (← links)
• Structured theory presentations and logic representations (Q1326777) (← links)
• Induction-recursion and initial algebras. (Q1412830) (← links)
• Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
• Detecting equivalence of modular specifications with categorical diagrams (Q1583247) (← links)
• Game semantics for dependent types (Q1641014) (← links)
• A note on the proof theory of the \(\lambda \Pi\)-calculus (Q1891931) (← links)
• The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
• A meaning explanation for HoTT (Q2054122) (← links)
• Univalence and completeness of Segal objects (Q2104885) (← links)
• Semantical analysis of contextual types (Q2200843) (← links)
• Combinatorial structure of type dependency (Q2254771) (← links)
• From signatures to monads in \textsf{UniMath} (Q2319990) (← links)
• Categories with families and first-order logic with dependent sorts (Q2326422) (← links)
• Nominal Lawvere theories: a category theoretic account of equational theories with names (Q2453579) (← links)
• A higher-order calculus and theory abstraction (Q2639838) (← links)
• C-system of a module over a \(Jf\)-relative monad (Q2689172) (← links)
• Theory Presentation Combinators (Q2907324) (← links)
• The Local Universes Model (Q2957763) (← links)
• C-systems defined by universe categories: presheaves (Q2963470) (← links)
• The (Pi,lambda)-structures on the C-systems defined by universe categories (Q2963471) (← links)
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories (Q3007659) (← links)
• Two-dimensional models of type theory (Q3395310) (← links)
• Dependently Sorted Logic (Q3499748) (← links)
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (Q3637183) (← links)
• Weak ω-Categories from Intensional Type Theory (Q3637194) (← links)
• Kripke Semantics for Martin-Löf’s Extensional Type Theory (Q3637199) (← links)
• (Q4510453) (← links)
• (Q4512408) (← links)
• (Q4525557) (← links)
• Internal type theory (Q4647575) (← links)
• Categorical structures for type theory in univalent foundations (Q4683858) (← links)
• Semantics of higher inductive types (Q4958656) (← links)
• Lawvere theories and C-systems (Q4959711) (← links)
• Model structures on categories of models of type theories (Q4961720) (← links)
• Categories with Families: Unityped, Simply Typed, and Dependently Typed (Q5014596) (← links)
• The Interpretation Lifting Theorem for C-Systems (Q5025082) (← links)
• (Q5028425) (← links)
• Hom weak ω-categories of a weak ω-category (Q5058363) (← links)