Alternate Definitions of Displayed Cats + Profunctor Homomorphism Stuff + Ends

[maxsnew]

This one is a bit of a grab bag of what I've been hacking on for a while, sorry for the mess.

1. A few experimental definitions related to displayed categories and fibers:
   • Displayed.Alt.Fibrous is an alternate definition of displayed category that includes a definition of the vertical category over an object.
   • Displayed.Alt.LevelPoly is an alternate definition that allows the universe level of the displayed objects to depend on the base. This can be used to define e.g., a displayed category of sets over the indiscrete category of universe levels. Ended up defining Indiscrete category as a helper here.
   • Cubical.Categories.Constructions.Fiber is an alternate definition of the fiber of a displayed category that tries to avoid transports: it defines a vertical morphism to be a displayed morphism that is over an object that is equal to the identity. I don't think this is actually that useful. Ended up defining Endo and ChangeOfObjects as helper constructions here.
2. A bunch of stuff about profunctor homomorphisms and natural elements that was originally part of Displayed.Alt.Fibrous until I realized it was unnecessary
   • Definitions of unary homomorphisms, bilinear homomorphisms and nullary homomorphisms (aka natural elements) of relators
   • categories of Profunctors and Relators
   • the universal property of the Hom relator: id is the universal natural element of an endo-relator
   • some convenient notation and proofs for Relators
3. A couple of definitions of universal constructions
   • ends, which uses natural elements in the definition. Based on me trying to give a "compositional" definition rather than the concrete definition @bond15 gave for coends.
   • weighted limits, which can be used to define ends, but not that nicely

I'll squash everything before it gets merged to main

[bond15]

I plan on looking over this after our meeting today