search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25 stars 5 forks source link

Alt Binary Product of Categories #30

Closed maxsnew closed 1 year ago

maxsnew commented 1 year ago

Recording what needs to be done as I don't have time to work on it for a few days. If someone wants to pick this up I wouldn't mind. Currently this is in Cubical.Categories.Constructions.BinProduct.AsLeftAdjoint.

The medium term goal of these changes is to get a better definition of the exponential functor. To do that we need to

  1. Change the definitions in this module (https://github.com/maxsnew/multi-poly-cats/blob/main/Cubical/Categories/Limits/BinProduct/More.agda#L48) to use the alt binary product
  2. Change this definition (https://github.com/maxsnew/multi-poly-cats/blob/main/Cubical/Categories/Exponentials.agda#L31) to use the alt binary product.
  3. See if this gives us the "most natural" definition of the functorial action of exponentials.

I think (1) can be implemented already with what I've defined. For (2) I think we will need something like the following:

  1. Define an associativity AssocBif : Bifunctor (C ×C D) D' E →Bifunctor C (D ×C D') E of bifunctors with respect to the alt binary product
  2. Probably define a functor showing ^op commutes with the alt bin product. This is sort of definitional for the ordinary bin product but not at all for this alt one.

Also what's a better name for it? I called it AsLeftAdjoint but I think that doesn't really capture it anymore.

maxsnew commented 1 year ago

I've already defined the functor from the usual cartesian product to the alt product but it's on a machine at home. I'll push it later

maxsnew commented 1 year ago

Completed in ead56bb157121d142c6bfa1ad53a22c0fa651fa5. It worked too yay