The following pages link to (Q4225149):
Displaying 50 items.
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory (Q280837) (← links)
- Martin-Löf complexes (Q385803) (← links)
- Combinatorial realizability models of type theory (Q385804) (← links)
- A dependent type theory with abstractable names (Q530845) (← links)
- The identity type weak factorisation system (Q959823) (← links)
- On the strength of dependent products in the type theory of Martin-Löf (Q1024547) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Inductively generated formal topologies. (Q1412832) (← links)
- Safe recursion with higher types and BCK-algebra (Q1577481) (← links)
- Univalent polymorphism (Q1987219) (← links)
- The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
- The universal exponentiable arrow (Q2078410) (← links)
- Semantical analysis of contextual types (Q2200843) (← links)
- Graded modal dependent type theory (Q2233475) (← links)
- Revisiting the categorical interpretation of dependent type theory (Q2253180) (← links)
- Categories with families and first-order logic with dependent sorts (Q2326422) (← links)
- Containers: Constructing strictly positive types (Q2566024) (← links)
- C-system of a module over a \(Jf\)-relative monad (Q2689172) (← links)
- Type Theory Should Eat Itself (Q2804938) (← links)
- Dependent Types and Fibred Computational Effects (Q2811331) (← links)
- Products of families of types and (Pi,lambda)-structures on C-systems (Q2953831) (← links)
- The Local Universes Model (Q2957763) (← links)
- Natural models of homotopy type theory (Q3130300) (← links)
- Games for Dependent Types (Q3449463) (← links)
- Dependently Sorted Logic (Q3499748) (← links)
- Kripke Semantics for Martin-Löf’s Extensional Type Theory (Q3637199) (← links)
- Cubical Type Theory: a constructive interpretation of the univalence axiom (Q4580226) (← links)
- (Q4611379) (← links)
- (Q4611383) (← links)
- Internal type theory (Q4647575) (← links)
- Conservativity of equality reflection over intensional type theory (Q4647577) (← links)
- Categorical structures for type theory in univalent foundations (Q4683858) (← links)
- (Q4993352) (← links)
- Model structure on the universe of all types in interval type theory (Q5022925) (← links)
- (Q5028425) (← links)
- Canonicity and homotopy canonicity for cubical type theory (Q5028486) (← links)
- Cubical methods in homotopy type theory and univalent foundations (Q5055493) (← links)
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types (Q5056372) (← links)
- Constructive sheaf models of type theory (Q5084309) (← links)
- On generalized algebraic theories and categories with families (Q5084311) (← links)
- (Q5089011) (← links)
- (Q5094128) (← links)
- Syntactic approaches to opetopes (Q5094693) (← links)
- Models of Type Theory Based on Moore Paths (Q5111326) (← links)
- Denotational semantics for guarded dependent type theory (Q5139284) (← links)
- (Q5155672) (← links)
- Modal dependent type theory and dependent right adjoints (Q5220184) (← links)
- Type Theory and Homotopy (Q5253928) (← links)
- The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective (Q5415629) (← links)
- 2-Dimensional Directed Type Theory (Q5739362) (← links)
