Thomas Lamiaux

@mortberg Finally done with that !

We were just talking about it. We have decided convention for Algebra and for some stuff in the general library but not for Category. The entire folder should also be...

should be fixed when #813 is

For Algebra, this du to a recent effort that is not finished to clean it. For instance the naming is a few months ald and was just enforced last week....

No I meant having an issue about refactoring Category and one about defining naming conventions or category. It don't really see how it is possible to define a general standard...

@aljungstrom won't compute after 10 minutes on my ok computer https://github.com/agda/cubical/pull/882/files#diff-b89e4f1599c7dba39bcde49cd6c8c0df1239f68261f2abf543ca8b274b049a45R461

@aljungstrom @mortberg This example is done up to the proof that `(a b : ℤ) → (ϕ₁ a) ⌣ (ϕ₁ b) ≡ 0ₕ 2` Proof that seems too slow to...

I have added : - it suffices to prove `(phi 1) cup (phi 1) = 0` to prove it for any `a b` - I have added that if the...

@mortberg With Axel lemme, it is now done

done