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

Right adjoints in product category #48

Closed stschaef closed 9 months ago

maxsnew commented 9 months ago

Does anyone remember what this was for? Specifically, the UnivEltProd file, the other is self explanatory

stschaef commented 9 months ago

IIRC it was Eric's first pass at getting a universal element for the product presheaf. And then I came in later and tried to generalize that construction as much as possible with the other file

I don't fully remember, but I think there was definitional differences between what he gave and what I made. Can't remember if they were reconcilable or not, can try to take a look at some point this week if you think its worth integrating both files

stschaef commented 9 months ago

@ericgiovannini did you ever need this?

ericgiovannini commented 9 months ago

@ericgiovannini did you ever need this?

I haven't utilized it yet, but I expect that it will be useful for formulating limits in double categories

maxsnew commented 9 months ago

What happened here?