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

Distributive Coproducts #4

Closed maxsnew closed 1 year ago

maxsnew commented 1 year ago
  1. Define coproducts (as dual of products?)
  2. Let C be a cartesian category. A coproduct cocone is distributive if it is preserved by the functor a \times - for every a.
  3. (Stretch) By RAPL: if C is cartesian closed, any coproduct is distributive.
GenericMonkey commented 1 year ago

I started work on this -- got ⊥ᴾ, +ᴾ, and Σᴾ defined cleanly as duals of the analogue definitions in UMP.agda.

Question about unarySum (analogue of UnaryProduct) + product, nestedproduct... etc. -- we want these to be statements about C and not Cop yes? I.e. the IsUniversal should be happening on C? So should a degree of unwrapping should be done for these, or are we content with it IsUniversal in the opposite category?

Also, what exactly to push and preserve do in UMP? looks like they lift a functor to a presheaf homomorphism? What are they used for?

maxsnew commented 1 year ago

Question about unarySum (analogue of UnaryProduct) + product, nestedproduct... etc. -- we want these to be statements about C and not Cop yes? I.e. the IsUniversal should be happening on C? So should a degree of unwrapping should be done for these, or are we content with it IsUniversal in the opposite category?

If we could get away with it, we could just not define any of unarySum, nestedSum etc. Let's try working directly with the definition in terms of product on the opposite category and only redefine things if it gets too complex to keep track of.

push and preserve are there to formalize what it means for a functor to preserve a universal property. For instance preserving products means that the product projections (i.e., the universal "cone") get mapped to product projections/cone in the codomain. The definition here (https://github.com/maxsnew/multi-poly-cats/blob/main/UMP.agda#L54) defines what it means that a cone gets mapped to a cone at all.

GenericMonkey commented 1 year ago

Think I have coproducts + coproduct cocone defined appropriately as dual constructions here. Would you mind taking a look and seeing if this is the direction you were envisioning?

Also, would be nice to chat about step 2 -- not really sure where to begin to state and prove a proposition as a type...

maxsnew commented 1 year ago

Those all look good. Step 2 above I think is a definition. Then you want to show if a category is CCC then any coproduct is distributive. As discussed in class, this follows from the more general RAPL theorem, so it might be worth proving that first. IIRC RAPL is proved in the Cubical stdlib already but their definition of limits is not in terms of representability so another strategy would be to define limits in terms of representability and prove it equivalent to the definition in the stdlib.

GenericMonkey commented 1 year ago

Going through the workflow we chatted about to define the (a \times -) functor, but think I forgot a few of the steps: I have the following written down:

I'm blanking on what you had meant by step 2. I know we defined the diagonal to eventually be the adjoint of the prod functor, but not sure exactly what you mean by step 2, or how defining the diagonal lets you more easily define - \times -

maxsnew commented 1 year ago

Step 2 is implementing https://github.com/maxsnew/multi-poly-cats/issues/7 and then using that to construct the product functor