Duplication of code in the library

[jpoiret]

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]

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]

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]

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

• SetSigmaIso
• IsoSetTruncateSndΣ

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

[anshwad10]

leftright in Cubical.Foundations.GroupoidLaws has the same type as compPath≡compPath' in Cubical.Foundations.Prelude, and they are provably (but not definitionally) equal.

[anshwad10]

preserveIsosF in Cubical.Categories.Functor.Properties and F-Iso in Cubical.Categories.Isomorphism. I think we should deprecate preserveIsosF