Presheaves, BinProd, Elements, TwistedArrow, Constant

[anuyts]

Expanding the presheaf library (Cubical.Categories.Presheaf)

[anuyts]

My apologies, this ended up being a mix of only moderately related things:

• I cleaned up the binary product of categories:
  • Renamed it to ×C
  • Added a functor pairing operation and based most other stuff on it
  • Merged the confusing file Categories.Functor.BinProduct into Categories.Constructions.BinProduct
• Categories of elements:
  • I redefined the contravariant version as the opposite of the covariant version; this required splitting it up in two modules,
• Defined the twisted arrow category as the category of elements of the Hom-functor
• Defined constant functors
• Renamed PreShv to PresheafCategory, in contrast to the type of presheaves Presheaf
• Defined non-presheaves together with forgetful, free and cofree functors, but did not prove adjointness.

[maxsnew]

I think if we want a "most general" version of a universal property, a good one to pick in my experience is "representable profunctor", i.e. a profunctor C^o x D -> Set that is equivalent to a composition of Hom with a functor either from C to D or vice-versa. This includes adjoint functors, relative adjoint functors, limits, colimits, Kan extensions etc very directly. I hacked something up here that could be cleaned up and submitted (https://github.com/maxsnew/cubical-cbpv/blob/main/Profunctor.agda).

[anuyts]

@maxsnew I think you probably wanted to post that comment in #873.

[ecavallo]

@mortberg are you going to review this? If not I'll do it

[mortberg]

@mortberg are you going to review this? If not I'll do it

Please do it! I'm way behind on all of my reviewing, so any help is very appreciated!

[ecavallo]

Thanks! I just did some minor cleanup.