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