search

maxsnew / cubical-categorical-logic

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

Some Equivalences of Categories #8

Closed maxsnew closed 6 months ago

maxsnew commented 1 year ago

Show

  1. λF and λFl in Cubical.Categories.Functors.More are equivalences of categories
  2. Proving this for λFl will be easiest by proving that Swap : C x D -> D x C is an equivalence of categories
stschaef commented 1 year ago

I'm gonna dig into this more on Thursday. I'm a little confused what "equivalence of categories" means here and want to double check what we want to show here. This isn't λF and λFl forming the pair of the equivalence, right? Because they map into the same target

Is the goal here to show that λF is one half of an equivalence between the category of functors from (\Gamma \times C) \to D and the category of functors \Gamma \to (Category of functors C to D). Sorry for this poor formatting. All I mean to ask, is if λF is behaving like one half of the currying isomorphism on functors and if we are searching to prove this equivalence by finding the inverse to this map. Likewise for λFl we make the same argument as for λF but compose it with the swapping maps.

Just as above, Swap as written is one half of this equivalence? The other half is the obvious functor D \times C \to C \times D?

maxsnew commented 1 year ago

Is the goal here to show that λF is one half of an equivalence between the category of functors from (\Gamma \times C) \to D and the category of functors \Gamma \to (Category of functors C to D).

Yes.

stschaef commented 1 year ago

Apologies for dragging my feet a little on this. Took a while to understand the usage of the equational reasoning syntax.

On my fork I have an extension of λFr to a functor between the appropriate functor categories. I can show this is at least faithful and have a rough idea on what to say for ESO and fullness, but I'm not really sure on how to use the existential/propositional truncation syntax. I cannot even get it to load with holes in it

Edit: nvm on this syntax issue. Was trying to build sigma terms with \Sigma and not a comma

stschaef commented 1 year ago

The bulk of this is done. I have fully faithful and ESO, but unsure how to tie everything together. It seems like its just instantiating the proper things. Then univalence + weak equivalence will establish what we want, but I'm not entirely sure what's going on with univalence yet

I'd appreciate if you have any quick thoughts on this, or on a good renaming of all the terms. If not, I can probably clean this up and submit a PR tomorrow

maxsnew commented 1 year ago

LGTM. Some names are bad, but as long as they're not part of the public interface it's not that important.

For univalence, you will need to add an additional assumption that the category D is univalent.

There's a nice analogy to keep in mind which is that Univalent Category : Poset :: Category : Preorder. (For this reason most other univalent libs call what cubical calls Univalent Categories just Categories and what cubical calls Categories Precategories. So the above is a generalization of the fact that if P is a poset and Q is a preorder then the ordered set of monotone functions P^Q is a poset.

maxsnew commented 1 year ago

I think it would be better to prove this is an isomorphism of categories, rather than an equivalence since that is strictly stronger and more useful for non-univalent categories.