The following pages link to Internal type theory (Q4647575):
Displaying 50 items.
- A constructive manifestation of the Kleene-Kreisel continuous functionals (Q290639) (← 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)
- A minimalist two-level foundation for constructive mathematics (Q1032635) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Game semantics for dependent types (Q1641014) (← links)
- Fibrational modal type theory (Q1744413) (← links)
- Univalent polymorphism (Q1987219) (← links)
- The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
- Finitary higher inductive types in the groupoid model (Q2130587) (← links)
- Semantical analysis of contextual types (Q2200843) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- Revisiting the categorical interpretation of dependent type theory (Q2253180) (← links)
- Combinatorial structure of type dependency (Q2254771) (← links)
- Guarded cubical type theory (Q2319985) (← links)
- Categories with families and first-order logic with dependent sorts (Q2326422) (← links)
- Canonicity and normalization for dependent type theory (Q2422026) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- Natural models of homotopy type theory (Q3130300) (← links)
- Cubical Type Theory: a constructive interpretation of the univalence axiom (Q4580226) (← links)
- (Q4611379) (← links)
- Models of type theory based on Moore paths (Q4611383) (← links)
- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids (Q4647569) (← links)
- Conservativity of equality reflection over intensional type theory (Q4647577) (← links)
- Categorical structures for type theory in univalent foundations (Q4683858) (← links)
- Lawvere theories and C-systems (Q4959711) (← links)
- Model structures on categories of models of type theories (Q4961720) (← links)
- Internal universes in models of homotopy type theory (Q4993352) (← links)
- (Q4993353) (← links)
- Categories with Families: Unityped, Simply Typed, and Dependently Typed (Q5014596) (← links)
- The Interpretation Lifting Theorem for C-Systems (Q5025082) (← links)
- Canonicity and homotopy canonicity for cubical type theory (Q5028486) (← links)
- Cubical methods in homotopy type theory and univalent foundations (Q5055493) (← links)
- On Church’s thesis in cubical assemblies (Q5055494) (← links)
- Bicategories in univalent foundations (Q5055496) (← links)
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types (Q5056372) (← links)
- An interpretation of dependent type theory in a model category of locally cartesian closed categories (Q5076386) (← links)
- Constructive sheaf models of type theory (Q5084309) (← links)
- On generalized algebraic theories and categories with families (Q5084311) (← links)
- (Q5089004) (← links)
- (Q5089011) (← links)
- Pointers in Recursion: Exploring the Tropics (Q5089027) (← links)
- (Q5089034) (← links)
- (Q5091148) (← links)
- Models of Type Theory Based on Moore Paths (Q5111326) (← links)
- Denotational semantics for guarded dependent type theory (Q5139284) (← links)
- (Q5141620) (← links)
- (Q5155672) (← links)
- LF+ in Coq for "fast and loose" reasoning (Q5210657) (← links)
