Define displayed categories, functors, natural transformations, adjoints

[ecavallo]

Thanks to 1lab for some guidance.

[felixwellen]

@maxsnew can you review this?

[maxsnew]

Looks good to me. The only question I have is about the displayed functors: this formulation is for a functor between displayed categories over a functor between different base categories. Would it be any simpler to have a direct definition of displayed functor where the base category is the same, i.e., equivalent to Functor^D over the identity functor? It would be simpler to formulate in that it involves Path rather than PathP but as long as the current definition simplifies to this one when instantiated with the identity functor it's probably fine.

If this code is copied from the 1lab, we also need to license it under AGPL >= 3.0. But if it's just adapted we don't need to.

[felixwellen]

Thanks for looking into this to @maxsnew and @jpoiret !

Would it be any simpler to have a direct definition of displayed functor where the base category is the same, i.e., equivalent to Functor^D over the identity functor?

I think we can leave this question to the future. I guess it is something that will be decided by usability.

If this code is copied from the 1lab, we also need to license it under AGPL >= 3.0. But if it's just adapted we don't need to.

As we know now, we cannot license things under a GPL here. But in this case, since @ecavallo said it was 'guidance', we should credit the 1lab, but there shouldn't be a licensing issue.

[ecavallo]

I don't see any immediate benefit to a dedicated definition for Functor^D over the identity.

[felixwellen]

Ok, I'm fine with how it is now and it still checks on latest master -> merging.