https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/

Do it in a pull request!

  • Introduction: "which are common place in current mathematical practice" - common-place?
  • Introduction: "half of these notes begin without the univalence axiom" - half cannot begin; also, it says 15 lines up: "we will do a fair amount of univalent mathematics before we formulate or assume the univalence axiom"
  • Homotopy type theory: two paragraphs are essentially duplicates of one another; link to HoTT/UF is broken.
  • Type universes: "given a category in one universe" - in A universe
  • Type universes: "We now bring our notation" - bring IN
  • Universes file:
    • "different ... but closer" - AND closer?
    • "next next type universe universe" - really?
  • The one-element type: "Agda knows 𝓤 is a universe variable because we said so above" - TOLD IT