abstractify QuotientAlgebra

[MatthiasHu]

This PR declares almost all definitions in Cubical.Algebra.CommAlgebra.QuotientAlgebra as abstract in an attempt to reduce long type checking times.

FPAlgebra (the only module that uses QuotientAlgebra so far) had to be slightly adjusted too. A witness inducedHom∘quotientHom had to be added to QuotientAlgebra for an equality that was a definitional equality before.

This replaces #856.

[MatthiasHu]

Just a note: I can't see how to "abstractify" FreeCommAlgebra in the same way, because it consists of FreeCommAlgebra.Base and FreeCommAlgebra.Properties, and I think there is no way to let the latter module look through abstract definitions in the first module. :-/

[mortberg]

Is it clear that making everything abstract like this is the right way to go? My experience is that constructions should not be opaque, but their properties can often be... Also, the "locking" trick that we use in some files for Z-cohomology could be helpful. It's an alternative to making things abstract

[MatthiasHu]

I think to avoid the unfolding of algebra terms, it has to be the construction (_/_) that is abstract. I think it would not help to make only properties abstract?
I will look at the locking trick...

[mortberg]

I think to avoid the unfolding of algebra terms, it has to be the construction (_/_) that is abstract. I think it would not help to make only properties abstract? I will look at the locking trick...

Yeah, maybe a locked version of _/_ is what you need. I'm not sure if there's some better place to look than https://agda.github.io/cubical/Cubical.Experiments.ZCohomologyOld.Properties.html#24355, but it's the first I found

[MatthiasHu]

I experimented a bit with the locking trick. In principle it seems very very nice to provide an interface where the user of the module can decide themselves whether they want to see reducing or non-reducing behavior (by plugging in either unlock or some general key : lockUnit). But it seems to be a considerable amount of overhead compared to basically just adding a few abstracts as in the present PR.

For example, the definition of quotientHom currently reads:

  quotientHom : CommAlgebraHom A (_/_)
  fst quotientHom x = [ x ]
  IsAlgebraHom.pres0 (snd quotientHom) = refl
  ...

With the locking method it would be either something like this (taken from here):

  quotientHomWithKey : (key : lockUnit) → CommAlgebraHom A (_/WithKey_ key)
  fst (quotientHomWithKey unlock) x = [ x ]
  IsAlgebraHom.pres0 (snd (quotientHomWithKey unlock)) = refl
  ...

  quotientHom : CommAlgebraHom A _/_
  quotientHom = quotientHomWithKey key

Or something like this (taken from here):

  quotientHomUnlocked : CommAlgebraHom A (_/Unlocked_)
  fst quotientHomUnlocked x = [ x ]
  IsAlgebraHom.pres0 (snd quotientHomUnlocked) = refl
  ...

  quotientHom : CommAlgebraHom A (_/_)
  quotientHom = lock' key
    (λ k → CommAlgebraHom A (lock k _/Unlocked_))
    quotientHomUnlocked

In particular, I don't see how to avoid writing out all the type signatures two (or even three) times, in slightly modified ways. This feels bad to me as they can become relatively long, e.g.:

  injectivePrecomp : (B : CommAlgebra R ℓ) (f g : CommAlgebraHom (A / I) B)
                     → f ∘a (quotientHom A I) ≡ g ∘a (quotientHom A I)
                     → f ≡ g

[felixwellen]

I'm certainly ok with using 'abstract' for now. Should I review this PR?

[MatthiasHu]

Should I review this PR?

Was this question directed at me? :-)

[felixwellen]

Yes. With a possibility for anders to intervene.

[MatthiasHu]

Oh, ok. Yes, I would be pleased if you could review this PR.

[felixwellen]

I can confirm a very nice type checking speed reduction in FPAlgebra! On my notebook, it used to take 80s and now it is down to 20s - which is mostly spend on deserialization, so I guess there is no immediate need to look for further speed improbements to FPAlgebra.

[felixwellen]

Only a couple of minor comments/requests for clarifications. Otherwise this is good to merge.
I think we can work with abstract interfaces like this one and see how it goes.

[MatthiasHu]

This is ready to be merged from my perspective.

[felixwellen]

Also from mine - looks great!