Higher Homotopies in a Hierarchy of Univalent Universes

Abstract

For Martin-Löf type theory with a hierarchy U 0 :U 1 :U 2 :… of univalent universes, we show that U n 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, U n is such a type if we restrict it to n -types.

Document Details

Document Type
Pub Defense Publication
Publication Date
Mar 21, 2015
Source ID
10.1145/2729979

Entities

People

  • Christian Sattler
  • Nicolai Kraus

Organizations

  • Air Force Research Laboratory
  • University of Nottingham

Tags

Fields of Study

  • Mathematics

Readers

  • Finite Element Method (FEM) for solving Partial Differential Equations (PDEs)
  • Quantum Chemistry
  • Theoretical Analysis.