scientific article; zbMATH DE number 6694181
From MaRDI portal
Publication:2968413
Recommendations
- A cubical model of homotopy type theory
- Nominal presentation of cubical sets models of type theory
- Axioms for modelling cubical type theory in a topos
- scientific article; zbMATH DE number 7003193
- Unifying Cubical Models of Univalent Type Theory
- Cubical type theory: a constructive interpretation of the univalence axiom
- On higher inductive types in cubical type theory
- Syntax and models of Cartesian cubical type theory
- Type theories from Barendregt's cube for theorem provers
- Combinatorial realizability models of type theory
Cited in
(85)- Game semantics for dependent types
- 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
- Combinatorial topology and constructive mathematics
- A cubical model of homotopy type theory
- The Frobenius condition, right properness, and uniform fibrations
- A meaning explanation for HoTT
- Rensets and renaming-based recursion for syntax with bindings
- Finitary higher inductive types in the groupoid model
- The construction of set-truncated higher inductive types
- Constructing a universe for the setoid model
- A Kripke model for simplicial sets
- The univalence axiom in cubical sets
- Canonicity for cubical type theory
- Some Wellfounded Trees in UniMath
- Parametric Polymorphism — Universally
- Notions of anonymous existence in Martin-Löf type theory
- A homotopy-theoretic model of function extensionality in the effective topos
- The Cayley-Dickson construction in homotopy type theory
- Cubical (, p)-categories
- Natural models of homotopy type theory
- Proof-Relevant Parametricity
- From mathesis universalis to provability, computability, and constructivity
- Games for dependent types
- Towards a cubical type theory without an interval
- Cubical type theory: a constructive interpretation of the univalence axiom
- Functional Kan simplicial sets: non-constructivity of exponentiation
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Models of type theory based on Moore paths
- An introduction to univalent foundations for mathematicians
- From multisets to sets in homotopy type theory
- Constructing higher inductive types as groupoid quotients
- Internal universes in models of homotopy type theory
- Model structure on the universe of all types in interval type theory
- Syntax and models of Cartesian cubical type theory
- Internal parametricity for cubical type theory
- Canonicity and homotopy canonicity for cubical type theory
- Cubical methods in homotopy type theory and univalent foundations
- Naive cubical type theory
- Languages of higher-dimensional automata
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Homotopy canonicity for cubical type theory
- Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
- A cubical language for Bishop sets
- Models of Type Theory Based on Moore Paths
- The law of excluded middle in the simplicial model of type theory
- Denotational semantics for guarded dependent type theory
- Stack semantics of type theory
- On higher inductive types in cubical type theory
- Partial univalence in n-truncated type theory
- Proof theory of constructive systems: inductive types and univalence
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY
- Nominal presentation of cubical sets models of type theory
- Axioms for modelling cubical type theory in a topos
- Varieties of cubical sets
- Adjoint logic with a 2-category of modes
- Eliminating dependent pattern matching without K
- Homotopical patch theory
- Universal properties for universal types in bifibrational parametricity
- A presheaf model of parametric type theory
- Bifibrational functorial semantics of parametric polymorphism
- Decomposing the univalence axiom
- scientific article; zbMATH DE number 7779294 (Why is no real title available?)
- Higher Structures in Homotopy Type Theory
- From cubes to twisted cubes via graph morphisms in type theory
- Rensets and renaming-based recursion for syntax with bindings extended version
- Martin-Löf identity types in C-systems
- Two-level type theory and applications
- Towards a constructive simplicial model of Univalent Foundations
- Transpension: the right adjoint to the Pi-type
- Kripke-Joyal forcing for type theory and uniform fibrations
- Single-set cubical categories and their formalisation with a proof assistant
- Examples and cofibrant generation of effective Kan fibrations
- A normalizing computation rule for propositional extensionality in higher-order minimal logic
- A sound and complete substitution algorithm for multimode type theory
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- A parametricity-based formalization of semi-simplicial and semi-cubical sets
- The RedPRL proof assistant (invited paper)
- Primitive recursive dependent type theory
- The univalence principle
- The equivariant model structure on cartesian cubical sets
- Separating path and identity types in presheaf models of univalent type theory
- A 2-categorical approach to the semantics of dependent type theory with computation axioms
- Cubical models of -presheaves and the Bousfield-Kan formula
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 Q2968413)
