type-theory/notes/HLevels.md

Properties

• Theorem 7.1.4:
  • IF: X is an $n$-type
  • IF: X \rightarrow Y is a retraction (has a left-inverse)
  • THEN: Y is an $n$-type
• Corollary 7.1.5:
  • IF: X \simeq Y
  • IF: X is an $n$-type
  • THEN: Y is an $n$-type
• Theorem 7.1.7:
  • IF: X is an $n$-type
  • THEN: it is also an $(n + 1)$-type
• Theorem 7.1.8:
  • IF: A is an $n$-type
  • IF: B(a) is an $n$-type for all a : A
  • THEN: \sum_{(x : A)} B(x) is an $n$-type

-2: Contractible

-1: Mere props

• If A and B are mere props, so is A \times B

• If B(a) is a prop for any a:A, then \prod_{(x:A)} B(x) is a prop