@@ -123,7 +123,7 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
123123||| + Inverse for `<+>`:
124124||| forall a, a <+> inverse a == neutral
125125||| forall a, inverse a <+> a == neutral
126−||| + Associativity of `<*>a:
126+||| + Associativity of `<*>`:
127127||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
128128||| + Neutral for `<*>`:
129129||| forall a, a <*> unity == a
@@ -264,9 +264,61 @@ class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a w
264264
265265class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
266266
267+-- Fields.
268+||| Sets equipped with two binary operations, both associative and commutative
269+||| supplied with a neutral element, with
270+||| distributivity laws relating the two operations. Must satisfy the following
271+||| laws:
272+|||
273+||| + Associativity of `<+>`:
274+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
275+||| + Commutativity of `<+>`:
276+||| forall a b, a <+> b == b <+> a
277+||| + Neutral for `<+>`:
278+||| forall a, a <+> neutral == a
279+||| forall a, neutral <+> a == a
280+||| + Inverse for `<+>`:
281+||| forall a, a <+> inverse a == neutral
282+||| forall a, inverse a <+> a == neutral
283+||| + Associativity of `<*>`:
284+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
285+||| + Unity for `<*>`:
286+||| forall a, a <*> unity == a
287+||| forall a, unity <*> a == a
288+||| + InverseM of `<*>`:
289+||| forall a, a <*> inverseM a == unity
290+||| forall a, inverseM a <*> a == unity
291+||| + Distributivity of `<*>` and `<->`:
292+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
293+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
294+class RingWithUnity a => Field a where
295+ inverseM : a -> a
296+
297+class (VerifiedRing a, Field a) => VerifiedField a where
298+ total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
299+ total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
300+
301+-- vector spaces.
302+||| A Vector Space over a Field can be considered as an additive Abeliean Group
303+||| of Vectors adjoined to the Field structure by distributivity laws relating
304+||| the two operations. Such that we satisfy the following laws:
305+|||
306+||| + Unity for `<*>`:
307+||| forall a, a <*> unity == a
308+||| forall a, unity <*> a == a
309+||| + Distributivity of `<*>` and `<+>`:
310+||| forall a x y, a <*> (x <+> y) == (a <*> x) <+> (a <*> y)
311+||| forall a b x, (a <+> b) <*> x == (a <*> x) <+> (b <*> x)
312+class (Field a, AbelianGroup a) => VectorSpace a a where {}
313+
314+class (VerifiedField a, VerifiedAbelianGroup a, VectorSpace a a) => VerifiedVectorSpace a a where
315+ total vectorspaceScalarUnityIsUnityL : (l : a) -> l <*> unity = l
316+ total vectorspaceScalarUnityIsUnityR : (r : a) -> unity <*> r = r
317+ total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : a) -> s <*> (x <+> y) = (s <*> x) <+> (s <*> y)
318+ total vectorspaceScalarIsDistributiveWRTFieldAddition : (s, t : a) -> (x : a) -> (s <+> t) <*> x = (s <*> x) <+> (t <*> x)
319+
267320
268321-- XXX todo:
269−-- Fields and vector spaces.
270322-- Structures where "abs" make sense.
271323-- Euclidean domains, etc.
272324-- Where to put fromInteger and fromRational?