scientific article; zbMATH DE number 7359418
From MaRDI portal
Publication:4993352
DOI10.4230/LIPIcs.FSCD.2018.22zbMath1462.03010arXiv1801.07664MaRDI QIDQ4993352
Ian Orton, Daniel R. Licata, Bas Spitters, Andrew M. Pitts
Publication date: 15 June 2021
Full work available at URL: https://arxiv.org/abs/1801.07664
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
universeshomotopy type theoryinternal languagedependent type theorymodalitiescubical setsunivalent foundations
Related Items (20)
Cubical methods in homotopy type theory and univalent foundations ⋮ On Church’s thesis in cubical assemblies ⋮ A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ Normalization by evaluation for modal dependent type theory ⋮ A general framework for the semantics of type theory ⋮ Two-level type theory and applications ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Semantical analysis of contextual types ⋮ Unnamed Item ⋮ Indexed type theories ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory
Uses Software
Cites Work
- Corrections to ``On right adjoints to exponential functors
- Fibrational modal type theory
- The Frobenius condition, right properness, and uniform fibrations
- A judgmental reconstruction of modal logic
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Internal type theory
- Contextual modal type theory
- Varieties of Cubical Sets
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication:
