book

book copied to clipboard

Bumps [peaceiris/actions-gh-pages](https://github.com/peaceiris/actions-gh-pages) from 3 to 4. Release notes Sourced from peaceiris/actions-gh-pages's releases. actions-github-pages v4.0.0 See CHANGELOG.md for more details. actions-github-pages v3.9.3 See CHANGELOG.md for more details. actions-github-pages v3.9.2 See CHANGELOG.md...

dependabot[bot]

Incorrect diagram for Example 8.7.16

1

I don't know anything about CW complexes but I think the diagram should have the left hand arrow in the pushout being `pr₁ : S₁ × 𝕊⁰ → S₁`, and...

roconnor

Exercise 11.6 seems to need WLPO not LPO

3

My metamath contributors and I have formalized, not exactly Exercise 11.6 as stated, but something pretty close. What we have is: * for part (ii) we were able to prove...

jkingdon

max and sup

9

Some people are complaining that the HoTT book uses $\mathsf{max}(x, y)$ to denote the $\mathsf{sup}$ operation in a lattice, and in particular the $\mathsf{sup}$ of two real numbers, whereas in...

ncfavier