Displayed Category Constructions

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

441 stars 134 forks source link

Displayed Category Constructions #1108

Closed stschaef closed 1 month ago

stschaef commented 4 months ago

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

felixwellen commented 4 months ago

@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...

mortberg commented 4 months ago

@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...

ecavallo commented 4 months ago

Same here, I don't know the problem.

stschaef commented 4 months ago

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

ecavallo commented 4 months ago

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

stschaef commented 4 months ago

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

stschaef commented 3 months ago

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

maxsnew commented 2 months ago

@felixwellen anything we can do to move this along?