search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

Categorical bits and pieces #1008

Closed jpoiret closed 1 year ago

jpoiret commented 1 year ago

Hi,

While attempting a categorical formulation of #1007 that I abandoned in the end, I collected a lot of simple results and modifications.

Noteworthy changes are 2491f5fd4a58ce99f6fdf93c4fd45e08e7b95950, a change to the definition of being an equivalence, which previously was not an hProp. I fixed all uses of it in the library to be compatible with the new definition. I also separated triangle identities from the definition of an adjunction in c55988cfb8a9c66526068fb134bf2547c5c93ef2, so that I could more easily add adjoint equivalences in c9cb16baa0ba94a140b4706a4d418bbe4fe31a21.

From what I can tell this is independent to #988, and shouldn't interfere with it.

LMKWYT

jpoiret commented 1 year ago

I just removed the stuff about subpresheaves and representable presheaves, as there's going to be something better with #988 anyways (I have to make time to send some changes to it).

felixwellen commented 1 year ago

Can you rebase?

jpoiret commented 1 year ago

Just pushed with the comment removed + a stylistic change in AdjointEquivalence. wrt. isEquivalence, I don't know of a good representation of it. If C is univalent, then being an adjoint equivalence might be it, but that's not a general characterization.

felixwellen commented 1 year ago

Thanks! Maybe you can put what you know into a comment at isEquivalence, I guess it is natural to wonder about that when reading the definition.

felixwellen commented 1 year ago

With "what you know" I mean that we don't know a notion which works analogous to "isEquiv" for not necessarily univalent categories.

felixwellen commented 1 year ago

Thanks! I'll merge.