diff --git a/libs/base/Control/Isomorphism.idr b/libs/base/Control/Isomorphism.idr
index f308a6b5c8..9302980f50 100644
--- a/libs/base/Control/Isomorphism.idr
+++ b/libs/base/Control/Isomorphism.idr
@@ -38,12 +38,31 @@ Category Iso where
   id = isoRefl
   (.) = flip isoTrans
 
+-- TODO : Prove these postulates! ------
+
+postulate private
+iso_semigroupOpIsAssociative : (l, c, r : Iso a a) ->
+  isoTrans l (isoTrans c r) = isoTrans (isoTrans l c) r
+
+postulate private
+iso_monoidNeutralIsNeutralL : (l : Iso a a) -> isoTrans l isoRefl = l
+
+postulate private
+iso_monoidNeutralIsNeutralR : (r : Iso a a) -> isoTrans isoRefl r = r
+
+----------------------------------------
+
 Semigroup (Iso a a) where
   (<+>) = isoTrans
 
+  semigroupOpIsAssociative = iso_semigroupOpIsAssociative
+
 Monoid (Iso a a) where
   neutral = isoRefl
 
+  monoidNeutralIsNeutralL = iso_monoidNeutralIsNeutralL
+  monoidNeutralIsNeutralR = iso_monoidNeutralIsNeutralR
+
 ||| Isomorphism is symmetric
 isoSym : Iso a b -> Iso b a
 isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
diff --git a/libs/base/Control/Monad/Identity.idr b/libs/base/Control/Monad/Identity.idr
index d3f2b1f266..115becc177 100644
--- a/libs/base/Control/Monad/Identity.idr
+++ b/libs/base/Control/Monad/Identity.idr
@@ -33,5 +33,13 @@ Enum a => Enum (Identity a) where
 (Semigroup a) => Semigroup (Identity a) where
   (<+>) x y = Id (runIdentity x <+> runIdentity y)
 
+  semigroupOpIsAssociative (Id l) (Id c) (Id r) =
+    rewrite semigroupOpIsAssociative l c r in Refl
+
 (Monoid a) => Monoid (Identity a) where
-  neutral = Id (neutral)
\ No newline at end of file
+  neutral = Id (neutral)
+
+  monoidNeutralIsNeutralL (Id l) =
+    rewrite monoidNeutralIsNeutralL l in Refl
+  monoidNeutralIsNeutralR (Id r) =
+    rewrite monoidNeutralIsNeutralR r in Refl
diff --git a/libs/base/Data/Morphisms.idr b/libs/base/Data/Morphisms.idr
index 559342f769..71f3151573 100644
--- a/libs/base/Data/Morphisms.idr
+++ b/libs/base/Data/Morphisms.idr
@@ -28,18 +28,60 @@ Applicative (Morphism r) where
 Monad (Morphism r) where
   (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
 
+-- Postulates --------------------------
+
+-- These are required for implementing verified interfaces.
+-- TODO : Prove them.
+
+postulate private
+morphism_assoc : Semigroup a => (f, g, h : r -> a) ->
+  Mor (\r => f r <+> (g r <+> h r)) = Mor (\r => f r <+> g r <+> h r)
+
+postulate private
+morphism_neutl : Monoid a => (f : r -> a) ->
+  Mor (\r => f r <+> Prelude.Algebra.neutral) = Mor f
+
+postulate private
+morphism_neutr : Monoid a => (f : r -> a) ->
+  Mor (\r => Prelude.Algebra.neutral <+> f r) = Mor f
+
+postulate private
+kleisli_assoc : (Semigroup a, Applicative f) => (i, j, k : s -> f a) ->
+   Kleisli (\r => pure (<+>) <*> i r <*> (pure (<+>) <*> j r <*> k r)) =
+     Kleisli (\r => pure (<+>) <*> (pure (<+>) <*> i r <*> j r) <*> k r)
+
+postulate private
+kleisli_neutl : (Monoid a, Applicative f) => (g : r -> f a) ->
+  Kleisli (\x => pure (<+>) <*> g x <*> pure Prelude.Algebra.neutral) = Kleisli g
+
+postulate private
+kleisli_neutr : (Monoid a, Applicative f) => (g : r -> f a) ->
+  Kleisli (\x => pure (<+>) <*> pure Prelude.Algebra.neutral <*> g x) = Kleisli g
+
+----------------------------------------
+
 Semigroup a => Semigroup (Morphism r a) where
   f <+> g = [| f <+> g |]
 
+  semigroupOpIsAssociative (Mor f) (Mor g) (Mor h) = morphism_assoc f g h
+
 Monoid a => Monoid (Morphism r a) where
   neutral = [| neutral |]
 
+  monoidNeutralIsNeutralL (Mor f) = morphism_neutl f
+  monoidNeutralIsNeutralR (Mor f) = morphism_neutr f
+
 Semigroup (Endomorphism a) where
   (Endo f) <+> (Endo g) = Endo $ g . f
 
+  semigroupOpIsAssociative (Endo _) (Endo _) (Endo _) = Refl
+
 Monoid (Endomorphism a) where
   neutral = Endo id
 
+  monoidNeutralIsNeutralL (Endo _) = Refl
+  monoidNeutralIsNeutralR (Endo _) = Refl
+
 Functor f => Functor (Kleislimorphism f a) where
   map f (Kleisli g) = Kleisli (map f . g)
 
@@ -51,12 +93,17 @@ Monad f => Monad (Kleislimorphism f a) where
   (Kleisli f) >>= g = Kleisli $ \r => applyKleisli (g !(f r)) r
 
 -- Applicative is a bit too strong, but there is no suitable superclass
-(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where
+(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f s a) where
   f <+> g = [| f <+> g |]
 
+  semigroupOpIsAssociative (Kleisli i) (Kleisli j) (Kleisli k) = kleisli_assoc i j k
+
 (Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where
   neutral = [| neutral |]
 
+  monoidNeutralIsNeutralL (Kleisli g) = kleisli_neutl g
+  monoidNeutralIsNeutralR (Kleisli g) = kleisli_neutr g
+
 Cast (Endomorphism a) (Morphism a a) where
   cast (Endo f) = Mor f
 
diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
index b95bc08a7e..a4e74ea7b6 100644
--- a/libs/contrib/Control/Algebra.idr
+++ b/libs/contrib/Control/Algebra.idr
@@ -19,6 +19,8 @@ infixl 7 <.>
 interface Monoid a => Group a where
   inverse : a -> a
 
+  groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
+
 (<->) : Group a => a -> a -> a
 (<->) left right = left <+> (inverse right)
 
@@ -36,7 +38,8 @@ interface Monoid a => Group a where
 ||| + Inverse for `<+>`:
 |||     forall a,     a <+> inverse a == neutral
 |||     forall a,     inverse a <+> a == neutral
-interface Group a => AbelianGroup a where { }
+interface Group a => AbelianGroup a where
+  abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
 
 ||| Sets equipped with two binary operations, one associative and commutative
 ||| supplied with a neutral element, and the other associative, with
@@ -61,6 +64,10 @@ interface Group a => AbelianGroup a where { }
 interface AbelianGroup a => Ring a where
   (<.>) : a -> a -> a
 
+  ringOpIsAssociative   : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
+  ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
+  ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
+
 ||| 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.  Must
@@ -87,6 +94,34 @@ interface AbelianGroup a => Ring a where
 interface Ring a => RingWithUnity a where
   unity : a
 
+  ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
+  ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
+
+||| Sets equipped with two binary operations, one associative and
+||| commutative supplied with a neutral element, and the other
+||| associative and commutative, with distributivity laws relating the
+||| two operations. Must 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
+||| + Commutativity of `<.>`:
+|||     forall a b,   a <.> b         == b <.> 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)
+interface Ring a => CommutativeRing a where
+  ringOpIsCommutative : (x, y : a) -> x <.> y = y <.> x
+
 ||| 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 must have a
@@ -104,6 +139,8 @@ interface Ring a => RingWithUnity a where
 |||     forall a,     inverse a <+> a == neutral
 ||| + Associativity of `<.>`:
 |||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+||| + Commutativity of `<.>`:
+|||     forall a b,   a <.> b         == b <.> a
 ||| + Unity for `<.>`:
 |||     forall a,     a <.> unity     == a
 |||     forall a,     unity <.> a     == a
@@ -113,9 +150,12 @@ interface Ring a => RingWithUnity a where
 ||| + 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)
-interface RingWithUnity a => Field a where
+interface (RingWithUnity a, CommutativeRing a) => Field a where
   inverseM : (x : a) -> Not (x = Algebra.neutral) -> a
 
+  fieldInverseIsInverseR : (r : a) -> (p : Not (r = Algebra.neutral)) ->
+    inverseM r p <.> r = Algebra.unity
+
 sum' : (Foldable t, Monoid a) => t a -> a
 sum' = concat
 
diff --git a/libs/contrib/Control/Algebra/Lattice.idr b/libs/contrib/Control/Algebra/Lattice.idr
index d2e418d779..e4a34ce57e 100644
--- a/libs/contrib/Control/Algebra/Lattice.idr
+++ b/libs/contrib/Control/Algebra/Lattice.idr
@@ -1,7 +1,7 @@
 module Control.Algebra.Lattice
 
 import Control.Algebra
-import Data.Heap
+import Data.Bool.Extra
 
 %access public export
 
@@ -19,14 +19,9 @@ import Data.Heap
 interface JoinSemilattice a where
   join : a -> a -> a
 
-implementation JoinSemilattice Nat where
-  join = maximum
-
-implementation Ord a => JoinSemilattice (MaxiphobicHeap a) where
-  join = merge
-
-JoinSemilattice Bool where
-  join a b = a || b
+  joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
+  joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l
+  joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e
 
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent.  Must satisfy the following laws:
@@ -42,11 +37,9 @@ JoinSemilattice Bool where
 interface MeetSemilattice a where
   meet : a -> a -> a
 
-implementation MeetSemilattice Nat where
-  meet = minimum
-
-MeetSemilattice Bool where
-  meet a b = a && b
+  meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
+  meetSemilatticeMeetIsCommutative : (l, r : a)    -> meet l r = meet r l
+  meetSemilatticeMeetIsIdempotent  : (e : a)       -> meet e e = e
 
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent and supplied with a unitary element.  Must satisfy the following
@@ -66,11 +59,7 @@ MeetSemilattice Bool where
 interface JoinSemilattice a => BoundedJoinSemilattice a where
   bottom  : a
 
-implementation BoundedJoinSemilattice Nat where
-  bottom = Z
-
-BoundedJoinSemilattice Bool where
-  bottom = False
+  joinBottomIsIdentity : (x : a) -> join x Lattice.bottom = x
 
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent and supplied with a unitary element.  Must satisfy the following
@@ -90,8 +79,7 @@ BoundedJoinSemilattice Bool where
 interface MeetSemilattice a => BoundedMeetSemilattice a where
   top : a
 
-BoundedMeetSemilattice Bool where
-  top = True
+  meetTopIsIdentity : (x : a) -> meet x Lattice.top = x
 
 ||| Sets equipped with two binary operations that are both commutative,
 ||| associative and idempotent, along with absorbtion laws for relating the two
@@ -111,10 +99,6 @@ BoundedMeetSemilattice Bool where
 |||     forall a b,   join a (meet a b) == a
 interface (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
 
-implementation Lattice Nat where { }
-
-Lattice Bool where { }
-
 ||| Sets equipped with two binary operations that are both commutative,
 ||| associative and idempotent and supplied with neutral elements, along with
 ||| absorbtion laws for relating the two binary operations.  Must satisfy the
@@ -137,4 +121,50 @@ Lattice Bool where { }
 |||     forall a,     join a bottom     == bottom
 interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
 
+-- Implementations ---------------------
+
+-- Nat
+
+JoinSemilattice Nat where
+  join = maximum
+  joinSemilatticeJoinIsAssociative = maximumAssociative
+  joinSemilatticeJoinIsCommutative = maximumCommutative
+  joinSemilatticeJoinIsIdempotent  = maximumIdempotent
+
+MeetSemilattice Nat where
+  meet = minimum
+  meetSemilatticeMeetIsAssociative = minimumAssociative
+  meetSemilatticeMeetIsCommutative = minimumCommutative
+  meetSemilatticeMeetIsIdempotent  = minimumIdempotent
+
+BoundedJoinSemilattice Nat where
+  bottom = Z
+  joinBottomIsIdentity = maximumZeroNLeft
+
+Lattice Nat where { }
+
+-- Bool
+
+JoinSemilattice Bool where
+  join a b = a || b
+  joinSemilatticeJoinIsAssociative = orAssociative
+  joinSemilatticeJoinIsCommutative = orCommutative
+  joinSemilatticeJoinIsIdempotent = orSameNeutral
+
+MeetSemilattice Bool where
+  meet a b = a && b
+  meetSemilatticeMeetIsAssociative = andAssociative
+  meetSemilatticeMeetIsCommutative = andCommutative
+  meetSemilatticeMeetIsIdempotent = andSameNeutral
+
+BoundedJoinSemilattice Bool where
+  bottom = False
+  joinBottomIsIdentity = orFalseNeutral
+
+BoundedMeetSemilattice Bool where
+  top = True
+  meetTopIsIdentity = andTrueNeutral
+
 BoundedLattice Bool where { }
+
+Lattice Bool where { }
diff --git a/libs/contrib/Control/Algebra/Laws.idr b/libs/contrib/Control/Algebra/Laws.idr
index 46e9356e82..4b9c040aa4 100644
--- a/libs/contrib/Control/Algebra/Laws.idr
+++ b/libs/contrib/Control/Algebra/Laws.idr
@@ -2,14 +2,13 @@ module Control.Algebra.Laws
 
 import Prelude.Algebra as A
 import Control.Algebra as Alg
-import Interfaces.Verified
 
-%access export
+%access public export
 
 -- Monoids
 
 ||| Inverses are unique.
-uniqueInverse : VerifiedMonoid t => (x, y, z : t) ->
+uniqueInverse : Monoid t => (x, y, z : t) ->
   y <+> x = A.neutral -> x <+> z = A.neutral -> y = z
 uniqueInverse x y z p q =
   rewrite sym $ monoidNeutralIsNeutralL y in
@@ -22,7 +21,7 @@ uniqueInverse x y z p q =
 -- Groups
 
 ||| Only identity is self-squaring.
-selfSquareId : VerifiedGroup t => (x : t) ->
+selfSquareId : Group t => (x : t) ->
   x <+> x = x -> x = A.neutral
 selfSquareId x p =
   rewrite sym $ monoidNeutralIsNeutralR x in
@@ -32,7 +31,7 @@ selfSquareId x p =
       Refl
 
 ||| Inverse elements commute.
-inverseCommute : VerifiedGroup t => (x, y : t) ->
+inverseCommute : Group t => (x, y : t) ->
   y <+> x = A.neutral -> x <+> y = A.neutral
 inverseCommute x y p = selfSquareId (x <+> y) prop where
   prop : (x <+> y) <+> (x <+> y) = x <+> y
@@ -44,13 +43,13 @@ inverseCommute x y p = selfSquareId (x <+> y) prop where
         Refl
 
 ||| Every element has a right inverse.
-groupInverseIsInverseL : VerifiedGroup t => (x : t) ->
+groupInverseIsInverseL : Group t => (x : t) ->
   x <+> inverse x = Algebra.neutral
 groupInverseIsInverseL x =
   inverseCommute x (inverse x) (groupInverseIsInverseR x)
 
 ||| -(-x) = x in any verified group.
-inverseSquaredIsIdentity : VerifiedGroup t => (x : t) ->
+inverseSquaredIsIdentity : Group t => (x : t) ->
   inverse (inverse x) = x
 inverseSquaredIsIdentity x =
   let x' = inverse x in
@@ -62,7 +61,7 @@ inverseSquaredIsIdentity x =
       (groupInverseIsInverseR x)
 
 ||| If every square in a group is identity, the group is commutative.
-squareIdCommutative : VerifiedGroup t => (x, y : t) ->
+squareIdCommutative : Group t => (x, y : t) ->
   ((a : t) -> a <+> a = A.neutral) ->
   x <+> y = y <+> x
 squareIdCommutative x y p =
@@ -80,7 +79,7 @@ squareIdCommutative x y p =
           p x
 
 ||| -0 = 0 in any verified group.
-inverseNeutralIsNeutral : VerifiedGroup t =>
+inverseNeutralIsNeutral : Group t =>
   inverse (the t A.neutral) = A.neutral
 inverseNeutralIsNeutral {t} =
   let e = the t neutral in
@@ -89,7 +88,7 @@ inverseNeutralIsNeutral {t} =
         inverseSquaredIsIdentity e
 
 ||| -(x + y) = -y + -x in any verified group.
-inverseOfSum : VerifiedGroup t => (l, r : t) ->
+inverseOfSum : Group t => (l, r : t) ->
   inverse (l <+> r) = inverse r <+> inverse l
 inverseOfSum {t} l r =
   let
@@ -120,7 +119,7 @@ inverseOfSum {t} l r =
               Refl
 
 ||| y = z if x + y = x + z.
-cancelLeft : VerifiedGroup t => (x, y, z : t) ->
+cancelLeft : Group t => (x, y, z : t) ->
   x <+> y = x <+> z -> y = z
 cancelLeft x y z p =
   rewrite sym $ monoidNeutralIsNeutralR y in
@@ -132,7 +131,7 @@ cancelLeft x y z p =
   monoidNeutralIsNeutralR z
 
 ||| y = z if y + x = z + x.
-cancelRight : VerifiedGroup t => (x, y, z : t) ->
+cancelRight : Group t => (x, y, z : t) ->
   y <+> x = z <+> x -> y = z
 cancelRight x y z p =
   rewrite sym $ monoidNeutralIsNeutralL y in
@@ -144,7 +143,7 @@ cancelRight x y z p =
   monoidNeutralIsNeutralL z
 
 ||| For any a and b, ax = b and ya = b have solutions.
-latinSquareProperty : VerifiedGroup t => (a, b : t) ->
+latinSquareProperty : Group t => (a, b : t) ->
   ((x : t ** a <+> x = b),
     (y : t ** y <+> a = b))
 latinSquareProperty a b =
@@ -159,17 +158,17 @@ latinSquareProperty a b =
           monoidNeutralIsNeutralL b))
 
 ||| For any a, b, x, the solution to ax = b is unique.
-uniqueSolutionR : VerifiedGroup t => (a, b, x, y : t) ->
+uniqueSolutionR : Group t => (a, b, x, y : t) ->
   a <+> x = b -> a <+> y = b -> x = y
 uniqueSolutionR a b x y p q = cancelLeft a x y $ trans p (sym q)
 
 ||| For any a, b, y, the solution to ya = b is unique.
-uniqueSolutionL : VerifiedGroup t => (a, b, x, y : t) ->
+uniqueSolutionL : Group t => (a, b, x, y : t) ->
   x <+> a = b -> y <+> a = b -> x = y
 uniqueSolutionL a b x y p q = cancelRight a x y $ trans p (sym q)
 
 ||| -(x + y) = -x + -y in any verified abelian group.
-inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->
+inverseDistributesOverGroupOp : AbelianGroup t => (l, r : t) ->
   inverse (l <+> r) = inverse l <+> inverse r
 inverseDistributesOverGroupOp l r =
   rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in
@@ -178,7 +177,7 @@ inverseDistributesOverGroupOp l r =
 -- Rings
 
 ||| Anything multiplied by zero yields zero back in a verified ring.
-multNeutralAbsorbingL : VerifiedRing t => (r : t) ->
+multNeutralAbsorbingL : Ring t => (r : t) ->
   A.neutral <.> r = A.neutral
 multNeutralAbsorbingL {t} r =
   let
@@ -196,7 +195,7 @@ multNeutralAbsorbingL {t} r =
   groupInverseIsInverseR exr
 
 ||| Anything multiplied by zero yields zero back in a verified ring.
-multNeutralAbsorbingR : VerifiedRing t => (l : t) ->
+multNeutralAbsorbingR : Ring t => (l : t) ->
   l <.> A.neutral = A.neutral
 multNeutralAbsorbingR {t} l =
   let
@@ -215,7 +214,7 @@ multNeutralAbsorbingR {t} l =
 
 ||| Inverse operator can be extracted before multiplication.
 ||| (-x)y = -(xy)
-multInverseInversesL : VerifiedRing t => (l, r : t) ->
+multInverseInversesL : Ring t => (l, r : t) ->
   inverse l <.> r = inverse (l <.> r)
 multInverseInversesL l r =
   let
@@ -234,7 +233,7 @@ multInverseInversesL l r =
 
 ||| Inverse operator can be extracted before multiplication.
 ||| x(-y) = -(xy)
-multInverseInversesR : VerifiedRing t => (l, r : t) ->
+multInverseInversesR : Ring t => (l, r : t) ->
   l <.> inverse r = inverse (l <.> r)
 multInverseInversesR l r =
   let
@@ -254,7 +253,7 @@ multInverseInversesR l r =
 ||| Multiplication of inverses is the same as multiplication of
 ||| original elements.
 ||| (-x)(-y) = xy
-multNegativeByNegativeIsPositive : VerifiedRing t => (l, r : t) ->
+multNegativeByNegativeIsPositive : Ring t => (l, r : t) ->
   inverse l <.> inverse r = l <.> r
 multNegativeByNegativeIsPositive l r =
     rewrite multInverseInversesR (inverse l) r in
@@ -262,14 +261,14 @@ multNegativeByNegativeIsPositive l r =
     rewrite inverseSquaredIsIdentity l in
     Refl
 
-inverseOfUnityR : VerifiedRingWithUnity t => (x : t) ->
+inverseOfUnityR : RingWithUnity t => (x : t) ->
   inverse Alg.unity <.> x = inverse x
 inverseOfUnityR x =
   rewrite multInverseInversesL Alg.unity x in
     rewrite ringWithUnityIsUnityR x in
       Refl
 
-inverseOfUnityL : VerifiedRingWithUnity t => (x : t) ->
+inverseOfUnityL : RingWithUnity t => (x : t) ->
   x <.> inverse Alg.unity = inverse x
 inverseOfUnityL x =
   rewrite multInverseInversesR x Alg.unity in
diff --git a/libs/contrib/Control/Algebra/NumericImplementations.idr b/libs/contrib/Control/Algebra/NumericImplementations.idr
index 12294cb910..25341d3240 100644
--- a/libs/contrib/Control/Algebra/NumericImplementations.idr
+++ b/libs/contrib/Control/Algebra/NumericImplementations.idr
@@ -3,6 +3,7 @@
 module Control.Algebra.NumericImplementations
 
 import Control.Algebra
+import Control.Algebra.Laws
 import Control.Algebra.VectorSpace
 import Data.Complex
 import Data.ZZ
@@ -14,119 +15,368 @@ import Data.ZZ
 Semigroup Integer where
   (<+>) = (+)
 
+  semigroupOpIsAssociative = believe_me Integer
+
 Monoid Integer where
   neutral = 0
 
+  monoidNeutralIsNeutralL = believe_me Integer
+  monoidNeutralIsNeutralR = believe_me Integer
+
 Group Integer where
   inverse = (* -1)
 
+  groupInverseIsInverseR = believe_me Integer
+
 AbelianGroup Integer where
+  abelianGroupOpIsCommutative = believe_me Integer
 
 Ring Integer where
   (<.>) = (*)
 
+  ringOpIsAssociative   = believe_me Integer
+  ringOpIsDistributiveL = believe_me Integer
+  ringOpIsDistributiveR = believe_me Integer
+
 RingWithUnity Integer where
   unity = 1
 
+  ringWithUnityIsUnityL = believe_me Integer
+  ringWithUnityIsUnityR = believe_me Integer
+
 -- Int
 
 Semigroup Int where
   (<+>) = (+)
 
+  semigroupOpIsAssociative = believe_me Int
+
 Monoid Int where
   neutral = 0
 
+  monoidNeutralIsNeutralL = believe_me Int
+  monoidNeutralIsNeutralR = believe_me Int
+
 Group Int where
   inverse = (* -1)
 
+  groupInverseIsInverseR = believe_me Int
+
 AbelianGroup Int where
+  abelianGroupOpIsCommutative = believe_me Int
 
 Ring Int where
   (<.>) = (*)
 
+  ringOpIsAssociative   = believe_me Int
+  ringOpIsDistributiveL = believe_me Int
+  ringOpIsDistributiveR = believe_me Int
+
 RingWithUnity Int where
   unity = 1
 
+  ringWithUnityIsUnityL = believe_me Int
+  ringWithUnityIsUnityR = believe_me Int
+
 -- Double
 
 Semigroup Double where
   (<+>) = (+)
 
+  semigroupOpIsAssociative = believe_me Double
+
 Monoid Double where
   neutral = 0
 
+  monoidNeutralIsNeutralL = believe_me Double
+  monoidNeutralIsNeutralR = believe_me Double
+
 Group Double where
   inverse = (* -1)
 
+  groupInverseIsInverseR = believe_me Double
+
 AbelianGroup Double where
+  abelianGroupOpIsCommutative = believe_me Double
 
 Ring Double where
   (<.>) = (*)
 
+  ringOpIsAssociative   = believe_me Double
+  ringOpIsDistributiveL = believe_me Double
+  ringOpIsDistributiveR = believe_me Double
+
 RingWithUnity Double where
   unity = 1
 
+  ringWithUnityIsUnityL = believe_me Double
+  ringWithUnityIsUnityR = believe_me Double
+
+CommutativeRing Double where
+  ringOpIsCommutative = believe_me Double
+
 Field Double where
   inverseM f _ = 1 / f
 
+  fieldInverseIsInverseR = believe_me Double
+
 -- Nat
 
 [PlusNatSemi] Semigroup Nat where
   (<+>) = (+)
+  semigroupOpIsAssociative = plusAssociative
 
 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
   neutral = 0
+  monoidNeutralIsNeutralL = plusZeroRightNeutral
+  monoidNeutralIsNeutralR = plusZeroLeftNeutral
 
 [MultNatSemi] Semigroup Nat where
   (<+>) = (*)
+  semigroupOpIsAssociative = multAssociative
 
 [MultNatMonoid] Monoid Nat using MultNatSemi where
   neutral = 1
+  monoidNeutralIsNeutralL = multOneRightNeutral
+  monoidNeutralIsNeutralR = multOneLeftNeutral
 
 -- ZZ
 
 [PlusZZSemi] Semigroup ZZ where
   (<+>) = (+)
+  semigroupOpIsAssociative = plusAssociativeZ
 
 [PlusZZMonoid] Monoid ZZ using PlusZZSemi where
   neutral = 0
+  monoidNeutralIsNeutralL = plusZeroRightNeutralZ
+  monoidNeutralIsNeutralR = plusZeroLeftNeutralZ
 
 Group ZZ using PlusZZMonoid where
   inverse = (* -1)
 
+  groupInverseIsInverseR k =
+    rewrite sym $ multCommutativeZ (NegS 0) k in
+    rewrite multNegLeftZ 0 k in
+    rewrite multOneLeftNeutralZ k in
+    plusNegateInverseRZ k
+
 AbelianGroup ZZ where
+  abelianGroupOpIsCommutative = plusCommutativeZ
 
 [MultZZSemi] Semigroup ZZ where
   (<+>) = (*)
+  semigroupOpIsAssociative = multAssociativeZ
 
 [MultZZMonoid] Monoid ZZ using MultZZSemi where
   neutral = 1
+  monoidNeutralIsNeutralL = multOneRightNeutralZ
+  monoidNeutralIsNeutralR = multOneLeftNeutralZ
 
 Ring ZZ where
   (<.>) = (*)
+  ringOpIsAssociative = multAssociativeZ
+  ringOpIsDistributiveL = multDistributesOverPlusRightZ
+  ringOpIsDistributiveR = multDistributesOverPlusLeftZ
 
 RingWithUnity ZZ where
   unity = 1
+  ringWithUnityIsUnityL = multOneRightNeutralZ
+  ringWithUnityIsUnityR = multOneLeftNeutralZ
 
 -- Complex
 
 Semigroup a => Semigroup (Complex a) where
   (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
 
-Monoid a => Monoid (Complex a) where
+  semigroupOpIsAssociative (a :+ x) (b :+ y) (c :+ z) =
+    rewrite semigroupOpIsAssociative a b c in
+      rewrite semigroupOpIsAssociative x y z in
+        Refl
+
+Monoid t => Monoid (Complex t) where
   neutral = (neutral :+ neutral)
 
-Group a => Group (Complex a) where
-  inverse (r :+ i) = (inverse r :+ inverse i)
+  monoidNeutralIsNeutralL (a :+ x) =
+    rewrite monoidNeutralIsNeutralL a in
+      rewrite monoidNeutralIsNeutralL x in
+        Refl
 
-Ring a => AbelianGroup (Complex a) where {}
+  monoidNeutralIsNeutralR (a :+ x) =
+    rewrite monoidNeutralIsNeutralR a in
+      rewrite monoidNeutralIsNeutralR x in
+        Refl
 
-Ring a => Ring (Complex a) where
+Group t => Group (Complex t) where
+  inverse (r :+ i) = (inverse r :+ inverse i)
+
+  groupInverseIsInverseR (r :+ i) =
+    rewrite groupInverseIsInverseR r in
+      rewrite groupInverseIsInverseR i in
+        Refl
+
+AbelianGroup t => AbelianGroup (Complex t) where
+  abelianGroupOpIsCommutative (a :+ i) (b :+ j) =
+    rewrite abelianGroupOpIsCommutative a b in
+      rewrite abelianGroupOpIsCommutative i j in
+        Refl
+
+-- A simple helper lemma
+private abelianGroupRearrange : AbelianGroup t => (a, b, c, d : t) ->
+  a <+> b <+> (c <+> d) = a <+> c <+> (b <+> d)
+abelianGroupRearrange a b c d =
+  rewrite sym $ semigroupOpIsAssociative a b (c <+> d) in
+    rewrite semigroupOpIsAssociative b c d in
+      rewrite abelianGroupOpIsCommutative b c in
+    rewrite sym $ semigroupOpIsAssociative c b d in
+  semigroupOpIsAssociative a c (b <+> d)
+
+Ring t => Ring (Complex t) where
   (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
 
-RingWithUnity a => RingWithUnity (Complex a) where
+  ringOpIsDistributiveR (a :+ x) (b :+ y) (c :+ z) =
+    -- Distribute inverses (target z)
+    rewrite sym $ multInverseInversesR (x <+> y) z in
+      rewrite sym $ multInverseInversesR x z in
+        rewrite sym $ multInverseInversesR y z in
+    -- Shuffle terms
+    rewrite shuffle a b c x y (inverse z) in
+      rewrite shuffle a b z x y c in
+        Refl where
+    shuffle : (f, g, h, i, j, k : t) ->
+      (f <+> g) <.> h <+> (i <+> j) <.> k =
+        f <.> h <+> i <.> k <+> (g <.> h <+> j <.> k)
+    shuffle f g h i j k =
+      rewrite ringOpIsDistributiveR f g h in
+        rewrite ringOpIsDistributiveR i j k in
+      abelianGroupRearrange (f <.> h) (g <.> h) (i <.> k) (j <.> k)
+
+  ringOpIsDistributiveL (a :+ x) (b :+ y) (c :+ z) =
+    -- Distribute inverses (target x)
+    rewrite sym $ multInverseInversesL x (y <+> z) in
+      rewrite sym $ multInverseInversesL x y in
+        rewrite sym $ multInverseInversesL x z in
+    -- Shuffle terms
+    rewrite shuffle a b c (inverse x) y z in
+      rewrite shuffle a y z x b c in
+        Refl where
+    shuffle : (f, g, h, i, j, k : t) ->
+      f <.> (g <+> h) <+> i <.> (j <+> k) =
+        f <.> g <+> i <.> j <+> (f <.> h <+> i <.> k)
+    shuffle f g h i j k =
+      rewrite ringOpIsDistributiveL f g h in
+        rewrite ringOpIsDistributiveL i j k in
+      abelianGroupRearrange (f <.> g) (f <.> h) (i <.> j) (i <.> k)
+
+  ringOpIsAssociative (a :+ x) (b :+ y) (c :+ z) =
+
+    let
+      b' = inverse b
+      y' = inverse y
+      bz = b <.> z
+      yc = y <.> c
+      xbz = x <.> bz
+      xyc = x <.> yc
+      ay = a <.> y
+      ay' = a <.> y'
+      xb = x <.> b
+      ab = a <.> b
+      xb' = x <.> b'
+      xy' = x <.> y'
+      bc = b <.> c
+      y'z = y' <.> z
+        in
+
+    -- Distribute inverses (target y if possible, else b)
+    rewrite ringOpIsDistributiveL x bz yc in
+      rewrite inverseDistributesOverGroupOp xbz xyc in
+        rewrite sym $ multInverseInversesR x yc in
+          rewrite sym $ multInverseInversesL y c in
+        rewrite sym $ multInverseInversesR x bz in
+          rewrite sym $ multInverseInversesL b z in
+        rewrite sym $ multInverseInversesL y z in
+      rewrite sym $ multInverseInversesL (ay <+> xb) z in
+        rewrite inverseDistributesOverGroupOp ay xb in
+          rewrite sym $ multInverseInversesR a y in
+            rewrite sym $ multInverseInversesR x b in
+      rewrite sym $ multInverseInversesR x y in
+
+    -- Distribute multiplications
+    rewrite ringOpIsDistributiveR ab xy' z in
+      rewrite ringOpIsDistributiveR ay xb c in
+    rewrite ringOpIsDistributiveL a bz yc in
+      rewrite ringOpIsDistributiveL x bc y'z in
+    rewrite ringOpIsDistributiveL a bc y'z in
+      rewrite ringOpIsDistributiveR ab xy' c in
+        rewrite ringOpIsDistributiveR ay' xb' z in
+
+    -- Shuffle the real part
+    let
+      abc = a <.> bc
+      ay'z = a <.> y'z
+      xb'z = x <.> (b' <.> z)
+      xy'c = x <.> (y' <.> c)
+        in
+    rewrite shuffle abc ay'z xb'z xy'c in
+      rewrite regroup a x b c y' c y' z b' z in
+
+    -- Shuffle the imaginary part
+    let
+      abz = a <.> bz
+      ayc = a <.> yc
+      xbc = x <.> bc
+      xy'z = x <.> y'z
+        in
+    rewrite shuffle abz ayc xbc xy'z in
+      rewrite regroup a x b z y' z y c b c in
+
+    Refl where
+
+    shuffle : (p, q, r, s : t) ->
+      p <+> q <+> (r <+> s) = p <+> s <+> (q <+> r)
+    shuffle p q r s =
+      rewrite sym $ semigroupOpIsAssociative p q (r <+> s) in
+        rewrite abelianGroupOpIsCommutative r s in
+          rewrite semigroupOpIsAssociative q s r in
+          rewrite abelianGroupOpIsCommutative q s in
+        rewrite sym $ semigroupOpIsAssociative s q r in
+      semigroupOpIsAssociative p s (q <+> r)
+
+    regroup : (aa, xx, x1, x2, x3, x4, x5, x6, x7, x8 : t) ->
+      (aa <.> (x1 <.> x2) <+> xx <.> (x3 <.> x4) <+>
+        (aa <.> (x5 <.> x6) <+> xx <.> (x7 <.> x8)))
+      =
+      (aa <.> x1 <.> x2 <+> xx <.> x3 <.> x4 <+>
+        (aa <.> x5 <.> x6 <+> xx <.> x7 <.> x8))
+    regroup aa xx x1 x2 x3 x4 x5 x6 x7 x8 =
+      rewrite ringOpIsAssociative aa x1 x2 in
+        rewrite ringOpIsAssociative aa x5 x6 in
+      rewrite ringOpIsAssociative xx x3 x4 in
+        rewrite ringOpIsAssociative xx x7 x8 in
+      Refl
+
+RingWithUnity t => RingWithUnity (Complex t) where
   unity = (unity :+ neutral)
 
+  ringWithUnityIsUnityL {t} (a :+ x) =
+    rewrite ringWithUnityIsUnityL a in
+      rewrite ringWithUnityIsUnityL x in
+    rewrite multNeutralAbsorbingR a in
+      rewrite multNeutralAbsorbingR x in
+    rewrite inverseNeutralIsNeutral {t=t} in
+      rewrite monoidNeutralIsNeutralL a in
+        rewrite monoidNeutralIsNeutralR x in
+    Refl
+
+  ringWithUnityIsUnityR (a :+ x) =
+    rewrite ringWithUnityIsUnityR a in
+      rewrite ringWithUnityIsUnityR x in
+    rewrite multNeutralAbsorbingL a in
+      rewrite multNeutralAbsorbingL x in
+    rewrite inverseNeutralIsNeutral {t=t} in
+      rewrite monoidNeutralIsNeutralL a in
+        rewrite monoidNeutralIsNeutralL x in
+    Refl
+
 RingWithUnity a => Module a (Complex a) where
   (<#>) x = map (x <.>)
 
diff --git a/libs/contrib/Data/Bool/Algebra.idr b/libs/contrib/Data/Bool/Algebra.idr
index 069b2e7da7..f9471f7203 100644
--- a/libs/contrib/Data/Bool/Algebra.idr
+++ b/libs/contrib/Data/Bool/Algebra.idr
@@ -1,7 +1,6 @@
 module Data.Bool.Algebra
 
 import Control.Algebra
-import Interfaces.Verified
 
 %access public export
 %default total
@@ -17,10 +16,9 @@ xor True True = False
 xor False False = False
 xor _ _ = True
 
-[PlusBoolSemi] Semigroup Bool where
+Semigroup Bool where
   (<+>) = xor
 
-[PlusBoolSemiV] VerifiedSemigroup Bool using PlusBoolSemi where
   semigroupOpIsAssociative True True True = Refl
   semigroupOpIsAssociative True True False = Refl
   semigroupOpIsAssociative True False True = Refl
@@ -30,36 +28,32 @@ xor _ _ = True
   semigroupOpIsAssociative False True False = Refl
   semigroupOpIsAssociative False False False = Refl
 
-[PlusBoolMonoid] Monoid Bool using PlusBoolSemi where
+Monoid Bool where
   neutral = False
 
-[PlusBoolMonoidV] VerifiedMonoid Bool using PlusBoolSemiV, PlusBoolMonoid where
   monoidNeutralIsNeutralL True = Refl
   monoidNeutralIsNeutralL False = Refl
 
   monoidNeutralIsNeutralR True = Refl
   monoidNeutralIsNeutralR False = Refl
 
-[PlusBoolGroup] Group Bool using PlusBoolMonoid where
+Group Bool where
   -- Each Bool is its own additive inverse.
   inverse = id
 
-[PlusBoolGroupV] VerifiedGroup Bool using PlusBoolMonoidV, PlusBoolGroup where
   groupInverseIsInverseR True = Refl
   groupInverseIsInverseR False = Refl
 
-[PlusBoolAbel] AbelianGroup Bool using PlusBoolGroup where
+AbelianGroup Bool where
 
-[PlusBoolAbelV] VerifiedAbelianGroup Bool using PlusBoolGroupV, PlusBoolAbel where
   abelianGroupOpIsCommutative True True = Refl
   abelianGroupOpIsCommutative True False = Refl
   abelianGroupOpIsCommutative False True = Refl
   abelianGroupOpIsCommutative False False = Refl
 
-[RingBool] Ring Bool using PlusBoolAbel where
+Ring Bool where
   (<.>) = and
 
-[RingBoolV] VerifiedRing Bool using RingBool, PlusBoolAbelV where
   ringOpIsAssociative True True True = Refl
   ringOpIsAssociative True True False = Refl
   ringOpIsAssociative True False True = Refl
@@ -87,12 +81,24 @@ xor _ _ = True
   ringOpIsDistributiveR False True False = Refl
   ringOpIsDistributiveR False False False = Refl
 
-[RingUnBool] RingWithUnity Bool using RingBool where
+RingWithUnity Bool where
   unity = True
 
-VerifiedRingWithUnity Bool using RingUnBool, RingBoolV where
   ringWithUnityIsUnityL True = Refl
   ringWithUnityIsUnityL False = Refl
 
   ringWithUnityIsUnityR True = Refl
   ringWithUnityIsUnityR False = Refl
+
+CommutativeRing Bool where
+  ringOpIsCommutative True True = Refl
+  ringOpIsCommutative True False = Refl
+  ringOpIsCommutative False True = Refl
+  ringOpIsCommutative False False = Refl
+
+Field Bool where
+  -- True is the only "nonzero" element
+  inverseM x _ = x
+
+  fieldInverseIsInverseR False p = void $ p Refl
+  fieldInverseIsInverseR True _ = Refl
diff --git a/libs/contrib/Data/BoundedList.idr b/libs/contrib/Data/BoundedList.idr
index 0be89a830e..46b12c4b7f 100644
--- a/libs/contrib/Data/BoundedList.idr
+++ b/libs/contrib/Data/BoundedList.idr
@@ -100,11 +100,28 @@ implementation Semigroup a => Semigroup (BoundedList n a) where
   xs <+> [] = xs
   [] <+> ys = ys
 
+  semigroupOpIsAssociative [] [] [] = Refl
+  semigroupOpIsAssociative [] [] (_ :: _) = Refl
+  semigroupOpIsAssociative [] (_ :: _) [] = Refl
+  semigroupOpIsAssociative [] (_ :: _) (_ :: _) = Refl
+  semigroupOpIsAssociative (_ :: _) [] [] = Refl
+  semigroupOpIsAssociative (_ :: _) [] (_ :: _) = Refl
+  semigroupOpIsAssociative (_ :: _) (_ :: _) [] = Refl
+  semigroupOpIsAssociative (x :: xs) (y :: ys) (z :: zs) =
+    rewrite semigroupOpIsAssociative x y z in
+      rewrite semigroupOpIsAssociative xs ys zs in
+        Refl
+
 -- The Semigroup constraint is only needed because that's how we make a
 -- semigroup from BoundedList, not used in this implementation.
 implementation Semigroup a => Monoid (BoundedList n a) where
   neutral = []
 
+  monoidNeutralIsNeutralL [] = Refl
+  monoidNeutralIsNeutralL (_ :: _) = Refl
+  monoidNeutralIsNeutralR [] = Refl
+  monoidNeutralIsNeutralR (_ :: _) = Refl
+
 --------------------------------------------------------------------------------
 -- Misc
 --------------------------------------------------------------------------------
diff --git a/libs/contrib/Data/CoList.idr b/libs/contrib/Data/CoList.idr
index 0748e8b10f..495997aa7f 100644
--- a/libs/contrib/Data/CoList.idr
+++ b/libs/contrib/Data/CoList.idr
@@ -1,5 +1,7 @@
 module Data.CoList
 
+import Control.Algebra
+
 %access public export
 %default total
 
@@ -13,12 +15,33 @@ codata CoList : Type -> Type where
 (++) []      right = right
 (++) (x::xs) right = x :: (xs ++ right)
 
+-- Postulates --------------------------
+
+-- These are required for implementing verified interfaces.
+-- TODO : Prove them.
+
+postulate private
+colist_assoc : (l, c, r : CoList a) -> l ++ c ++ r = (l ++ c) ++ r
+
+postulate private
+colist_neutl : (l : CoList a) -> l ++ [] = l
+
+postulate private
+colist_neutr : (r : CoList a) -> [] ++ r = r
+
+----------------------------------------
+
 implementation Semigroup (CoList a) where
   (<+>) = (++)
 
+  semigroupOpIsAssociative = colist_assoc
+
 implementation Monoid (CoList a) where
   neutral = []
 
+  monoidNeutralIsNeutralL = colist_neutl
+  monoidNeutralIsNeutralR = colist_neutr
+
 implementation Functor CoList where
   map f []      = []
   map f (x::xs) = f x :: map f xs
diff --git a/libs/contrib/Data/Heap.idr b/libs/contrib/Data/Heap.idr
index 32576833cc..2a944afdf7 100644
--- a/libs/contrib/Data/Heap.idr
+++ b/libs/contrib/Data/Heap.idr
@@ -5,6 +5,7 @@
 
 module Data.Heap
 
+import Control.Algebra.Lattice
 
 %default total
 %access export
@@ -122,12 +123,27 @@ implementation Eq a => Eq (MaxiphobicHeap a) where
     ls == rs && ll == rl && le == re && lr == rr
   _                  == _                  = False
 
-implementation Ord a => Semigroup (MaxiphobicHeap a) where
+-- This is required for implementing verified semigroup.
+-- TODO : Prove it!
+postulate private
+maxiphobicheap_assoc : Ord a => (l, c, r : MaxiphobicHeap a) ->
+  merge l (merge c r) = merge (merge l c) r
+
+Ord a => Semigroup (MaxiphobicHeap a) where
   (<+>) = merge
 
-implementation Ord a => Monoid (MaxiphobicHeap a) where
+  semigroupOpIsAssociative = maxiphobicheap_assoc
+
+Ord a => Monoid (MaxiphobicHeap a) where
   neutral = empty
 
+  monoidNeutralIsNeutralL Empty = Refl
+  monoidNeutralIsNeutralL (Node _ _ _ _) = Refl
+  monoidNeutralIsNeutralR _ = Refl
+
+-- Ord a => JoinSemilattice (MaxiphobicHeap a) where
+--   join = merge
+
 --------------------------------------------------------------------------------
 -- Properties
 --------------------------------------------------------------------------------
diff --git a/libs/contrib/Data/Matrix/Algebraic.idr b/libs/contrib/Data/Matrix/Algebraic.idr
index 10a28f90bf..2322436525 100644
--- a/libs/contrib/Data/Matrix/Algebraic.idr
+++ b/libs/contrib/Data/Matrix/Algebraic.idr
@@ -5,7 +5,6 @@ module Data.Matrix.Algebraic
 
 import public Control.Algebra
 import public Control.Algebra.VectorSpace
-import public Control.Algebra.NumericImplementations
 
 import public Data.Matrix
 
@@ -26,27 +25,85 @@ infixr 7 <&>  -- matrix tensor product
 --               Vectors as members of algebraic interfaces
 -----------------------------------------------------------------------
 
-implementation Semigroup a => Semigroup (Vect n a) where
+-- TODO: Prove properties of matrix algebra for verified algebraic interfaces
+
+Semigroup a => Semigroup (Vect n a) where
   (<+>)= zipWith (<+>)
 
-implementation Monoid a => Monoid (Vect n a) where
+  semigroupOpIsAssociative [] [] [] = Refl
+  semigroupOpIsAssociative (x :: xs) (y :: ys) (z :: zs) =
+    rewrite semigroupOpIsAssociative x y z in
+      rewrite semigroupOpIsAssociative xs ys zs in
+        Refl
+
+Monoid a => Monoid (Vect n a) where
   neutral {n} = replicate n neutral
 
-implementation Group a => Group (Vect n a) where
+  monoidNeutralIsNeutralL [] = Refl
+  monoidNeutralIsNeutralL (x :: xs) =
+    rewrite monoidNeutralIsNeutralL x in
+      rewrite monoidNeutralIsNeutralL xs in
+        Refl
+
+  monoidNeutralIsNeutralR [] = Refl
+  monoidNeutralIsNeutralR (x :: xs) =
+    rewrite monoidNeutralIsNeutralR x in
+      rewrite monoidNeutralIsNeutralR xs in
+        Refl
+
+Group a => Group (Vect n a) where
   inverse = map inverse
 
-implementation AbelianGroup a => AbelianGroup (Vect n a) where {}
+  groupInverseIsInverseR [] = Refl
+  groupInverseIsInverseR (x :: xs) =
+    rewrite groupInverseIsInverseR x in
+      rewrite groupInverseIsInverseR xs in
+        Refl
+
+AbelianGroup a => AbelianGroup (Vect n a) where
+  abelianGroupOpIsCommutative [] [] = Refl
+  abelianGroupOpIsCommutative (x :: xs) (y :: ys) =
+    rewrite abelianGroupOpIsCommutative x y in
+      rewrite abelianGroupOpIsCommutative xs ys in
+        Refl
 
-implementation Ring a => Ring (Vect n a) where
+Ring a => Ring (Vect n a) where
   (<.>) = zipWith (<.>)
 
-implementation RingWithUnity a => RingWithUnity (Vect n a) where
+  ringOpIsAssociative [] [] [] = Refl
+  ringOpIsAssociative (x :: xs) (y :: ys) (z :: zs) =
+    rewrite ringOpIsAssociative x y z in
+      rewrite ringOpIsAssociative xs ys zs in
+        Refl
+  ringOpIsDistributiveL [] [] [] = Refl
+  ringOpIsDistributiveL (x :: xs) (y :: ys) (z :: zs) =
+    rewrite ringOpIsDistributiveL x y z in
+      rewrite ringOpIsDistributiveL xs ys zs in
+        Refl
+  ringOpIsDistributiveR [] [] [] = Refl
+  ringOpIsDistributiveR (x :: xs) (y :: ys) (z :: zs) =
+    rewrite ringOpIsDistributiveR x y z in
+      rewrite ringOpIsDistributiveR xs ys zs in
+        Refl
+
+RingWithUnity a => RingWithUnity (Vect n a) where
   unity {n} = replicate n unity
 
-implementation RingWithUnity a => Module a (Vect n a) where
+  ringWithUnityIsUnityR [] = Refl
+  ringWithUnityIsUnityR (x :: xs) =
+    rewrite ringWithUnityIsUnityR x in
+      rewrite ringWithUnityIsUnityR xs in
+        Refl
+  ringWithUnityIsUnityL [] = Refl
+  ringWithUnityIsUnityL (x :: xs) =
+    rewrite ringWithUnityIsUnityL x in
+      rewrite ringWithUnityIsUnityL xs in
+        Refl
+
+RingWithUnity a => Module a (Vect n a) where
   (<#>) r = map (r <.>)
 
-implementation RingWithUnity a => Module a (Vect n (Vect l a)) where
+RingWithUnity a => Module a (Vect n (Vect l a)) where
   (<#>) r = map (r <#>)
 -- should be Module a b => Module a (Vect n b), but results in 'overlapping implementation'
 
@@ -141,9 +198,3 @@ det {n} m = case n of
   Z     => det2 m
   (S k) => altSum . map (\c => indices FZ c m <.> det (subMatrix FZ c m))
          $ fins (S (S (S k)))
-
------------------------------------------------------------------------
---                      Matrix Algebra Properties
------------------------------------------------------------------------
-
--- TODO: Prove properties of matrix algebra for 'Verified' algebraic interfaces
diff --git a/libs/contrib/Data/Monoid.idr b/libs/contrib/Data/Monoid.idr
index f3ee5224c0..6da17e39b1 100644
--- a/libs/contrib/Data/Monoid.idr
+++ b/libs/contrib/Data/Monoid.idr
@@ -11,11 +11,30 @@ module Data.Monoid
 Semigroup () where
   (<+>) _ _ = ()
 
+  semigroupOpIsAssociative _ _ _ = Refl
+
 Monoid () where
   neutral = ()
 
+  monoidNeutralIsNeutralL () = Refl
+  monoidNeutralIsNeutralR () = Refl
+
 (Semigroup m, Semigroup n) => Semigroup (m, n) where
   (a, b) <+> (c, d) = (a <+> c, b <+> d)
 
+  semigroupOpIsAssociative (a, x) (b, y) (c, z) =
+    rewrite semigroupOpIsAssociative a b c in
+      rewrite semigroupOpIsAssociative x y z in
+        Refl
+
 (Monoid m, Monoid n) => Monoid (m, n) where
   neutral = (neutral, neutral)
+
+  monoidNeutralIsNeutralL (a, b) =
+    rewrite monoidNeutralIsNeutralL a in
+      rewrite monoidNeutralIsNeutralL b in
+        Refl
+  monoidNeutralIsNeutralR (a, b) =
+    rewrite monoidNeutralIsNeutralR a in
+      rewrite monoidNeutralIsNeutralR b in
+        Refl
diff --git a/libs/contrib/Data/PosNat.idr b/libs/contrib/Data/PosNat.idr
index d59d8a5dbf..88a16dea03 100644
--- a/libs/contrib/Data/PosNat.idr
+++ b/libs/contrib/Data/PosNat.idr
@@ -43,14 +43,32 @@ succ (n ** _) = (S n ** ItIsSucc)
 Semigroup PosNat where
   (<+>) = plusPosNat
 
+  semigroupOpIsAssociative (S a ** _) (S b ** _) (S c ** _) =
+    cong {f = \q => (S q ** ItIsSucc)} $
+      plusAssociative a (S b) (S c)
+
+-- I must be missing something obvious here, because it doesn't seem
+-- like it should be hard to prove this. TODO
+
+postulate private
+posnat_semigroupOpIsAssociative : (l, c, r : PosNat) ->
+  multPosNat l (multPosNat c r) = multPosNat (multPosNat l c) r
+
 ||| Semigroup using multiplication
 [MultPosNatSemi] Semigroup PosNat where
   (<+>) = multPosNat
 
+  semigroupOpIsAssociative = posnat_semigroupOpIsAssociative
+
 ||| Monoid, neutral = 1
 [MultPosNatMonoid] Monoid PosNat using MultPosNatSemi where
   neutral = one
 
+  monoidNeutralIsNeutralL (S k ** ItIsSucc) =
+    rewrite multOneRightNeutral k in Refl
+  monoidNeutralIsNeutralR (S k ** ItIsSucc) =
+    rewrite multOneLeftNeutral k in Refl
+
 ||| Convert a Nat to a PosNat, using automatic proof search
 p : (n : Nat) -> {auto ok : IsSucc n} -> PosNat
 p Z {ok} impossible
diff --git a/libs/contrib/Data/SortedBag.idr b/libs/contrib/Data/SortedBag.idr
index e5e1e41db1..87b1009367 100644
--- a/libs/contrib/Data/SortedBag.idr
+++ b/libs/contrib/Data/SortedBag.idr
@@ -6,6 +6,7 @@ import Data.Chain
 import Data.Combinators
 import Data.PosNat
 import Data.SortedMap
+import Control.Algebra
 
 %default total
 %access export
@@ -120,8 +121,13 @@ Foldable SortedBag where
 union : EndoChain 2 (SortedBag k)
 union = onMaps {n=2} merge
 
-Semigroup (SortedBag a) where
-  (<+>) = union
+-- Semigroup (SortedBag a) where
+--   (<+>) = union
 
-Ord a => Monoid (SortedBag a) where
-  neutral = empty
+--   semigroupOpIsAssociative l c r = ???
+
+-- Ord a => Monoid (SortedBag a) where
+--   neutral = empty
+
+--   monoidNeutralIsNeutralL l = ???
+--   monoidNeutralIsNeutralR r = ???
diff --git a/libs/contrib/Data/SortedMap.idr b/libs/contrib/Data/SortedMap.idr
index 3d3af28461..48e74a61ab 100644
--- a/libs/contrib/Data/SortedMap.idr
+++ b/libs/contrib/Data/SortedMap.idr
@@ -1,5 +1,7 @@
 module Data.SortedMap
 
+import Control.Algebra
+
 -- TODO: write split
 
 private
@@ -300,12 +302,18 @@ export
 -- strictly more powerful I believe, because `mergeLeft` can be emulated with
 -- the `First` monoid. However, this does require more code to do the same
 -- thing.
-export
-Semigroup v => Semigroup (SortedMap k v) where
-  (<+>) = merge
 
-||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
-||| However, semantically, it should be equal.
-export
-(Ord k, Semigroup v) => Monoid (SortedMap k v) where
-  neutral = empty
+-- export
+-- Semigroup v => Semigroup (SortedMap k v) where
+--   (<+>) = merge
+
+--   semigroupOpIsAssociative l c r = ???
+
+-- ||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
+-- ||| However, semantically, it should be equal.
+-- export
+-- (Ord k, Semigroup v) => Monoid (SortedMap k v) where
+--   neutral = empty
+
+--   monoidNeutralIsNeutralL l = Refl
+--   monoidNeutralIsNeutralR r = ???
diff --git a/libs/contrib/Data/SortedSet.idr b/libs/contrib/Data/SortedSet.idr
index b952e8c2c3..e7af8b5318 100644
--- a/libs/contrib/Data/SortedSet.idr
+++ b/libs/contrib/Data/SortedSet.idr
@@ -1,6 +1,7 @@
 module Data.SortedSet
 
 import Data.SortedMap
+import Control.Algebra
 
 export
 data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())
@@ -53,13 +54,18 @@ export
 intersection : (x, y : SortedSet k) -> SortedSet k
 intersection x y = difference x (difference x y)
 
-export
-Ord k => Semigroup (SortedSet k) where
-  (<+>) = union
+-- export
+-- Ord k => Semigroup (SortedSet k) where
+--   (<+>) = union
 
-export
-Ord k => Monoid (SortedSet k) where
-  neutral = empty
+--   semigroupOpIsAssociative l c r = ???
+
+-- export
+-- Ord k => Monoid (SortedSet k) where
+--   neutral = empty
+
+--   monoidNeutralIsNeutralL l = ???
+--   monoidNeutralIsNeutralR r = ???
 
 export
 keySet : SortedMap k v -> SortedSet k
diff --git a/libs/contrib/Interfaces/Verified.idr b/libs/contrib/Interfaces/Verified.idr
index f7abf35337..b11ca0b494 100644
--- a/libs/contrib/Interfaces/Verified.idr
+++ b/libs/contrib/Interfaces/Verified.idr
@@ -1,12 +1,6 @@
 module Interfaces.Verified
 
-import Control.Algebra
-import Control.Algebra.Lattice
-import Control.Algebra.NumericImplementations
-import Control.Algebra.VectorSpace
 import Data.Vect
-import Data.ZZ
-import Data.Bool.Extra
 
 %default total
 %access public export
@@ -18,6 +12,8 @@ import Data.Bool.Extra
 -- prelude, in the cases of Functor, Applicative, Monad, Semigroup,
 -- and Monoid).
 
+-- Functor -----------------------------
+
 interface Functor f => VerifiedFunctor (f : Type -> Type) where
   functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) -> (x : f a) -> map g x = x
   functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
@@ -55,6 +51,8 @@ VerifiedFunctor (Vect n) where
   functorComposition [] _ _ = Refl
   functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
 
+-- Applicative -------------------------
+
 interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
   applicativeMap : (x : f a) -> (g : a -> b) ->
                    map g x = pure g <*> x
@@ -167,6 +165,8 @@ VerifiedApplicative Maybe where
   applicativeInterchange x Nothing = Refl
   applicativeInterchange x (Just y) = Refl
 
+-- Monad -------------------------------
+
 interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
   monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
                      mf <*> mx = mf >>= \f =>
@@ -215,6 +215,8 @@ VerifiedMonad List where
       (foldrConcatEq' (g1 x) (foldr (\x1, meth => g1 x1 ++ meth) [] xs) g2)
       (cong $ monadAssociativity xs g1 g2)
 
+-- Alternative -------------------------
+
 interface (Alternative f, VerifiedApplicative f) => VerifiedAlternative (f : Type -> Type) where
   alternativeLeftIdentity : (x : f a) -> Applicative.empty <|> x = x
   alternativeRightIdentity : (x : f a) -> x <|> Applicative.empty = x
@@ -232,123 +234,3 @@ VerifiedAlternative List where
   alternativeLeftIdentity _ = Refl
   alternativeRightIdentity = appendNilRightNeutral
   alternativeAssociativity = appendAssociative
-
-interface Semigroup a => VerifiedSemigroup a where
-  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
-
-implementation VerifiedSemigroup (List a) where
-  semigroupOpIsAssociative = appendAssociative
-
-[PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where
-  semigroupOpIsAssociative = plusAssociative
-
-[MultNatSemiV] VerifiedSemigroup Nat using MultNatSemi where
-  semigroupOpIsAssociative = multAssociative
-
-[PlusZZSemiV] VerifiedSemigroup ZZ using PlusZZSemi where
-  semigroupOpIsAssociative = plusAssociativeZ
-
-[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
-  semigroupOpIsAssociative = multAssociativeZ
-
-interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
-  monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
-  monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
-
-[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
-   monoidNeutralIsNeutralL = plusZeroRightNeutral
-   monoidNeutralIsNeutralR = plusZeroLeftNeutral
-
-[MultNatMonoidV] VerifiedMonoid Nat using MultNatSemiV, MultNatMonoid where
-  monoidNeutralIsNeutralL = multOneRightNeutral
-  monoidNeutralIsNeutralR = multOneLeftNeutral
-
-[PlusZZMonoidV] VerifiedMonoid ZZ using PlusZZSemiV, PlusZZMonoid where
-   monoidNeutralIsNeutralL = plusZeroRightNeutralZ
-   monoidNeutralIsNeutralR = plusZeroLeftNeutralZ
-
-[MultZZMonoidV] VerifiedMonoid ZZ using MultZZSemiV, MultZZMonoid where
-  monoidNeutralIsNeutralL = multOneRightNeutralZ
-  monoidNeutralIsNeutralR = multOneLeftNeutralZ
-
-implementation VerifiedMonoid (List a) where
-  monoidNeutralIsNeutralL = appendNilRightNeutral
-  monoidNeutralIsNeutralR xs = Refl
-
-interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
-  groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
-
-VerifiedGroup ZZ using PlusZZMonoidV where
-  groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in
-                             rewrite multNegLeftZ 0 k in
-                             rewrite multOneLeftNeutralZ k in
-                             plusNegateInverseRZ k
-
-interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
-  abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
-
-VerifiedAbelianGroup ZZ where
-  abelianGroupOpIsCommutative = plusCommutativeZ
-
-interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
-  ringOpIsAssociative   : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
-  ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
-  ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
-
-VerifiedRing ZZ where
-  ringOpIsAssociative = multAssociativeZ
-  ringOpIsDistributiveL = multDistributesOverPlusRightZ
-  ringOpIsDistributiveR = multDistributesOverPlusLeftZ
-
-interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
-  ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
-  ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
-
-VerifiedRingWithUnity ZZ where
-  ringWithUnityIsUnityL = multOneRightNeutralZ
-  ringWithUnityIsUnityR = multOneLeftNeutralZ
-
-interface JoinSemilattice a => VerifiedJoinSemilattice a where
-  joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
-  joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l
-  joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e
-
-VerifiedJoinSemilattice Nat where
-  joinSemilatticeJoinIsAssociative = maximumAssociative
-  joinSemilatticeJoinIsCommutative = maximumCommutative
-  joinSemilatticeJoinIsIdempotent  = maximumIdempotent
-
-VerifiedJoinSemilattice Bool where
-  joinSemilatticeJoinIsAssociative = orAssociative
-  joinSemilatticeJoinIsCommutative = orCommutative
-  joinSemilatticeJoinIsIdempotent = orSameNeutral
-
-interface MeetSemilattice a => VerifiedMeetSemilattice a where
-  meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
-  meetSemilatticeMeetIsCommutative : (l, r : a)    -> meet l r = meet r l
-  meetSemilatticeMeetIsIdempotent  : (e : a)       -> meet e e = e
-
-VerifiedMeetSemilattice Nat where
-  meetSemilatticeMeetIsAssociative = minimumAssociative
-  meetSemilatticeMeetIsCommutative = minimumCommutative
-  meetSemilatticeMeetIsIdempotent  = minimumIdempotent
-
-VerifiedMeetSemilattice Bool where
-  meetSemilatticeMeetIsAssociative = andAssociative
-  meetSemilatticeMeetIsCommutative = andCommutative
-  meetSemilatticeMeetIsIdempotent = andSameNeutral
-
-interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
-  joinBottomIsIdentity : (x : a) -> join x Lattice.bottom = x
-
-VerifiedBoundedJoinSemilattice Nat where
-  joinBottomIsIdentity = maximumZeroNLeft
-
-VerifiedBoundedJoinSemilattice Bool where
-  joinBottomIsIdentity = orFalseNeutral
-
-interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
-  meetTopIsIdentity : (x : a) -> meet x Lattice.top = x
-
-VerifiedBoundedMeetSemilattice Bool where
-  meetTopIsIdentity = andTrueNeutral
diff --git a/libs/contrib/Text/PrettyPrint/WL/Core.idr b/libs/contrib/Text/PrettyPrint/WL/Core.idr
index fab2c4e0e9..e5c3c64758 100644
--- a/libs/contrib/Text/PrettyPrint/WL/Core.idr
+++ b/libs/contrib/Text/PrettyPrint/WL/Core.idr
@@ -92,12 +92,20 @@ flatten other = other
 group : Doc -> Doc
 group x = Union (flatten x) x
 
+-- TODO : Prove these believe_me statements, or at least replace them
+--        with explicit postulates.
+
 Semigroup Doc where
   (<+>) x y = beside x y
 
+  semigroupOpIsAssociative x y z = believe_me Doc
+
 Monoid Doc where
   neutral = empty
 
+  monoidNeutralIsNeutralL l = believe_me Doc
+  monoidNeutralIsNeutralR r = believe_me Doc
+
 fold : (f : Doc -> Doc -> Doc) -> (ds : List Doc) -> Doc
 fold _ Nil     = empty
 fold f (x::xs) = foldl f x xs
diff --git a/libs/prelude/Prelude/Algebra.idr b/libs/prelude/Prelude/Algebra.idr
index c84220ffbf..8ec5a2fd13 100644
--- a/libs/prelude/Prelude/Algebra.idr
+++ b/libs/prelude/Prelude/Algebra.idr
@@ -18,6 +18,9 @@ infixl 6 <+>
 interface Semigroup ty where
   (<+>) : ty -> ty -> ty
 
+  semigroupOpIsAssociative : (l, c, r : ty) ->
+    l <+> (c <+> r) = (l <+> c) <+> r
+
 ||| Sets equipped with a single binary operation that is associative, along with
 ||| a neutral element for that binary operation.  Must satisfy the following
 ||| laws:
@@ -29,3 +32,6 @@ interface Semigroup ty where
 |||     forall a,     neutral <+> a   == a
 interface Semigroup ty => Monoid ty where
   neutral : ty
+
+  monoidNeutralIsNeutralL : (l : ty) -> l <+> Algebra.neutral = l
+  monoidNeutralIsNeutralR : (r : ty) -> Algebra.neutral <+> r = r
diff --git a/libs/prelude/Prelude/List.idr b/libs/prelude/Prelude/List.idr
index 06bdc0eafe..fba9bfbaca 100644
--- a/libs/prelude/Prelude/List.idr
+++ b/libs/prelude/Prelude/List.idr
@@ -272,12 +272,6 @@ Ord a => Ord (List a) where
     else
       compare xs ys
 
-Semigroup (List a) where
-  (<+>) = (++)
-
-Monoid (List a) where
-  neutral = []
-
 Functor List where
   map f []      = []
   map f (x::xs) = f x :: map f xs
@@ -417,14 +411,6 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
     intersperse' sep []      = []
     intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
 
-||| Given a separator list and some more lists, produce a new list by
-||| placing the separator between each of the lists.
-|||
-||| @ sep the separator
-||| @ xss the lists between which the separator will be placed
-intercalate : (sep : List a) -> (xss : List (List a)) -> List a
-intercalate sep xss = concat $ intersperse sep xss
-
 ||| Transposes rows and columns of a list of lists.
 |||
 ||| ```idris example
@@ -975,3 +961,24 @@ splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
                 in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)
   where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)
         aux Refl Refl = Refl
+
+-- Algebra -----------------------------
+
+Semigroup (List a) where
+  (<+>) = (++)
+
+  semigroupOpIsAssociative = appendAssociative
+
+Monoid (List a) where
+  neutral = []
+
+  monoidNeutralIsNeutralL = appendNilRightNeutral
+  monoidNeutralIsNeutralR xs = Refl
+
+||| Given a separator list and some more lists, produce a new list by
+||| placing the separator between each of the lists.
+|||
+||| @ sep the separator
+||| @ xss the lists between which the separator will be placed
+intercalate : (sep : List a) -> (xss : List (List a)) -> List a
+intercalate sep xss = concat $ intersperse sep xss
diff --git a/libs/prelude/Prelude/Maybe.idr b/libs/prelude/Prelude/Maybe.idr
index 7838bec9b2..18f77e7d56 100644
--- a/libs/prelude/Prelude/Maybe.idr
+++ b/libs/prelude/Prelude/Maybe.idr
@@ -115,6 +115,10 @@ Semigroup (Maybe a) where
   Nothing   <+> m = m
   (Just x)  <+> _ = Just x
 
+  semigroupOpIsAssociative (Just _) _ _ = Refl
+  semigroupOpIsAssociative Nothing (Just _) _ = Refl
+  semigroupOpIsAssociative Nothing Nothing _ = Refl
+
 ||| Transform any semigroup into a monoid by using `Nothing` as the
 ||| designated neutral element and collecting the contents of the
 ||| `Just` constructors using a semigroup structure on `a`. This is
@@ -124,9 +128,24 @@ Semigroup (Maybe a) where
   m         <+> Nothing = m
   (Just m1) <+> (Just m2) = Just (m1 <+> m2)
 
+  semigroupOpIsAssociative Nothing Nothing _ = Refl
+  semigroupOpIsAssociative Nothing (Just _) Nothing = Refl
+  semigroupOpIsAssociative Nothing (Just _) (Just _) = Refl
+  semigroupOpIsAssociative (Just x) Nothing Nothing = Refl
+  semigroupOpIsAssociative (Just x) Nothing (Just y) = Refl
+  semigroupOpIsAssociative (Just _) (Just _) Nothing = Refl
+  semigroupOpIsAssociative (Just x) (Just y) (Just z) =
+    rewrite semigroupOpIsAssociative x y z in Refl
+
 Monoid (Maybe a) where
   neutral = Nothing
 
+  monoidNeutralIsNeutralL Nothing = Refl
+  monoidNeutralIsNeutralL (Just _) = Refl
+
+  monoidNeutralIsNeutralR Nothing = Refl
+  monoidNeutralIsNeutralR (Just _) = Refl
+
 (Monoid a, Eq a) => Cast a (Maybe a) where
   cast = raiseToMaybe
 
diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr
index 26b6a36a39..1184f97262 100644
--- a/libs/prelude/Prelude/Nat.idr
+++ b/libs/prelude/Prelude/Nat.idr
@@ -260,48 +260,6 @@ Cast String Nat where
 Cast Nat String where
   cast n = cast (the Integer (cast n))
 
-||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (*)
-record Multiplicative where
-  constructor GetMultiplicative
-  _ : Nat
-
-||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (+)
-record Additive where
-  constructor GetAdditive
-  _ : Nat
-
-Semigroup Multiplicative where
-  (<+>) left right = GetMultiplicative $ left' * right'
-    where
-      left'  : Nat
-      left'  =
-       case left of
-          GetMultiplicative m => m
-
-      right' : Nat
-      right' =
-        case right of
-          GetMultiplicative m => m
-
-Semigroup Additive where
-  left <+> right = GetAdditive $ left' + right'
-    where
-      left'  : Nat
-      left'  =
-        case left of
-          GetAdditive m => m
-
-      right' : Nat
-      right' =
-        case right of
-          GetAdditive m => m
-
-Monoid Multiplicative where
-  neutral = GetMultiplicative $ S Z
-
-Monoid Additive where
-  neutral = GetAdditive Z
-
 ||| Casts negative `Ints` to 0.
 Cast Int Nat where
   cast i = fromInteger (cast i)
@@ -811,3 +769,64 @@ sucMinL (S l) = cong (sucMinL l)
 total sucMinR : (l : Nat) -> minimum l (S l) = l
 sucMinR Z = Refl
 sucMinR (S l) = cong (sucMinR l)
+
+-- Algebra -----------------------------
+
+||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (*)
+record Multiplicative where
+  constructor GetMultiplicative
+  _ : Nat
+
+||| A wrapper for Nat that specifies the semigroup and monoid implementations that use (+)
+record Additive where
+  constructor GetAdditive
+  _ : Nat
+
+Semigroup Multiplicative where
+  (<+>) left right = GetMultiplicative $ left' * right'
+    where
+      left'  : Nat
+      left'  =
+       case left of
+          GetMultiplicative m => m
+
+      right' : Nat
+      right' =
+        case right of
+          GetMultiplicative m => m
+
+  semigroupOpIsAssociative
+    (GetMultiplicative l) (GetMultiplicative c) (GetMultiplicative r) =
+      rewrite multAssociative l c r in Refl
+
+Semigroup Additive where
+  left <+> right = GetAdditive $ left' + right'
+    where
+      left'  : Nat
+      left'  =
+        case left of
+          GetAdditive m => m
+
+      right' : Nat
+      right' =
+        case right of
+          GetAdditive m => m
+
+  semigroupOpIsAssociative
+    (GetAdditive l) (GetAdditive c) (GetAdditive r) =
+      rewrite plusAssociative l c r in Refl
+
+Monoid Multiplicative where
+  neutral = GetMultiplicative $ S Z
+
+  monoidNeutralIsNeutralL (GetMultiplicative l) =
+    rewrite multOneRightNeutral l in Refl
+  monoidNeutralIsNeutralR (GetMultiplicative r) =
+    rewrite plusZeroRightNeutral r in Refl
+
+Monoid Additive where
+  neutral = GetAdditive Z
+
+  monoidNeutralIsNeutralL (GetAdditive l) =
+    rewrite plusZeroRightNeutral l in Refl
+  monoidNeutralIsNeutralR (GetAdditive r) = Refl
diff --git a/libs/prelude/Prelude/Strings.idr b/libs/prelude/Prelude/Strings.idr
index 33a6ecb58f..e99d7228b0 100644
--- a/libs/prelude/Prelude/Strings.idr
+++ b/libs/prelude/Prelude/Strings.idr
@@ -209,9 +209,14 @@ Cast Char String where
 Semigroup String where
   (<+>) = (++)
 
+  semigroupOpIsAssociative = believe_me String
+
 Monoid String where
   neutral = ""
 
+  monoidNeutralIsNeutralL = believe_me String
+  monoidNeutralIsNeutralR = believe_me String
+
 ||| Splits the string into a part before the predicate
 ||| returns False and the rest of the string.
 |||
diff --git a/test/interfaces004/interfaces004.idr b/test/interfaces004/interfaces004.idr
index 0b5b887a8e..8e7839e3b2 100644
--- a/test/interfaces004/interfaces004.idr
+++ b/test/interfaces004/interfaces004.idr
@@ -2,15 +2,25 @@
 [PlusNatSemi] Semigroup Nat where
   (<+>) x y = x + y
 
+  semigroupOpIsAssociative = plusAssociative
+
 [MultNatSemi] Semigroup Nat where
   (<+>) x y = x * y
 
+  semigroupOpIsAssociative = multAssociative
+
 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
   neutral = 0
 
+  monoidNeutralIsNeutralL = plusZeroRightNeutral
+  monoidNeutralIsNeutralR = plusZeroLeftNeutral
+
 [MultNatMonoid] Monoid Nat using MultNatSemi where
   neutral = 1
 
+  monoidNeutralIsNeutralL = multOneRightNeutral
+  monoidNeutralIsNeutralR = multOneLeftNeutral
+
 test : Monoid a => a -> a
 test x = x <+> x <+> neutral
 
@@ -29,7 +39,6 @@ using implementation PlusNatMonoid
   main : IO ()
   main = do printLn (test (the Nat 6))
             printLn (test @{MultNatMonoid} 6)
-            
+
             printLn (foo 3 4)
             printLn (foo' 3 4)
-