Strict segal homotopy category

[gio256]

This PR includes (partial) proofs of the following:

• Two 1-simplices in a StrictSegal simplicial set are homotopic if and only if they are equal.
• The OneTruncation of a StrictSegal simplicial set is a category.

To avoid translating back and forth between paths (defined by directed paths of edges of type X _[1]) and homotopies, I have used the definition of homotopies from mathlib4#10006(comment). This differs slightly from the definition in #51. My tentative plan is to clean up the admitted proofs here, then open a new PR using the definition of homotopies from #51 for comparison.

[gio256]

If anyone needs it, there is a very rough proof of associativity on the branch segal-assoc (more specifically, see this commit).

For now, I am leaving the admitted proof on this branch for a few reasons:

• The proof on the segal-assoc branch is pretty ugly.
• Rather than cleaning it up now, time seems better spent adapting this branch to use the existing definition of the homotopy relations.
• The OneTruncation instance is already quite slow, for reasons that are still a mystery to me.