scientific article; zbMATH DE number 7561492

DOI10.4230/LIPIcs.TYPES.2018.7MaRDI QIDQ5091148

Taichi Uemura

Publication date: 21 July 2022

Full work available at URL: https://arxiv.org/abs/1803.06649

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

univalencerealizabilitycubical type theoryimpredicative universepropositional resizing

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Cubical methods in homotopy type theory and univalent foundations ⋮ On Church’s thesis in cubical assemblies ⋮ On Small Types in Univalent Foundations ⋮ Univalent polymorphism ⋮ Is Impredicativity Implicitly Implicit ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Realizability. An introduction to its categorical side
• The calculus of constructions
• A small complete category
• Comprehension categories and the semantics of type dependency
• Categorical logic and type theory
• The homotopy theory of type theories
• The Frobenius condition, right properness, and uniform fibrations
• The univalence axiom in cubical sets
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• A homotopy-theoretic model of function extensionality in the effective topos
• Constructive natural deduction and its ‘ω-set’ interpretation
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Internal type theory
• Propositions as [Types]
• Impredicative Encodings of (Higher) Inductive Types
• On Higher Inductive Types in Cubical Type Theory
• Modal dependent type theory and dependent right adjoints
• Varieties of Cubical Sets
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Understanding the small object argument

This page was built for publication: