chore: make Discrete into a record so it displays better

[plt-amy]

Now if you're in a context like

module _ {ℓ} {A : Type ℓ} ⦃ d : Discrete A ⦄ (x y : A) where

the normal form of x ≡? y will print as x ≡? y instead of just d.

[Lavenza]

Pull request preview

Changed pages

• Algebra.Group.Cat.FinitelyComplete (± 23)
• Algebra.Group.Subgroup (± 21)
• Algebra.Ring.Module.Category (± 17)
• Algebra.Group.Ab.Tensor (± 15)
• Algebra.Monoid.Category (+14, -15)
• Algebra.Group.Ab.Hom (± 12)
• Algebra.Group.Free.Product (± 11)
• Algebra.Ring.Module.Action (± 10)
• Algebra.Group.Action (± 9)
• Algebra.Group.Semidirect (± 9)
• Algebra.Group.Ab.Sum (± 7)
• 1Lab.Classical (± 6)
• Algebra.Group.Ab.Abelianisation (± 6)
• Algebra.Group.Cat.Monadic (± 6)
• Algebra.Group.Instances.Cyclic (± 6)
• Algebra.Group.Ab (+4, -7)
• Algebra.Group.Concrete (± 5)
• Algebra.Ring.Cat.Initial (± 5)
• Algebra.Ring.Module (± 5)
• Algebra.Ring.Module.Vec (± 5)