`comp1o` -> `comp1s`

[affeldt-aist]

hierarchy-builder/examples/cat/cat.v

Line 74 in e4e487d

comp1o : forall (a b : C) (f : a ~> b), idmap \; f = f;

because the statement is using the \; (sequence) notation.
comp1o looks like the lemma should be idmap \o f,
this is a bit disturbing

@t6s @shinya-katsumata

[affeldt-aist]

We propose to do either of the following:

1. rename comp into seq in cat.v so that the name better fits the type and the notation (;)

2. change the type so that it fits the name (and then we should use \o instead of ;)

3. is a bit easier to implement but we slightly prefer 2. because it betters fits the conventions in many textbooks (MacLane, Kelly, Kashiwara-Shapira)

moreover, the comp in ssrfun.v has a type different from comp in cat.v

This has an influence on the naming of the lemmas that follow.

Would you accept a PR implementing 2.?

@t6s @shinya-katsumata

[CohenCyril]

Sure. Actually I want both notations, but your naming makes more sense. Beware this is an example file and not a library yet. A proper library will come with algebraic universes.