Matthias Ritter (formerly Hutzler)

This PR just generalizes the type signatures of operations like `AlgebraHom≡` or `_∘≃a_` to algebras of different levels.

Examples for modalities

1

This PR provides a few simple examples of modalities (as defined in `Cubical.Modalities.Modality`). Note that there is already `HLevelTruncModality` in `Cubical.HITs.Truncation.Properties`.

Flipped type signatures in comments

6

When reexporting things, there are sometimes type signatures stated in comments. I think I found a few places where these type signatures are inaccurate, for example: https://github.com/agda/agda-stdlib/blob/ebfb8814b4330b314da8fb9cae527e6a6fab01aa/src/Data/Nat/Properties.agda#L1196 This function actually...

Use commAlgebraFromCommRing in the equivalence between algebras and over-rings

1

This small PR uses the `commAlgebraFromCommRing` construction more consequently, in code that was written before it. We also single out a property of the construction (`commAlgebraFromCommRing→CommRing`) from the surrounding proof.

More elegant construction of ZariskiLattice

2

Here is an idea for an improvement in [ZariskiLattice.Base](https://github.com/agda/cubical/blob/master/Cubical/AlgebraicGeometry/ZariskiLattice/Base.agda) . The current set-quotient construction begins by defining a preorder (without using this name) and deriving the equivalence relation `_∼_` from...

Simplify `Embedding-into-hLevel→hLevel`

5

This small PR simplifies the proofs of `Embedding-into-hLevel→hLevel` and the two special cases for `isProp` and `isSet`. `Embedding-into-hLevel→hLevel` was unnecessarily defined by case distinction. The reason is probably the definition...

trying to make FreeCommAlgebra opaque...

Point out `--overlapping-instances` in error messages.

6

When instance resolution fails because of overlapping instances, the error message lists the candidates, but it is not very clear about the fact that it stops searching *because* there is...