Remove the makeX functions but keep the makeIsX

[mortberg]

We could remove for example makeGroup as groups should be constructed using copatterns anyway. It might still be nice to keep the makeIsGroup and it should hopefully not be a problem as the copatterns in the group def will block the laws from getting unfolded unless necessary

[barrettj12]

I disagree, since I think makeX gives much more readable definitions. E.g. looking at the current definition of the group ℤ in Cubical.Algebra.Group.Instances.Int:

ℤ : Group₀
fst ℤ = ℤType
1g (snd ℤ) = 0
_·_ (snd ℤ) = _+ℤ_
inv (snd ℤ) = _-ℤ_ 0
isGroup (snd ℤ) = isGroupℤ
  where
  abstract
    isGroupℤ : IsGroup (pos 0) _+ℤ_ (_-ℤ_ (pos 0))
    isGroupℤ = makeIsGroup isSetℤ +Assoc (λ _ → refl) (+Comm 0)
                           (λ x → +Comm x (pos 0 -ℤ x) ∙ minusPlus x 0)
                           (λ x → minusPlus x 0)

vs using makeGroup:

ℤ = makeGroup
  0
  _+ℤ_
  (_-ℤ_ 0)
  isSetℤ
  +Assoc
  (λ _ → refl)
  (+Comm 0)
  (λ x → +Comm x (pos 0 -ℤ x) ∙ minusPlus x 0)
  (λ x → minusPlus x 0)

You could even annotate it:

ℤ = makeGroup
  0          -- identity
  _+ℤ_       -- group operation
  (_-ℤ_ 0)   -- inverses
  ...

[barrettj12]

On the other hand, I just tried doing this with the GroupStr constructor groupstr:

ℤ : Group₀
ℤ = ℤType , groupstr
      0
      _+ℤ_
      (_-ℤ_ 0)
      (makeIsGroup 
        isSetℤ
        +Assoc
        (λ _ → refl)
        (+Comm 0)
        (λ x → +Comm x (pos 0 -ℤ x) ∙ minusPlus x 0)
        (λ x → minusPlus x 0)
      )

which looks very similar. Probably not all of these are necessary to keep.

I think some of the makeX functions (e.g. makeGroup-left, makeGroup-right and makeAbGroup) are worth keeping because they allow you to provide only a minimal amount of structure when the rest can be inferred.

[mortberg]

It's mainly a matter of efficiency. Copatterns have the benefit that Agda won't unfold the definitions unless one applies a projection. This seems completely essential to ensure reasonable typechecking times for complex constructions (e.g. Z cohomology groups). By now I also find the copattern definitions more readable as well. If you have

ℤ : Group₀
fst ℤ = ℤType
1g (snd ℤ) = 0
_·_ (snd ℤ) = _+ℤ_
inv (snd ℤ) = _-ℤ_ 0
...

you don't need any comments about what is the 1, operation and inverse are

So I think all algebra structure operations should be given by copatterns, but the proofs that these operations form an instance of the structure can be given using the makeX (and then also maybe made opaque using abstract)

[barrettj12]

If X / isX is a record type, then can't we just use a constructor instead of makeX / makeIsX?