Higher Homotopies in a Hierarchy of Univalent Universes

DOI10.1145/2729979zbMath1354.03100arXiv1311.4002OpenAlexW2104240658MaRDI QIDQ2957700

Nicolai Kraus, Christian Sattler

Publication date: 27 January 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

loop spaceshomotopy type theorytruncation levelsunivalent universes

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Topological categories, foundations of homotopy theory (55U40)

Related Items (5)

Modalities in homotopy type theory ⋮ Naïve Type Theory ⋮ Higher Structures in Homotopy Type Theory ⋮ Eliminating dependent pattern matching without K ⋮ Univalent polymorphism

Uses Software

• Agda
• GitHub

Cites Work

• The General Universal Property of the Propositional Truncation

This page was built for publication: Higher Homotopies in a Hierarchy of Univalent Universes