scientific article; zbMATH DE number 1302059
From MaRDI portal
Publication:4247303
Recommendations
Cited in
(94)- On the strength of dependent products in the type theory of Martin-Löf
- Game semantics for dependent types
- Univalent completion
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- Univalent foundations as structuralist foundations
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- Univalence as a principle of logic
- The simplicial model of univalent foundations (after Voevodsky)
- A characterisation of elementary fibrations
- Towards a directed homotopy type theory
- Constructing a universe for the setoid model
- The justification of identity elimination in Martin-Löf's type theory
- Preface: Special issue on homotopy type theory and univalent foundations
- On a possible application of the homotopy concept to model theory
- Observability in the univalent universe
- 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
- Canonicity of weak -groupoid laws using parametricity theory
- The intrinsic topology of Martin-Löf universes
- Homotopy type theory and Voevodsky's univalent foundations
- The local universes model: an overlooked coherence construction for dependent type theories
- Idempotents in intensional type theory
- Notions of anonymous existence in Martin-Löf type theory
- Homotopy-theoretic models of type theory
- scientific article; zbMATH DE number 5994829 (Why is no real title available?)
- A homotopy-theoretic model of function extensionality in the effective topos
- Data types with symmetries and polynomial functors over groupoids
- scientific article; zbMATH DE number 4181647 (Why is no real title available?)
- Homotopies in Grothendieck fibrations
- Mathesis Universalis and Homotopy Type Theory
- From mathesis universalis to provability, computability, and constructivity
- Weak ω-Categories from Intensional Type Theory
- Martin-Löf complexes
- Combinatorial realizability models of type theory
- A coherence theorem for Martin-Löf's type theory
- scientific article; zbMATH DE number 2075881 (Why is no real title available?)
- Heterogeneous substitution systems revisited
- Conservativity of equality reflection over intensional type theory
- scientific article; zbMATH DE number 1420784 (Why is no real title available?)
- scientific article; zbMATH DE number 1420788 (Why is no real title available?)
- Semantics of higher inductive types
- Constructing higher inductive types as groupoid quotients
- HOMOTOPY MODEL THEORY
- Internal parametricity for cubical type theory
- The category of equilogical spaces and the effective topos as homotopical quotients
- Bicategories in univalent foundations
- Hom weak ω-categories of a weak ω-category
- Martin Hofmann’s contributions to type theory: Groupoids and univalence
- Elementary fibrations of enriched groupoids
- The genesis of the groupoid model
- Bicategories in univalent foundations
- Cubical syntax for reflection-free extensional equality
- Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
- A cubical language for Bishop sets
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically
- Typal heterogeneous equality types
- Constructions of categories of setoids from proof-irrelevant families
- Eta-rules in Martin-Löf type theory
- Univalence in locally Cartesian closed categories
- Type theory and homotopy
- Generalizations of Hedberg's theorem
- The calculus of dependent lambda eliminations
- 2-Dimensional Directed Type Theory
- MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
- Type theories, toposes and constructive set theory: Predicative aspects of AST
- Naïve Type Theory
- A Comparison of Type Theory with Set Theory
- scientific article; zbMATH DE number 7756115 (Why is no real title available?)
- Elimination of extensionality in Martin-Löf type theory
- A formal logic for formal category theory
- Martin-Löf identity types in C-systems
- On the ∞$\infty$‐topos semantics of homotopy type theory
- Game semantics of Martin-Löf type theory
- Topological quantum gates in homotopy type theory
- Proof-relevance of families of setoids and identity in type theory
- A type theory for strictly unital -categories
- A direct-categorical approach to opetopic sets and opetopes
- Frobenius structure and the Beck-Chevalley condition for algebraic weak factorization systems
- Monoidal closure of Grothendieck constructions via -tractable monoidal structures and Dialectica formulas
- Homotopy.io: a proof assistant for finitely-presented globular n-categories
- The Grothendieck computability model
- Toward a geometry for syntax
- The quantum monadology
- Delooping cyclic groups with lens spaces in homotopy type theory
- Groupoidal realizability for intensional type theory
- The univalence principle
- On different ways of being equal
- Strict universes for Grothendieck topoi
- Synthetic 1-categories in directed type theory
- A 2-categorical approach to the semantics of dependent type theory with computation axioms
- Isomorphism is equality
- The identity type weak factorisation system
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247303)
