cubical Displayed Category Constructions

Meant to be the first thrust of #1106 code as we separate that large hunk of code into modular and manageable PRs

Here we add the following things to reason about displayed categories

displayed full subcategories
displayed preorders
displayed terminal category
displaying a category D over a category C
displayed opposite category and opposite functor
introduction principles to define functors into certain classes of displayed categories. Such as the displayed total category and when a displayed category has prop hom sets
the left adjoint to reindexing

Mar 01 '24 03:03 stschaef

@ecavallo @mortberg does anyone have any idea why the CI is not running? Might be because @stschaef is first-time contributor, but usually there appears some button to run the CI...

Mar 01 '24 09:03 felixwellen

@ecavallo @mortberg does anyone have any idea why the CI is not running? Might be because @stschaef is first-time contributor, but usually there appears some button to run the CI...

Indeed, very strange. I see no button either...

Mar 01 '24 09:03 mortberg

Same here, I don't know the problem.

Mar 01 '24 09:03 ecavallo

Could it be that I'm merging in a branch with a name that isn't master

Mar 01 '24 15:03 stschaef

Now the button to run CI appeared. Not sure what changed, but I clicked it.

Mar 01 '24 16:03 ecavallo

Now the button to run CI appeared. Not sure what changed, but I clicked it.

I pushed another commit to fix a naming typo. Seems like that did the trick

Mar 01 '24 16:03 stschaef

Whitespace is fixed, and the left adjoint has been moved. Should be ready for review

Apr 08 '24 15:04 stschaef