Pages that link to "Item:Q3325725"

The following pages link to Locally cartesian closed categories and type theory (Q3325725):

Displaying 50 items.

• A constructive manifestation of the Kleene-Kreisel continuous functionals (Q290639) (← links)
• Martin-Löf complexes (Q385803) (← links)
• Totality in arena games (Q636307) (← links)
• A note on inconsistencies caused by fixpoints in a cartesian closed category (Q749648) (← links)
• Categorical and algebraic aspects of Martin-Löf type theory (Q750438) (← links)
• Alpha conversion, conditions on variables and categorical logic (Q913792) (← links)
• A note on Russell's paradox in locally Cartesian closed categories (Q914668) (← links)
• The identity type weak factorisation system (Q959823) (← links)
• The proof monad (Q974136) (← links)
• A minimalist two-level foundation for constructive mathematics (Q1032635) (← links)
• Algebra of constructions. I. The word problem for partial algebras (Q1107515) (← links)
• A small complete category (Q1112159) (← links)
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558) (← links)
• Comprehension categories and the semantics of type dependency (Q1208414) (← links)
• A natural semantics of first-order type dependency (Q1314402) (← links)
• On the semantics of the universal quantifier (Q1371430) (← links)
• Induction-recursion and initial algebras. (Q1412830) (← links)
• Wellfounded trees in categories (Q1577483) (← links)
• Cartesian logic (Q1605480) (← links)
• The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
• Axiomatic reals and certified efficient exact real computation (Q2148797) (← links)
• Composition of deductions within the propositions-as-types paradigm (Q2228351) (← links)
• Revisiting the categorical interpretation of dependent type theory (Q2253180) (← links)
• Containers: Constructing strictly positive types (Q2566024) (← links)
• A higher-order calculus and theory abstraction (Q2639838) (← links)
• Classifying categories for partial equational logic (Q2842828) (← links)
• Logic in Category Theory (Q2909761) (← links)
• Homotopy type theory and Voevodsky’s univalent foundations (Q2933829) (← links)
• The Local Universes Model (Q2957763) (← links)
• The (Pi,lambda)-structures on the C-systems defined by universe categories (Q2963471) (← links)
• Homotopy-Theoretic Models of Type Theory (Q3007656) (← links)
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories (Q3007659) (← links)
• A homotopy-theoretic model of function extensionality in the effective topos (Q3119466) (← links)
• European Summer Meeting of the Association for Symbolic Logic, Uppsala 1991 (Q3138023) (← links)
• Data Types with Symmetries and Polynomial Functors over Groupoids (Q3178294) (← links)
• (Q3201049) (← links)
• Two-dimensional models of type theory (Q3395310) (← links)
• Homotopy theoretic models of identity types (Q3598111) (← links)
• Three extensional models of type theory (Q3625679) (← links)
• Kripke Semantics for Martin-Löf’s Extensional Type Theory (Q3637199) (← links)
• Categorical semantics for higher order polymorphic lambda calculus (Q3783264) (← links)
• (Q3986546) (← links)
• Dependence and independence results for (impredicative) calculi of dependent types (Q4006238) (← links)
• Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions (Q4279249) (← links)
• (Q4510453) (← links)
• (Q4512408) (← links)
• (Q4525557) (← links)
• (Q4555336) (← links)
• Internal type theory (Q4647575) (← links)
• A category-theoretic account of program modules (Q4713399) (← links)