Cats is CartesianClosed (when all levels the same) about agda-categories HOT 6 CLOSED

So I think I know what the source of difficulty is: the definition of 'exponential object' used assumes that some products (as necessary) exist; but we already know all products exist. The problem is that the definition doesn't use the product just given. But of course the it is CCC is with respect to that one product. [This definition is inherited from the original port]. I think that if the definition was adjusted so that the exponential object was coherent, by construction, with the given product, lots of things would be considerably simpler. And it would match the definitions in the literature too.

from agda-categories.

actually the current behavior is correct.

consider a trivial example. usually we say a product of A and B is A × B. However, it doesn't have to be the canonical representation of the product. for example, B × A is also an legitimate representation. in fact, there isn't a preference between both; they are just equally good, and there are other equally good representations. the uniqueness part of products concludes all such best representations are isomorphic and that's good enough. that the exponential part does not make assumption of concrete representation of a product is consistent with this extensional view.

from agda-categories.

The current behaviour is definitely not wrong. I agree with your reasoning.

I wonder if anyone has ever proved it in full generality though? I really have no idea of how to proceed in those 2 holes. I suspect that existing proofs are either just sketches or 'for convenience' pick one product, since they are all "the same" anyways.

from agda-categories.

I did it in 1c7e2f4

it is not too difficult. the problem is that there are slow computation parts. the idea is to make use of the UMP of the products in the construction. assuming a canonical construction is morally correct, because if we only inspect objects and morphisms extensionally consistently, there shouldn't be a problem. this is seen in many other constructions where properties like associativity etc are ignored.

from agda-categories.

Thanks. A couple of hours after I posted my comment, your remarks finally sunk in properly, and it finally occurred to me to use the UMP of products. Still, there was quite a bit of work to do to make it all come together! Very nice.

from agda-categories.

I developed @HuStmpHrrr's insight a bit further in #90.

from agda-categories.