Fundamental Group of the Circle

• Overview
• Quest 0 - Working with the Circle
  • Part 0 - The Circle
  • Part 1 - Refl ≡ loop is empty
  • Part 2 - Defining flipPath via Univalence
  • Part 3 - Lifting paths using doubleCover
• Quest 0 - Side Quests
  • Different notions of “empty”
  • Proving true≢false
  • Defining cong
• Quest 1 - Loop Space of the Circle
  • Part 0 - Definition of the Loop Space
  • Part 1 - Making a Path From ℤ to Itself
  • Part 2 - Winding Number
• Quest 2 - ℤ is a Set
  • Part 0 - loopSpace loopSpace
  • Part 1 - ℤ as a disjoint sum ℕ ⊔ ℕ
  • Part 2 - Disjoint Sum of Sets is a Set
  • Part 3 - Path Space of Disjoint Sums
  • Part 4 - Proving Path≡⊔NoConfusion
  • Part 5 - Using the Propositional Perspective
• Quest 3 - The Loop Space is ℤ
  • Part 0 - rewind
  • Part 1 - rewind is a right inverse
  • Part 2 - rewind is a left inverse
  • Part 3 - The Loop Space is ℤ