Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Normal forms in cubical type theory

Xu Huang

Abstract

This note documents the specification of normal forms in cubical type theory. The definition is already present in the proof of normalization for cubical type theory, but we present it in a more traditional style explicitly for reference.

Normal forms in cubical type theory

Abstract

This note documents the specification of normal forms in cubical type theory. The definition is already present in the proof of normalization for cubical type theory, but we present it in a more traditional style explicitly for reference.

Paper Structure

This paper contains 15 sections, 11 equations.

Table of Contents

  1. Introduction
  2. Martin-Löf type theory
  3. Π-types
  4. Σ-types
  5. Boolean type
  6. Universes
  7. Cubical type theory
  8. Interval and cofibrations
  9. Cofibration assumptions
  10. Frontier of instability
  11. Composition structure
  12. Weak Booleans
  13. The circle
  14. Glue types
  15. Equality on normal forms

Theorems & Definitions (6)

  • Remark 1
  • Remark 2
  • Remark 3
  • Remark 4
  • Remark 5
  • Remark 6