Literature overview for Introduction to Homotopy Type Theory

[VojtechStep]

The plan for this PR is to contain as much of Part 1 of the book as possible (that's chapters 1 to 8).

Typos/potential oversights found during transcription:

• Page 51, Exercise 5.8 (b), fourth equation: y * succ y should be x * succ y
• Page 60, Exercise 6.1 (b), multiplication is denoted by juxtaposition instead of ·
• Page 83, Definition 8.2.1, "collatz" is spelled in lowercase in the definition but capitalized in Remark 8.2.2
• Page 86, Corollary 8.2.5, upper bounds of families are only defined later in Definition 8.3.1
• Page 96, Exercise 8.8, proving decidable equality in sigma types uses Hedberg's theorem (Theorem 12.3.5) and characterization of identifications of dependent pair types (Theorem 9.3.4). Is there supposed to be an alternative lower-tech proof?
• Page 96, Exercise 8.9 (b), showing decidable equality of dependent functions sounds like it would need function extensionality (Axiom 13.1.3)

[VojtechStep]

Note that the PR is a draft, prose will be added to explain differences between the book and the library.

[fredrik-bakke]

Ah, thanks for the reminder, I didn't notice it was a draft.

[VojtechStep]

I'm opening this to review. I don't plan on formalizing the missing exercises. I included some anonymous definitions to bundle up implications into logical equivalences, since that's what the book exercises call for, but we don't really keep logical equivalences around. Let me know if we want those in the main corpus and I should name and move them.

@EgbertRijke I basically proof-read Part 1 of Intro to HoTT and noticed some typos/potential oversights, which I recorded in the PR description for now.

@fredrik-bakke could you explain the synthetic-homotopy-theory label?

[fredrik-bakke]

@fredrik-bakke could you explain the synthetic-homotopy-theory label?

Sorry, I initially thought the overview would contain parts of the second half of Egbert's book, where I believe he does some synthetic homotopy theory. Please adjust the labels to your liking.

[EgbertRijke]

Thank you for proof-reading the book. I will incorporate your suggestions in the final version.