Clean up code in BinProduct.

[anuyts]

[maxsnew]

1. I don't think ×C-sym is a good naming convention, I prefer Sym. You can always use qualified imports to make it explicit which Sym you are going for. IMO this ultimately reduces proliferation of long qualifiers.
2. The Yoneda embedding is already defined as YO in Cubical.Categories.Yoneda

[anuyts]

• Thanks for pointing me to YO, I had missed that somehow.

• The lemma Sym has not followed a pre-existent naming convention already adopted by ×C-assoc. Whatever is decided, both should follow the same naming scheme.

• One would probably want to use _×C_ unqualified, so one would need an unqualified import as well. Then either the file should be imported as

  open import Cubical.Categories.Constructions.BinProduct using ({-bunch of stuff that's clearly product-related-})
  import Cubical.Categories.Constructions.BinProduct as ×C
  

  or we need to put everything that can get a shorter name by not mentioning it is product-related in a named submodule.

  The file https://github.com/agda/cubical/blob/master/NAMING.md doesn't commit to any approach.

• Given that categories are big records with eta-equality, often bearing complicated equality proofs, they often perform very badly as implicit arguments and produce poor interactive-mode guidance. So I would still suggest to make these arguments to Sym/×C-sym explicit as is the case in ×C-assoc.

[anshwad10]

One would probably want to use ×C unqualified, so one would need an unqualified import as well. Then either the file should be imported as

open import Cubical.Categories.Constructions.BinProduct using ({-bunch of stuff that's clearly product-related-})
import Cubical.Categories.Constructions.BinProduct as ×C

or we need to put everything that can get a shorter name by not mentioning it is product-related in a named submodule.

A better way to do this is to write it in a single line like so:

open import Cubical.Categories.Constructions.BinProduct as ×C using ({-bunch of stuff that's clearly product-related-})