Categorical bits and pieces

[jpoiret]

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 2491f5f, 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 c55988c, so that I could more easily add adjoint equivalences in c9cb16b.

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

LMKWYT

[jpoiret]

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]

Can you rebase?

[felixwellen]

Thanks for the contribution!
I commented only on one small detail and will merge anyway if you don't have the time to fix it.
One question though: Are there any candidates we should consider as a definition of isEquivalence, which are naturally a proposition?

[jpoiret]

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]

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]

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

[felixwellen]

Thanks!
I'll merge.