Data.ComMonoid

Definitions

record ComMonoid : Type -> Type

  Commutative monoid
  Not encoding the property of commutativity here

Totality: total
Visibility: public export
Constructor: 

MkComMonoid : (a -> a -> a) -> a -> ComMonoid a

Projections:

.neutral : ComMonoid a -> a

.plus : ComMonoid a -> a -> a -> a

Hints:

ComMonoid Double

ComMonoid ()

Num a => ComMonoid a

ComMonoid a => ComMonoid b => ComMonoid (a, b)

.plus : ComMonoid a -> a -> a -> a

Visibility: public export

plus : ComMonoid a -> a -> a -> a

Visibility: public export

.neutral : ComMonoid a -> a

Visibility: public export

neutral : ComMonoid a -> a

Visibility: public export

doubleIsMonoid : ComMonoid Double

Visibility: public export

unitIsMonoid : ComMonoid ()

Visibility: public export

numIsMonoid : Num a => ComMonoid a

Visibility: public export

listIsMonoid : ComMonoid (List a)

Visibility: public export

pairIsMonoid : ComMonoid a => ComMonoid b => ComMonoid (a, b)

Visibility: public export

sum : ComMonoid a => List a -> a

Visibility: public export

ComMonoid : Type

  Same as ComMonoid, but without exposing the underlying carrier in the type

Visibility: public export

record ComMonoidHomo : ComMonoid -> ComMonoid -> Type

Totality: total
Visibility: public export
Constructor: 

MkComMonoidHomo : (underlyingMap : (c .fst -> d .fst)) -> ((x : c .fst) -> (y : c .fst) -> underlyingMap ((c .snd) .plus x y) = (d .snd) .plus (underlyingMap x) (underlyingMap y)) -> underlyingMap ((c .snd) .neutral) = (d .snd) .neutral -> ComMonoidHomo c d

Projections:

.neutralPreserve : ({rec:0} : ComMonoidHomo c d) -> underlyingMap {rec:0} ((c .snd) .neutral) = (d .snd) .neutral

.plusPreserve : ({rec:0} : ComMonoidHomo c d) -> (x : c .fst) -> (y : c .fst) -> underlyingMap {rec:0} ((c .snd) .plus x y) = (d .snd) .plus (underlyingMap {rec:0} x) (underlyingMap {rec:0} y)

.underlyingMap : ComMonoidHomo c d -> c .fst -> d .fst

.underlyingMap : ComMonoidHomo c d -> c .fst -> d .fst

Visibility: public export

underlyingMap : ComMonoidHomo c d -> c .fst -> d .fst

Visibility: public export

.plusPreserve : ({rec:0} : ComMonoidHomo c d) -> (x : c .fst) -> (y : c .fst) -> underlyingMap {rec:0} ((c .snd) .plus x y) = (d .snd) .plus (underlyingMap {rec:0} x) (underlyingMap {rec:0} y)

Visibility: public export

plusPreserve : ({rec:0} : ComMonoidHomo c d) -> (x : c .fst) -> (y : c .fst) -> underlyingMap {rec:0} ((c .snd) .plus x y) = (d .snd) .plus (underlyingMap {rec:0} x) (underlyingMap {rec:0} y)

Visibility: public export

.neutralPreserve : ({rec:0} : ComMonoidHomo c d) -> underlyingMap {rec:0} ((c .snd) .neutral) = (d .snd) .neutral

Visibility: public export

neutralPreserve : ({rec:0} : ComMonoidHomo c d) -> underlyingMap {rec:0} ((c .snd) .neutral) = (d .snd) .neutral

Visibility: public export