scientific article; zbMATH DE number 1241699
From MaRDI portal
Publication:4225149
zbMath0919.68083MaRDI QIDQ4225149
Publication date: 18 January 1999
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Categorical structures for type theory in univalent foundations, A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory, Games for Dependent Types, Cubical methods in homotopy type theory and univalent foundations, A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types, Constructive sheaf models of type theory, On generalized algebraic theories and categories with families, Martin-Löf complexes, Combinatorial realizability models of type theory, Dependently Sorted Logic, Unnamed Item, The Local Universes Model, Reduction Free Normalisation for a proof irrelevant type of propositions, Two-level type theory and applications, Canonicity and homotopy canonicity for cubical type theory, C-system of a module over a \(Jf\)-relative monad, Semantical analysis of contextual types, Induction-recursion and initial algebras., Inductively generated formal topologies., Unnamed Item, Unnamed Item, A presheaf model of parametric type theory, Unnamed Item, Denotational semantics for guarded dependent type theory, Graded modal dependent type theory, Univalent polymorphism, Internal type theory, Conservativity of equality reflection over intensional type theory, For Finitary Induction-Induction, Induction is Enough, 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, A dependent type theory with abstractable names, Syntactic approaches to opetopes, 2-Dimensional Directed Type Theory, Cubical Type Theory: a constructive interpretation of the univalence axiom, Unnamed Item, Unnamed Item, The simplicial model of univalent foundations (after Voevodsky), Type Theory Should Eat Itself, Dependent Types and Fibred Computational Effects, Modal dependent type theory and dependent right adjoints, Kripke Semantics for Martin-Löf’s Extensional Type Theory, On the strength of dependent products in the type theory of Martin-Löf, Unnamed Item, Unnamed Item, The universal exponentiable arrow, Categories with families and first-order logic with dependent sorts, Safe recursion with higher types and BCK-algebra, Models of Type Theory Based on Moore Paths, Containers: Constructing strictly positive types, Unnamed Item, Type Theory and Homotopy, Natural models of homotopy type theory, Model structure on the universe of all types in interval type theory
