Higher Homotopies in a Hierarchy of Univalent Universes

Nicolai Kraus; Christian Sattler

doi:10.1145/2729979

Higher Homotopies in a Hierarchy of Univalent Universes

Nicolai Kraus, Christian Sattler

Computer Science

Research output: Contribution to journal › Article › peer-review

7 Citations (Scopus)

Abstract

For Martin-Lof type theory with a hierarchy U₀ : U₁ : U₂ : . . . of univalent universes, we show that U_nis not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher inductive types. In particular, Un is such a type if we restrict it to n-types.
We have fully formalized and verified our results within the dependently typed language and proof assistant Agda.

Original language	English
Article number	18
Number of pages	12
Journal	ACM Transactions on Computational Logic
Volume	16
Issue number	2
DOIs	https://doi.org/10.1145/2729979
Publication status	Published - Apr 2015

Keywords

Homotopy type theory
loop spaces
truncation levels
univalent universes

Access to Document

10.1145/2729979Licence: None: All rights reserved

https://doi.org/10.1145/2729979Licence: None: All rights reserved

Cite this

@article{7d9bfaba46ec463894b28fb6b9b3dfd0,

title = "Higher Homotopies in a Hierarchy of Univalent Universes",

abstract = "For Martin-Lof type theory with a hierarchy U0 : U1 : U2 : . . . of univalent universes, we show that Un is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher inductive types. In particular, Un is such a type if we restrict it to n-types.We have fully formalized and verified our results within the dependently typed language and proof assistant Agda.",

keywords = "Homotopy type theory, loop spaces, truncation levels, univalent universes",

author = "Nicolai Kraus and Christian Sattler",

year = "2015",

month = apr,

doi = "10.1145/2729979",

language = "English",

volume = "16",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery (ACM)",

number = "2",

}

TY - JOUR

T1 - Higher Homotopies in a Hierarchy of Univalent Universes

AU - Kraus, Nicolai

AU - Sattler, Christian

PY - 2015/4

Y1 - 2015/4

N2 - For Martin-Lof type theory with a hierarchy U0 : U1 : U2 : . . . of univalent universes, we show that Un is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher inductive types. In particular, Un is such a type if we restrict it to n-types.We have fully formalized and verified our results within the dependently typed language and proof assistant Agda.

AB - For Martin-Lof type theory with a hierarchy U0 : U1 : U2 : . . . of univalent universes, we show that Un is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without using higher inductive types. In particular, Un is such a type if we restrict it to n-types.We have fully formalized and verified our results within the dependently typed language and proof assistant Agda.

KW - Homotopy type theory

KW - loop spaces

KW - truncation levels

KW - univalent universes

U2 - 10.1145/2729979

DO - 10.1145/2729979

M3 - Article

SN - 1529-3785

VL - 16

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 2

M1 - 18

ER -

Higher Homotopies in a Hierarchy of Univalent Universes

Abstract

Keywords

Access to Document

Fingerprint

Cite this