Idris2Doc : Control.Algebra

Control.Algebra

(<.>) : Ringty => ty -> ty -> ty

Fixity Declaration: infixl operator, level 7
interfaceAbelianGroup : 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
interfaceField : 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
interfaceGroup : 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) -> inverser<+>r = neutral

Implementations:
AbelianGroupty -> Groupty
GroupHomomorphismab -> Groupa
GroupHomomorphismab -> Groupb
Ringty -> Groupty
interfaceGroupHomomorphism : 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) = tox<+>toy
interfaceMonoidV : Type -> Type
Parameters: ty
Constraints: Monoid ty, SemigroupV ty
Methods:
monoidNeutralIsNeutralL : (l : ty) -> l<+>neutral = l
monoidNeutralIsNeutralR : (r : ty) -> neutral<+>r = r

Implementation: 
MonoidVty => MonoidV (Identityty)
interfaceRing : 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: 
RingWithUnityty -> Ringty
interfaceRingWithUnity : 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: 
Fieldty -> RingWithUnityty
interfaceSemigroupV : Type -> Type
Parameters: ty
Constraints: Semigroup ty
Methods:
semigroupOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) -> l<+> (c<+>r) = (l<+>c) <+>r

Implementation: 
SemigroupVty => SemigroupV (Identityty)
groupInverseIsInverseR : Groupty => (r : ty) -> inverser<+>r = neutral
groupOpIsCommutative : AbelianGroupty => (l : ty) -> (r : ty) -> l<+>r = r<+>l
inverse : Groupty => ty -> ty
inverseM : Fieldty => (x : ty) -> Not (x = neutral) -> ty
monoidNeutralIsNeutralL : MonoidVty => (l : ty) -> l<+>neutral = l
monoidNeutralIsNeutralR : MonoidVty => (r : ty) -> neutral<+>r = r
ringOpIsAssociative : Ringty => (l : ty) -> (c : ty) -> (r : ty) -> l<.> (c<.>r) = (l<.>c) <.>r
ringOpIsDistributiveL : Ringty => (l : ty) -> (c : ty) -> (r : ty) -> l<.> (c<+>r) = (l<.>c) <+> (l<.>r)
ringOpIsDistributiveR : Ringty => (l : ty) -> (c : ty) -> (r : ty) -> (l<+>c) <.>r = (l<.>r) <+> (c<.>r)
semigroupOpIsAssociative : SemigroupVty => (l : ty) -> (c : ty) -> (r : ty) -> l<+> (c<+>r) = (l<+>c) <+>r
to : GroupHomomorphismab => a -> b
toGroup : GroupHomomorphismab => (x : a) -> (y : a) -> to (x<+>y) = tox<+>toy
unity : RingWithUnityty => ty
unityIsRingIdL : RingWithUnityty => (l : ty) -> l<.>unity = l
unityIsRingIdR : RingWithUnityty => (r : ty) -> unity<.>r = r