||| Algebra.Magma: A representation of magmas.
|||
||| A magma is more-or-less the simplest non-trivial example of a algebraic
||| structure. It is simply a set together with a lawless binary operation over
||| it. More formally, it is *any* pair
||| \\(\mathscr{M} = (M:\mathscr{V}, \* : M^2 \to M)\\). It doesn't matter what
||| the function \\(\*\\) is. It can have any properties whatsoever; the only
||| reuirement is that it be a function of the specified type. That is, it must
||| be a total co-injective relation with domain \\(M^2\\) and codomain \\(M\\),
||| where by \"co-injective\" I mean that for every input, there is no more than
||| one output. Together with totality, which states that every input has at
||| least one output, this means that a function is a relation where every input
||| has exactly one output.
|||
||| Magmas aren't especially interesting in and of themselves. Because there are
||| no magma axioms, just a type, there isn't much that can be said about magmas
||| in general. However, they give a useful way to talk about other algebraic
||| structures. A group, for example, is a magma satisfying certain laws. In
||| other words, talking in terms of magmas and related lawless algebraic
||| structures just gives us a more convenient way to talk about the signature
||| of the more interesting ones. (Of course, all of this leads naturally to
||| groups, semigroups, monoids, etc. being extensions of the `Magma`
||| record.)
|||
||| That's not to say there's nothing interesting about magmas. There are
||| interesting combinatorial questions arising from freely generated magmas.
||| That is, consider a magma generated by three elements, \\(a, b, c\\). By
||| \"freely generated\", we mean that there are no equalities except those
||| directly entailed by the axioms; since there aren't any axioms, there aren't
||| any (non-reflexive) equalities! E.g., in a freely generated magma, we know
||| that \\((x\*y)\*z \neq x\*(y\*z)\\) for every \\(x, y, z\\). If they were
||| equal, it would still be a magma, but not a freely generated one. Now, for
||| the free magma with 3 generating elements, how many elements are there with
||| exactly \\(k\\) applications of the operation \\(\*\\)? Or more generally,
||| what if there are \\(n\\) generating elements? If you like combinatorics,
||| you might enjoy working these and related questions out\-\-\-and, as usual,
||| there's a connection to the Catalan numbers.
module Algebra.Magma

%default total

infix 7 |*|

||| The record representing magmas. Note that there are no proofs to be
||| automatically filled in; magmas don't have any extra properties beyond their
||| signature.
public export
record Magma where
  constructor MkMagma
  Set' : Type
  op'  : Set' -> Set' -> Set'

public export
Set : {magma : Magma} -> Type
Set {magma} = Set' magma

public export
(|*|) : {magma : Magma} -> Set {magma} -> Set {magma} -> Set {magma}
(|*|) {magma} = op' magma


{-
public export
AddMagma : (Num ty) => Magma
AddMagma {ty} = MkMagma ty (+)

public export
MultMagma : (Num ty) => Magma
MultMagma {ty} = MkMagma ty (*)

-- -}


-- data Magma : (Set : Type) -> (Set -> Set -> Set) -> Type where
--   Magmoid :
-- {-
