scientific article; zbMATH DE number 2079044
From MaRDI portal
Publication:4474857
zbMath1044.03544MaRDI QIDQ4474857
Publication date: 21 July 2004
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)
Related Items
Modeling Martin-Löf type theory in categories, AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS, A constructive manifestation of the Kleene-Kreisel continuous functionals, Cubical methods in homotopy type theory and univalent foundations, Axiomatic reals and certified efficient exact real computation, An interpretation of dependent type theory in a model category of locally cartesian closed categories, Homotopy type theory and Voevodsky’s univalent foundations, On generalized algebraic theories and categories with families, Non-well-founded trees in categories, The Local Universes Model, A general framework for the semantics of type theory, Towards a constructive simplicial model of Univalent Foundations, Unnamed Item, Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets, Denotational semantics for guarded dependent type theory, EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS, The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, The identity type weak factorisation system, The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective, Revisiting the categorical interpretation of dependent type theory, Combinatorial structure of type dependency, The simplicial model of univalent foundations (after Voevodsky), Dependent Types and Fibred Computational Effects, Modal dependent type theory and dependent right adjoints, Kripke Semantics for Martin-Löf’s Extensional Type Theory, A minimalist two-level foundation for constructive mathematics, Joyal's arithmetic universes via type theory, Wellfounded trees in categories, Containers: Constructing strictly positive types, Type Theory and Homotopy, Natural models of homotopy type theory, Categories with Families: Unityped, Simply Typed, and Dependently Typed, MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
