Duplication of code in the library

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

447 stars 136 forks source link

Duplication of code in the library #1017

Open jpoiret opened 1 year ago

jpoiret commented 1 year ago

I've been noticing quite a lot of code that's duplicated in the library recently, so I think we could create a main issue for all such cases that we can expand over time. I haven't been taking notes up to now, so I'll add stuff as I stumble upon it. If you see any duplicated code, please mention it here and I'll add it to the list.

[ ] cong-∙ and congFunct with their related functions in Cubical.Foundations.GroupoidLaws.

phijor commented 10 months ago

uaη is proved twice:

via J in Cubical.Foundations.Univalence.uaη
via Glue in Cubical.Foundations.Transport.uaTransportη

The latter is a much more direct proof.

mortberg commented 10 months ago

Feel free to make PRs either removing one of the proofs or documenting why we have two versions (maybe also moving results to the same place).

Something that annoyed me recently is that we have both Data.Fin and Data.FinData. Some things are done with one version of Fin and some with the other. It would be better to get decide which version to use and get rid of the other. I think I prefer Data.Fin instead of Data.FinData

phijor commented 6 months ago

Another day, another duplication. Cubical.HITs.Settruncation.Properties contains two proofs of Iso ∥ Σ A B ∥₂ ∥ Σ A (λ x → ∥ B x ∥₂) ∥₂:

Up to η-expansion of Iso , these are definitionally the same.