added Pointed algebraic structure, (raw) bundle and homomorphism

[jamesmckinna]

See issue #1957

TODOs:

• add a RawPointed instance to Data.Maybe.Base
• FreePointed functor, as in The free Magma on a Set, resp. Setoid [bis] #1962
• Data.Nat.Base? List? what else?
• forgetful functor from Pointed back to Setoid
• what else?

[jamesmckinna]

Hmmm... the library disagrees with @JacquesCarette 's analysis that Pointed belongs under Algebra:

module Relation.Nullary.Construct.Add.Point where

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

Maybe this PR isn't required after all? Or at least, in a way which is suitably/sensibly (backwards) compatible.

UPDATED: and with apologies for insufficient testing before issuing the PR :-(

[JacquesCarette]

See my comments on #1957 .

There's a difference between the theory and the free algebra associated to it. I meant the theory, which belongs in Algebra. The data structure belong in Data. That the construction lives under Relation is fine, but Relation.Nullary is an aberration. What's the use of a relation on nothing?

[jamesmckinna]

As with #1963 I'm going to close this for now, pending (the design of) a resolution of #1957, at which point this PR might be the (best?) place to implement such a solution.