The following pages link to (Q2968413):
Displaying 50 items.
- Game semantics for dependent types (Q1641014) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- Univalent foundations as structuralist foundations (Q1708879) (← links)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (Q1731963) (← links)
- Combinatorial topology and constructive mathematics (Q1788338) (← links)
- A cubical model of homotopy type theory (Q1799035) (← links)
- The Frobenius condition, right properness, and uniform fibrations (Q2013548) (← links)
- A meaning explanation for HoTT (Q2054122) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Finitary higher inductive types in the groupoid model (Q2130587) (← links)
- The construction of set-truncated higher inductive types (Q2133178) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- A Kripke model for simplicial sets (Q2257308) (← links)
- The univalence axiom in cubical sets (Q2319981) (← links)
- Canonicity for cubical type theory (Q2319982) (← links)
- Some Wellfounded Trees in UniMath (Q2819193) (← links)
- Parametric Polymorphism — Universally (Q2947462) (← links)
- A homotopy-theoretic model of function extensionality in the effective topos (Q3119466) (← links)
- (Q3121020) (← links)
- Cubical $(\omega,p)$-categories (Q3121024) (← links)
- Natural models of homotopy type theory (Q3130300) (← links)
- Proof-Relevant Parametricity (Q3188282) (← links)
- From Mathesis Universalis to Provability, Computability, and Constructivity (Q3305633) (← links)
- Games for Dependent Types (Q3449463) (← links)
- Towards a Cubical Type Theory without an Interval (Q4580224) (← links)
- Cubical Type Theory: a constructive interpretation of the univalence axiom (Q4580226) (← links)
- Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation (Q4580229) (← links)
- (Q4611379) (← links)
- (Q4611383) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- (Q4989403) (← links)
- (Q4993352) (← links)
- Model structure on the universe of all types in interval type theory (Q5022925) (← links)
- Syntax and models of Cartesian cubical type theory (Q5022926) (← links)
- (Q5028425) (← links)
- Canonicity and homotopy canonicity for cubical type theory (Q5028486) (← links)
- Cubical methods in homotopy type theory and univalent foundations (Q5055493) (← links)
- Naive cubical type theory (Q5055495) (← links)
- Languages of higher-dimensional automata (Q5076390) (← links)
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities (Q5079726) (← links)
- (Q5089011) (← links)
- (Q5091148) (← links)
- (Q5094128) (← links)
- Models of Type Theory Based on Moore Paths (Q5111326) (← links)
- Denotational semantics for guarded dependent type theory (Q5139284) (← links)
- Proof Theory of Constructive Systems: Inductive Types and Univalence (Q5214792) (← links)
- UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY (Q5241229) (← links)
- Varieties of Cubical Sets (Q5283204) (← links)
- Adjoint Logic with a 2-Category of Modes (Q5283430) (← links)
- Eliminating dependent pattern matching without K (Q5371975) (← links)
