Felix Cherubini

> * I haven't been working with the algebra libraries much. Is adding `GroupHom`, `RingHom` etc outrageous? No - that is actually how types of Homs are named right now....

I don't know a better presentation of the open modality.

I agree that it would be good to change all instances of that in a PR.

> I would very much welcome suggestions on how to better hide the increased generality for users only interested in ordinary adjunctions. How about splitting it up into two files,...

I think alienation is not a problem, if you just provide an example everyone knows. Without too much thought, I can imagine the following to be a good way set...

@anuyts: Is this intentionally left in draft state?

I like the approach of ``groupes algébriques'' a lot. As far as I remember, they still use constructive reasoning in their site of rings. But as Max pointed out, some...

I should add, that the synthetic approach might be something completely different than what you are looking for.

> Thank you for pointing out this synthetic approach. I am not sure that it is directly related but i would be interested to see how it is implemented. There...

> Incidentally, i just realized that the relation with the lattice approach is the following: one would like to prove from what is already in the cubical library that R->Spec(A)(R)=Hom(A,R)...