
  0 | module Data.Magma
  1 | 
  2 | import Data.Maybe
  3 | 
  4 | %default total
  5 | 
  6 | export infixr 6 .*.
  7 | 
  8 | public export
  9 | record RawMagma where
 10 |   constructor MkRawMagma
 11 |   Carrier : Type
 12 |   Product : Carrier -> Carrier -> Carrier
 13 | 
 14 | namespace List
 15 |   public export
 16 |   rawMagma : (a : Type) -> RawMagma
 17 |   rawMagma a = MkRawMagma (List a) (++)
 18 | 
 19 | namespace String
 20 |   public export
 21 |   rawMagma : RawMagma
 22 |   rawMagma = MkRawMagma String (++)
 23 | 
 24 | namespace Unit
 25 |   public export
 26 |   rawMagma : RawMagma
 27 |   rawMagma = MkRawMagma Unit $ const $ const ()
 28 | 
 29 | namespace Maybe
 30 |   public export
 31 |   rawMagma : RawMagma -> RawMagma
 32 |   rawMagma magma = MkRawMagma (Maybe magma.Carrier)
 33 |     (\case
 34 |        Nothing => id
 35 |        Just x => \case
 36 |          Nothing => Just x
 37 |          Just y => Just (magma.Product x y))
 38 | 
 39 | public export
 40 | openMagma : (magma : RawMagma) -> Semigroup magma.Carrier
 41 | openMagma magma = MkSemigroup magma.Product
 42 |