scientific article; zbMATH DE number 1302059
From MaRDI portal
Publication:4247303
zbMath0930.03089MaRDI QIDQ4247303
Martin Hofmann, Thomas Streicher
Publication date: 15 February 2000
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
constructive type theoryequalityidentity setscategory-theoretic semanticstranslation functioncountermodelcanonical objectsdependent function spacesderivability of UIP in pure type theorygroupoid interpretationintensional Martin-Löf type theoryuniqueness of identity proofs
Related Items (67)
Homotopies in Grothendieck fibrations ⋮ Category theory, logic and formal linguistics: some connections, old and new ⋮ Modeling Martin-Löf type theory in categories ⋮ A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory ⋮ Unnamed Item ⋮ A characterisation of elementary fibrations ⋮ The intrinsic topology of Martin-Löf universes ⋮ Towards a directed homotopy type theory ⋮ Bicategories in univalent foundations ⋮ Data Types with Symmetries and Polynomial Functors over Groupoids ⋮ Hom weak ω-categories of a weak ω-category ⋮ Game semantics for dependent types ⋮ Univalent completion ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ Martin Hofmann’s contributions to type theory: Groupoids and univalence ⋮ Elementary fibrations of enriched groupoids ⋮ The genesis of the groupoid model ⋮ Martin-Löf complexes ⋮ Combinatorial realizability models of type theory ⋮ Unnamed Item ⋮ Observability in the univalent universe ⋮ Homotopy type theory in Lean ⋮ Meaning explanations at higher dimension ⋮ Naïve Type Theory ⋮ A Comparison of Type Theory with Set Theory ⋮ A formal logic for formal category theory ⋮ The Local Universes Model ⋮ Martin-Löf identity types in C-systems ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Unnamed Item ⋮ Game semantics of Martin-Löf type theory ⋮ Leibniz equality is isomorphic to Martin-Löf identity, parametrically ⋮ Univalent foundations as structuralist foundations ⋮ The calculus of dependent lambda eliminations ⋮ Unnamed Item ⋮ On a possible application of the homotopy concept to model theory ⋮ Unnamed Item ⋮ Proof-relevance of families of setoids and identity in type theory ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Constructing a universe for the setoid model ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ Homotopy-Theoretic Models of Type Theory ⋮ The category of equilogical spaces and the effective topos as homotopical quotients ⋮ Constructions of categories of setoids from proof-irrelevant families ⋮ Univalence in locally Cartesian closed categories ⋮ The identity type weak factorisation system ⋮ 2-Dimensional Directed Type Theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Type theories, toposes and constructive set theory: Predicative aspects of AST ⋮ Univalence as a principle of logic ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ The justification of identity elimination in Martin-Löf's type theory ⋮ Semantics of higher inductive types ⋮ Isomorphism is equality ⋮ Weak ω-Categories from Intensional Type Theory ⋮ On the strength of dependent products in the type theory of Martin-Löf ⋮ Preface: Special issue on homotopy type theory and univalent foundations ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Heterogeneous Substitution Systems Revisited ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Type Theory and Homotopy ⋮ HOMOTOPY MODEL THEORY ⋮ MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
This page was built for publication:
