Idris2Doc : Control.Algebra

# Control.Algebra

## Definitions

`interface SemigroupV : Type -> Type`
Parameters: ty
Constraints: Semigroup ty
Methods:
`semigroupOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> l <+> (c <+> r) = (l <+> c) <+> r`

Implementations:
`SemigroupV ty => SemigroupV (Identity ty)`
`SemigroupV ty => SemigroupV (Identity ty)`
`semigroupOpIsAssociative : {auto __con : SemigroupV ty} -> (l : ty) -> (c : ty) -> (r : ty) -> l <+> (c <+> r) = (l <+> c) <+> r`
Visibility: public export
`interface MonoidV : Type -> Type`
Parameters: ty
Constraints: Monoid ty, SemigroupV ty
Methods:
`monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral = l`
`monoidNeutralIsNeutralR : (r : ty) -> neutral <+> r = r`

Implementations:
`MonoidV ty => MonoidV (Identity ty)`
`MonoidV ty => MonoidV (Identity ty)`
`monoidNeutralIsNeutralL : {auto __con : MonoidV ty} -> (l : ty) -> l <+> neutral = l`
Visibility: public export
`monoidNeutralIsNeutralR : {auto __con : MonoidV ty} -> (r : ty) -> neutral <+> r = r`
Visibility: public export
`interface Group : Type -> Type`
`  Sets equipped with a single binary operation that is associative,  along with a neutral element for that binary operation and  inverses for all elements. Satisfies the following laws:    + Associativity of `<+>`:      forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Neutral for `<+>`:      forall a,     a <+> neutral   == a      forall a,     neutral <+> a   == a  + Inverse for `<+>`:      forall a,     a <+> inverse a == neutral      forall a,     inverse a <+> a == neutral`

Parameters: ty
Constraints: MonoidV ty
Methods:
`inverse : ty -> ty`
`groupInverseIsInverseR : (r : ty) -> inverse r <+> r = neutral`

Implementations:
`AbelianGroup ty -> Group ty`
`GroupHomomorphism a b -> Group a`
`GroupHomomorphism a b -> Group b`
`Ring ty -> Group ty`
`inverse : Group ty => ty -> ty`
Visibility: public export
`groupInverseIsInverseR : {auto __con : Group ty} -> (r : ty) -> inverse r <+> r = neutral`
Visibility: public export
`interface AbelianGroup : Type -> Type`
`  Sets equipped with a single binary operation that is associative  and commutative, along with a neutral element for that binary  operation and inverses for all elements. Satisfies the following  laws:    + Associativity of `<+>`:      forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:      forall a b,   a <+> b         == b <+> a  + Neutral for `<+>`:      forall a,     a <+> neutral   == a      forall a,     neutral <+> a   == a  + Inverse for `<+>`:      forall a,     a <+> inverse a == neutral      forall a,     inverse a <+> a == neutral`

Parameters: ty
Constraints: Group ty
Methods:
`groupOpIsCommutative : (l : ty) -> (r : ty) -> l <+> r = r <+> l`
`groupOpIsCommutative : {auto __con : AbelianGroup ty} -> (l : ty) -> (r : ty) -> l <+> r = r <+> l`
Visibility: public export
`interface GroupHomomorphism : Type -> Type -> Type`
`  A homomorphism is a mapping that preserves group structure.`

Parameters: a, b
Constraints: Group a, Group b
Methods:
`to : a -> b`
`toGroup : (x : a) -> (y : a) -> to (x <+> y) = to x <+> to y`
`to : GroupHomomorphism a b => a -> b`
Visibility: public export
`toGroup : {auto __con : GroupHomomorphism a b} -> (x : a) -> (y : a) -> to (x <+> y) = to x <+> to y`
Visibility: public export
`interface Ring : Type -> Type`
`  Sets equipped with two binary operations, one associative and  commutative supplied with a neutral element, and the other  associative, with distributivity laws relating the two operations.  Satisfies the following laws:    + Associativity of `<+>`:      forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:      forall a b,   a <+> b         == b <+> a  + Neutral for `<+>`:      forall a,     a <+> neutral   == a      forall a,     neutral <+> a   == a  + Inverse for `<+>`:      forall a,     a <+> inverse a == neutral      forall a,     inverse a <+> a == neutral  + Associativity of `<.>`:      forall a b c, a <.> (b <.> c) == (a <.> b) <.> c  + Distributivity of `<.>` and `<+>`:      forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)      forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)`

Parameters: ty
Constraints: Group ty
Methods:
`(<.>) : ty -> ty -> ty`
Fixity Declaration: infixl operator, level 7
`ringOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <.> r) = (l <.> c) <.> r`
`ringOpIsDistributiveL : (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)`
`ringOpIsDistributiveR : (l : ty) -> (c : ty) -> (r : ty) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)`

Implementation:
`RingWithUnity ty -> Ring ty`
`(<.>) : Ring ty => ty -> ty -> ty`
Visibility: public export
Fixity Declaration: infixl operator, level 7
`ringOpIsAssociative : {auto __con : Ring ty} -> (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <.> r) = (l <.> c) <.> r`
Visibility: public export
`ringOpIsDistributiveL : {auto __con : Ring ty} -> (l : ty) -> (c : ty) -> (r : ty) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)`
Visibility: public export
`ringOpIsDistributiveR : {auto __con : Ring ty} -> (l : ty) -> (c : ty) -> (r : ty) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)`
Visibility: public export
`interface RingWithUnity : Type -> Type`
`  Sets equipped with two binary operations, one associative and  commutative supplied with a neutral element, and the other  associative supplied with a neutral element, with distributivity  laws relating the two operations. Satisfies the following laws:    +  Associativity of `<+>`:      forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:      forall a b,   a <+> b         == b <+> a  + Neutral for `<+>`:      forall a,     a <+> neutral   == a      forall a,     neutral <+> a   == a  + Inverse for `<+>`:      forall a,     a <+> inverse a == neutral      forall a,     inverse a <+> a == neutral  + Associativity of `<.>`:      forall a b c, a <.> (b <.> c) == (a <.> b) <.> c  + Neutral for `<.>`:      forall a,     a <.> unity     == a      forall a,     unity <.> a     == a  + Distributivity of `<.>` and `<+>`:      forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)      forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)`

Parameters: ty
Constraints: Ring ty
Methods:
`unity : ty`
`unityIsRingIdL : (l : ty) -> l <.> unity = l`
`unityIsRingIdR : (r : ty) -> unity <.> r = r`

Implementation:
`Field ty -> RingWithUnity ty`
`unity : RingWithUnity ty => ty`
Visibility: public export
`unityIsRingIdL : {auto __con : RingWithUnity ty} -> (l : ty) -> l <.> unity = l`
Visibility: public export
`unityIsRingIdR : {auto __con : RingWithUnity ty} -> (r : ty) -> unity <.> r = r`
Visibility: public export
`interface Field : Type -> Type`
`  Sets equipped with two binary operations – both associative,  commutative and possessing a neutral element – and distributivity  laws relating the two operations. All elements except the additive  identity should have a multiplicative inverse. Should (but may  not) satisfy the following laws:    + Associativity of `<+>`:      forall a b c, a <+> (b <+> c) == (a <+> b) <+> c  + Commutativity of `<+>`:      forall a b,   a <+> b         == b <+> a  + Neutral for `<+>`:      forall a,     a <+> neutral   == a      forall a,     neutral <+> a   == a  + Inverse for `<+>`:      forall a,     a <+> inverse a == neutral      forall a,     inverse a <+> a == neutral  + Associativity of `<.>`:      forall a b c, a <.> (b <.> c) == (a <.> b) <.> c  + Unity for `<.>`:      forall a,     a <.> unity     == a      forall a,     unity <.> a     == a  + InverseM of `<.>`, except for neutral      forall a /= neutral,  a <.> inverseM a == unity      forall a /= neutral,  inverseM a <.> a == unity  + Distributivity of `<.>` and `<+>`:      forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)      forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)`

Parameters: ty
Constraints: RingWithUnity ty
Methods:
`inverseM : (x : ty) -> Not (x = neutral) -> ty`
`inverseM : {auto __con : Field ty} -> (x : ty) -> Not (x = neutral) -> ty`
Visibility: public export