Functor Comprehension

[stschaef]

Adding a module called Comprehension, and associated dependencies, that provides a method for constructing functors without providing the full functorial structure up front.

That is, say you wish to define a functor F : C → D via some universal property P. Instead of manually constructing the action on objects, morphisms, and proving functoriality, one can instead just give an action on objects and prove the functoriality of the property P.

This is a pretty big PR. I have tried to integrate most of our changes into the appropriate spots so far, and I'll be marking it as a draft until I address these

• Continue renaming and integrating our changes. For instance, the modules that currently end in More
• Considering moving Comprehension.agda back under the Profunctor directory.
• Some dangling TODOs and naming concerns

[stschaef]

Originially we had comprehension under Profunctor rather than Functor, but after looking at the cubical directory structure, I'm thinking it might make more sense to put comprehension underneath Functor.

I'm torn on this though. After all we are constructing a functor, even if the implementation makes use of profunctors

[felixwellen]

I have no opinion on the names so far. If you can do that git-wise, it would be great if you split the PR up by topics - I think a couple of things are happening at once and that makes it harder to review.

[stschaef]

@felixwellen Yeah sorry for the spam, that was moreso to not have to comb through them later.

For splitting up the PR, would you prefer something like rebased commits by topics all in a single PR or distinct PRs?

We have written a big web of mess building up to this comprehension construction, but I think these can be decoupled roughly into

• displayed category additions
• bifunctor additions
• profunctor additions
• the comprehension construction itself

[felixwellen]

If it is easy for you to split it into multiple PRs by topic, that would be great.