Improve definitional behavior of the category of elements

[jpoiret]

Align with the definition of a fiber to simplify arguments down the line.

I had this lying around, you can see that it removes a bunch of syms just by virtue of using the more widespread direction for equalities that arises from fiber.

[felixwellen]

Needs rebasing

[felixwellen]

Thanks!

[felixwellen]

Looks very good to me -> merging.