Internal type theory

DOI10.1007/3-540-61780-9_66zbMath1434.03149OpenAlexW1494555245MaRDI QIDQ4647575

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61780-9_66

zbMATH Keywords

type theory proof assistant dependent type coherence condition equality judgement

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Mechanization of proofs and logical operations (03B35) Special categories (18B99) Type theory (03B38)

Related Items

LF+ in Coq for "fast and loose" reasoning, Categorical structures for type theory in univalent foundations, Finitary higher inductive types in the groupoid model, A constructive manifestation of the Kleene-Kreisel continuous functionals, Cubical methods in homotopy type theory and univalent foundations, On Church’s thesis in cubical assemblies, Bicategories in univalent foundations, A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types, Game semantics for dependent types, From realizability to induction via dependent intersection, Unnamed Item, An interpretation of dependent type theory in a model category of locally cartesian closed categories, Constructive sheaf models of type theory, On generalized algebraic theories and categories with families, Combinatorial realizability models of type theory, Unnamed Item, Unnamed Item, Normalization by evaluation for modal dependent type theory, Canonicity and normalization for dependent type theory, A formal logic for formal category theory, The compatibility of the minimalist foundation with homotopy type theory, The Interpretation Lifting Theorem for C-Systems, Martin-Löf identity types in C-systems, A general framework for the semantics of type theory, Two-level type theory and applications, Monoidal weak ω-categories as models of a type theory, On the ∞$\infty$‐topos semantics of homotopy type theory, Canonicity and homotopy canonicity for cubical type theory, Game semantics of Martin-Löf type theory, Semantical analysis of contextual types, Induction-recursion and initial algebras., Pure type systems with explicit substitutions, Unnamed Item, Unnamed Item, Unnamed Item, Denotational semantics for guarded dependent type theory, Constructing a universe for the setoid model, Fibrational modal type theory, Univalent polymorphism, Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids, Conservativity of equality reflection over intensional type theory, For Finitary Induction-Induction, Induction is Enough, The identity type weak factorisation system, The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective, Revisiting the categorical interpretation of dependent type theory, A dependent type theory with abstractable names, Combinatorial structure of type dependency, Cubical Type Theory: a constructive interpretation of the univalence axiom, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, The simplicial model of univalent foundations (after Voevodsky), Lawvere theories and C-systems, Model structures on categories of models of type theories, Modal dependent type theory and dependent right adjoints, Pointers in Recursion: Exploring the Tropics, A minimalist two-level foundation for constructive mathematics, Guarded cubical type theory, Unnamed Item, Unnamed Item, Unnamed Item, Categories with families and first-order logic with dependent sorts, Models of Type Theory Based on Moore Paths, Unnamed Item, Type Theory and Homotopy, Natural models of homotopy type theory, Categories with Families: Unityped, Simply Typed, and Dependently Typed

Uses Software

LEGO

Cites Work