RS17, Proposition 9.10.

[robin-carlier]

I noticed Proposition 9.10 was stated in the exposition but not formalized.

The proof is split between has-initial-tot-is-representable-family-is-segal and has-initial-tot-is-representable-family-is-segal. I also added a helper lemma that states that equivalences map initial objects to initial objects (as well as its dual for final objects).

This closes #21.

[emilyriehl]

@fizruk can you remind me (and @robin-carlier) how the user can do this fix:

Checking formatting...
[warn] src/simplicial-hott/09-yoneda.rzk.md
[warn] Code style issues found in the above file. Run Prettier with --write to fix.

[emilyriehl]

@robin-carlier thanks for the contribution. Perhaps you could add a sentence or two in markdown before each of your main lemmas explaining the idea of the proof? But once that and minor formatting issues are fixed, we can merge.

[robin-carlier]

@fizruk can you remind me (and @robin-carlier) how the user can do this fix:

Checking formatting...
[warn] src/simplicial-hott/09-yoneda.rzk.md
[warn] Code style issues found in the above file. Run Prettier with --write to fix.

Installing prettier (via npm for me) and running prettier --write **/*.{md,json,yaml,yml} seemed to do the trick.

[emilyriehl]

Looks good.