Trinitarianism

• Overview
  • Terms and Types
  • Non-dependent Types
  • Dependent Types
  • What is ‘the Same’?
• Quest 0 - Terms and Types
  • Part 0 - True / Unit / Terminal object
  • Part 1 - False / Empty / Initial object
  • Part 2 - The natural numbers
  • Part 3 - Universes
• Quest 1 - Dependent Types
  • Part 0 - Predicates / Dependent Constructions / Bundles
  • Part 1 - Interpretations of Bundles
  • Part 2 - Using the Trinitarianism
• Quest 2 - Sigma Types
  • Part 0 - Existence / Dependent Pair / Total Space of Bundles
  • Part 1 - Making terms in Sigma Types
  • Part 2 - Using Terms in Sigma Types
• Quest 2 - Side Quests
  • A Tautology / Currying / Cartesian Closed
• Quest 3 - Pi Types
  • Part 0 - Defining Addition
  • Part 1 - The Statement
  • Part 2 - Remarks
• Quest 3 - Side Quests
  • Decidability of isEven
• Quest 4 - Paths and Equality
  • Part 0 - The Identity Type
  • Part 1 - The Path Space
  • Part 2 - Properties of the Path Space
  • Part 3 - Univalence
• Quest 4 - Side Quests
  • Functional Extensionality
  • Justifying J
• Quest 5 - Dependent Paths
  • Part 0 - A motivating example
  • Part 1 - Dependent Paths
  • Part 2 - How pathToFun Interacts with Other Types