Duality of cocartesian causes qualified solves

[Reijix]

Something that has always been bugging me is that when working with cocartesian automatically solving goals becomes tedious because the coproduct operators sometimes get inserted qualified, i.e. coproduct.[_,_], coproduct.i₁, Dual.op-binaryProducts.⁂.

To reproduce go to Categories.Category.Distributive.Properties and in the proof of distributeˡ⁻¹-π₁ replace [ π₁ ∘ ((id ⁂ i₁)) , π₁ ∘ (id ⁂ i₂) ] with a hole before solving it (C-c C-s).

I'm not sure if that only happens if cartesian is also in scope. Is that a known issue? Am I just importing things wrongly?
I could not find related issues when searching.

[Reijix]

Also generally, Categories.Category.Distributive.Properties highlights asymmetries between Cartesian and Cocartesian:

• For Cartesian we always need to open BinaryProducts as well, while Cocartesian publicly opens them
• In Cocartesian we have +₁, while in Cartesian it is called ⁂ (is there any reason not to call it ×₁?)

There are probably more, these are just at the top of my head. Has there been a discussion before to adjust these definitions to be more symmetric?

[JacquesCarette]

I've seen similar reports independently of agda-categories. It seems to be an odd thing of Agda's. Some recent PRs against Agda itself (which I think will make it to 2.9) help a lot.

The most important question:

Has there been a discussion before to adjust these definitions to be more symmetric?

Some - and some small PRs have made progress in that direction. I would definitely welcome more!

[TOTBWF]

The culprit is these lines:

agda-categories/src/Categories/Category/Cocartesian.agda

Lines 49 to 57 in 9d50d25

	module coproduct {A} {B} = Coproduct (coproduct {A} {B})
	_+_ : Obj → Obj → Obj
	A + B = coproduct.A+B {A} {B}
	open coproduct
	using (i₁; i₂; [_,_]; inject₁; inject₂; []-cong₂; ∘-distribˡ-[])
	renaming (unique to +-unique; η to +-η; g-η to +-g-η)
	public

If you do an open of a module without a telescope, then Agda will forget all of the display forms. The solution is to instead do something along the lines of

module coproduct {A} {B} = Coproduct (coproduct {A} {B}) 

module _ (A B : Obj) where
  open Coproduct (coproduct {A} {B})
    renaming (A+B to infixr 6 _+_)
    using ()
    public
  
module _ {A B : Obj} where
  open Coproduct (coproduct {A} {B})
    using (i₁; i₂; [_,_]; inject₁; inject₂; []-cong₂; ∘-distribˡ-[]) 
    renaming (unique to +-unique; η to +-η; g-η to +-g-η) 
    public 

We do this in the 1lab here and here.