Fernando Chu comments

Results 16 comments of


                                            Fernando Chu

how can this be run on non-nixos-plattforms?

You only need nix, not nixos. See the official page for guidance https://nixos.org/download.html

Clarification of the proof of Lemma 6.2.9. (universal property of the circle)

I've been thinking about this, and doing path induction on `p` and `eqf` in `(ap φ p)⁻¹ ∙ eqf = eqg` simplifies the goal to `refl (φ f) ≡ eqg`,...

Clarification of the proof of Lemma 6.2.9. (universal property of the circle)

Thanks, you're right. I've been thinking about this. We can not induct on `p` but we can induct on `eqg`, it is also enough to prove it for the case...

Clarification of the proof of Lemma 6.2.9. (universal property of the circle)

Yup I definetely agree, managing 2-paths is still very hard (to me). I suggest again maybe changing to the usual quasi-inverses proof, I can PR if you want.

Clarification of the proof of Lemma 6.2.9. (universal property of the circle)

I've just finished it! (I've also formalized it in [my agda repo](https://github.com/shiranaiyo/HoTT-Book-Agda/blob/b0a6ea213f29b1b991ccffa9adfcade23eb725a2/src/Chapter6/Book.lagda.md#L122)). I'll be closing this issue :) Thank you!

Clarification of the proof of Lemma 6.2.9. (universal property of the circle)

Oh I didn't know, thanks for reopening then

Migrate to TypeScript

Same here :)

"Encountered two children with the same key"

Same thing happens to me, though it seems only when I use sizes/breakpoints

Assumption that `A // R` is a set

Actually, you're right. I meant that the required properties were not introduced, but they were if you count the exercises, with the exception that `Prop` is a set, but that's...

Assumption that `A // R` is a set

I mistook `Prop` being a set with `isProp` being a set. The latter is easy, but the former does not seem so (to me), and that's what we need here....