Pointed: Setoid with a distinguished point

[jamesmckinna]

This concept doesn't exist in the library (for Set, Data.Maybe does the trick of course), so we should add it.

But where should it belong? A Setoid-with-a-point: is it an Algebra (with a very boring signature, consisting of a single nullary operation), or a special kind of Setoid, and hence should live with those things under Relation.Binary?

(this may be a separate library design pain point regarding Setoid: is that an Algebra too, albeit one with no operations?)

UPDATED: grrr. Pointed introduced in two ways already. Once to add a distinguished point; this apparently lives under Relation.Nullary.Construct.Add.Point where

open import Data.Maybe.Base public
  using () renaming (Maybe to Pointed; nothing to ∙; just to [_])

and once to add a distinguished point which is moreover an identity for a binary operation. And overloading the shared common use of Maybe as the representing Free functor. This seems a bit wart-y how to proceed?

Either way, we might then want a Free such thing, (cf. #1962 / #1954 ) and know that its algebra is that of the usual adjoint/monadic situation arising from Maybe and the forgetful operation of throwing away the distinguished point.

[JacquesCarette]

I picture Pointed as a theory, so a record. What Relation.Nullary.Construct.Add.Point does is build the free Pointed on a Set, as @jamesmckinna says.

Maybe isn't a theory, it's a data-structure -- which is a standard implementation of the Free Pointed Set.

[jamesmckinna]

Disentangling the existing design to separate out the various use cases seems like:
"Another one to punt until after v2.0, I think ;-)"

UPDATED: now we are at such a point, what is the best way to proceed? Suggestions @JacquesCarette ?

[JacquesCarette]

I still see it as something that belongs in Algebra. It could be called Pointed but also PointedCarrier, PointedSet, PointedSetoid, I'm ok with all of those.

[jamesmckinna]

I'm going to close this for now:

• difficulty figuring out how to refactor the existing (overlapping) uses of Maybe into a more coherent design
• failure to achieve consensus on how to tackle Free constructions generally The free Magma on a Set, resp. Setoid [bis] #1962 and much other discussion on- and off-line about this.

I'll re-open as and when we make progress on the second? Hopefully the first will follow (more) straightforwardly after that?