scientific article; zbMATH DE number 6748870

DOI10.4230/LIPIcs.CSL.2016.21zbMath1370.03014arXiv1604.03799MaRDI QIDQ5278407

Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus

Publication date: 19 July 2017

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

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

zbMATH Keywords

homotopy type theorycoherenceshomotopy type systemstrict equality

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Related Items (9)

A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ Finitary type theories with and without contexts ⋮ A formal logic for formal category theory ⋮ A general framework for the semantics of type theory ⋮ Two-level type theory and applications ⋮ Unnamed Item ⋮ Cartesian cubical computational type theory: Constructive reasoning with paths and equalities ⋮ Model structure on the universe of all types in interval type theory ⋮ A rewriting coherence theorem with applications in homotopy type theory

This page was built for publication: