diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
index b95bc08a7e..2991772497 100644
--- a/libs/contrib/Control/Algebra.idr
+++ b/libs/contrib/Control/Algebra.idr
@@ -22,22 +22,6 @@ interface Monoid a => Group a where
 (<->) : Group a => a -> a -> a
 (<->) left right = left <+> (inverse right)
 
-||| 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. 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
-interface Group a => AbelianGroup a where { }
-
 ||| 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.  Must satisfy the following
@@ -58,7 +42,7 @@ interface Group a => AbelianGroup 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 AbelianGroup a => Ring a where
+interface Group a => Ring a where
   (<.>) : a -> a -> a
 
 ||| Sets equipped with two binary operations, one associative and commutative
@@ -145,3 +129,41 @@ mtimes (S k) x = stimes (S k) x
 --   Structures where "abs" make sense.
 --   Euclidean domains, etc.
 --   Where to put fromInteger and fromRational?
+
+-- "Verified" Interfaces -----------------
+
+interface Semigroup a => VerifiedSemigroup a where
+  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
+
+interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
+  monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
+  monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
+
+interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
+  groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
+
+||| 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. 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
+interface VerifiedGroup a => AbelianGroup a where
+  abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
+
+interface (AbelianGroup 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)
+
+interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
+  ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
+  ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
diff --git a/libs/contrib/Control/Algebra/ComplexImplementations.idr b/libs/contrib/Control/Algebra/ComplexImplementations.idr
new file mode 100644
index 0000000000..21b657c3c0
--- /dev/null
+++ b/libs/contrib/Control/Algebra/ComplexImplementations.idr
@@ -0,0 +1,68 @@
+module Control.Algebra.ComplexImplementations
+
+import Data.Complex
+import Control.Algebra
+import Control.Algebra.Laws
+import Control.Algebra.VectorSpace
+
+%access public export
+%default total
+
+Semigroup a => Semigroup (Complex a) where
+  (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
+
+Monoid a => Monoid (Complex a) where
+  neutral = (neutral :+ neutral)
+
+Group a => Group (Complex a) where
+  inverse (r :+ i) = (inverse r :+ inverse i)
+
+Ring a => Ring (Complex a) where
+  (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
+
+RingWithUnity a => RingWithUnity (Complex a) where
+  unity = (unity :+ neutral)
+
+RingWithUnity a => Module a (Complex a) where
+  (<#>) x = map (x <.>)
+
+RingWithUnity a => InnerProductSpace a (Complex a) where
+  (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z
+
+----------------------------------------
+
+VerifiedSemigroup a => VerifiedSemigroup (Complex a) where
+  semigroupOpIsAssociative (a :+ x) (b :+ y) (c :+ z) =
+    rewrite semigroupOpIsAssociative a b c in
+      rewrite semigroupOpIsAssociative x y z in
+        Refl
+
+VerifiedMonoid t => VerifiedMonoid (Complex t) where
+  monoidNeutralIsNeutralL (a :+ x) =
+    rewrite monoidNeutralIsNeutralL a in
+      rewrite monoidNeutralIsNeutralL x in
+        Refl
+
+  monoidNeutralIsNeutralR (a :+ x) =
+    rewrite monoidNeutralIsNeutralR a in
+      rewrite monoidNeutralIsNeutralR x in
+        Refl
+
+VerifiedGroup t => VerifiedGroup (Complex t) where
+  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
+
+-- An interface resolution bug seems to make this impossible to prove.
+
+-- https://github.com/idris-lang/Idris-dev/issues/4853
+-- https://github.com/idris-lang/Idris2/issues/72
+
+-- VerifiedRing t => VerifiedRing (Complex t) where
diff --git a/libs/contrib/Control/Algebra/CyclicGroup.idr b/libs/contrib/Control/Algebra/CyclicGroup.idr
new file mode 100644
index 0000000000..9858c225ad
--- /dev/null
+++ b/libs/contrib/Control/Algebra/CyclicGroup.idr
@@ -0,0 +1,63 @@
+import Control.Algebra
+
+import Data.ZZ
+
+%access public export
+%default total
+
+----------------------------------------
+
+-- The Verified constraints here are required
+-- to work around an interface resolution bug.
+
+-- https://github.com/idris-lang/Idris-dev/issues/4853
+-- https://github.com/idris-lang/Idris2/issues/72
+
+mtimes' : VerifiedMonoid a => (n : Nat) -> a -> a
+mtimes' Z x = neutral
+mtimes' (S k) x = x <+> mtimes' k x
+
+gtimes : VerifiedGroup a => (n : ZZ) -> a -> a
+gtimes (Pos k) x = mtimes' k x
+gtimes (NegS k) x = mtimes' (S k) (inverse x)
+
+----------------------------------------
+
+mtimesTimes : VerifiedMonoid a => (x : a) -> (n, m : Nat) ->
+  mtimes' (n + m) x = mtimes' n x <+> mtimes' m x
+mtimesTimes x Z m = sym $ monoidNeutralIsNeutralR $ mtimes' m x
+mtimesTimes x (S k) m =
+  rewrite mtimesTimes x k m in
+    semigroupOpIsAssociative x (mtimes' k x) (mtimes' m x)
+
+-- TODO: prove this. It's definitely true in spirit, and I'm pretty
+-- sure the implementation of gtimes is correct, but working with ZZ
+-- is not easy.
+postulate
+gtimesTimes : VerifiedGroup a => (x : a) -> (n, m : ZZ) ->
+  gtimes (n + m) x = gtimes n x <+> gtimes m x
+
+gtimesCommutes : VerifiedGroup a => (x : a) -> (n, m : ZZ) ->
+  gtimes n x <+> gtimes m x = gtimes m x <+> gtimes n x
+gtimesCommutes x n m =
+  rewrite sym $ gtimesTimes x n m in
+    rewrite plusCommutativeZ n m in
+      gtimesTimes x m n
+
+||| A cyclic group is a group in which every element can be gotten by
+||| repeatedly adding or subtracting a particular element known as the
+||| generator.
+interface VerifiedGroup a => CyclicGroup a where
+  generator : (g : a ** (x : a) -> (n : ZZ ** x = gtimes n g))
+
+||| Every cyclic group is commutative.
+CyclicGroup a => AbelianGroup a where
+  abelianGroupOpIsCommutative {a} l r =
+    let
+      (g ** gen) = generator {a=a}
+      (n ** gl) = gen l
+      (m ** gr) = gen r
+        in
+    rewrite gl in
+      rewrite gr in
+        gtimesCommutes g n m
diff --git a/libs/contrib/Control/Algebra/GroupHomomorphism.idr b/libs/contrib/Control/Algebra/GroupHomomorphism.idr
new file mode 100644
index 0000000000..e22ba57358
--- /dev/null
+++ b/libs/contrib/Control/Algebra/GroupHomomorphism.idr
@@ -0,0 +1,30 @@
+import Prelude.Algebra as A
+import Control.Algebra
+import Control.Algebra.Laws
+
+%access public export
+
+||| A homomorphism is a mapping that preserves group structure.
+interface (VerifiedGroup a, VerifiedGroup b) => GroupHomomorphism a b where
+  to : a -> b
+  toGroup : (x, y : a) ->
+    to (x <+> y) = (to x) <+> (to y)
+
+||| Homomorphism preserves neutral.
+homoNeutral : GroupHomomorphism a b =>
+  to (the a A.neutral) = the b A.neutral
+homoNeutral {a} =
+  let ae = the a A.neutral in
+    selfSquareId (to ae) $
+      trans (sym $ toGroup ae ae) $
+        cong {f = to} $ monoidNeutralIsNeutralL ae
+
+||| Homomorphism preserves inverses.
+homoInverse : GroupHomomorphism a b => (x : a) ->
+  the b (to $ inverse x) = the b (inverse $ to x)
+homoInverse {a} {b} x =
+  cancelRight (to x) (to $ inverse x) (inverse $ to x) $
+    trans (sym $ toGroup (inverse x) x) $
+      trans (cong {f = to} $ groupInverseIsInverseR x) $
+        trans (homoNeutral {a=a} {b=b}) $
+          sym $ groupInverseIsInverseR (to x)
diff --git a/libs/contrib/Control/Algebra/Laws.idr b/libs/contrib/Control/Algebra/Laws.idr
index 46e9356e82..54cd23a60b 100644
--- a/libs/contrib/Control/Algebra/Laws.idr
+++ b/libs/contrib/Control/Algebra/Laws.idr
@@ -2,9 +2,9 @@ module Control.Algebra.Laws
 
 import Prelude.Algebra as A
 import Control.Algebra as Alg
-import Interfaces.Verified
 
-%access export
+%access public export
+%default total
 
 -- Monoids
 
@@ -143,6 +143,20 @@ cancelRight x y z p =
     rewrite groupInverseIsInverseL x in
   monoidNeutralIsNeutralL z
 
+||| ab = 0 -> a = b^-1
+neutralProductInverseR : VerifiedGroup ty => (a, b : ty) ->
+  a <+> b = A.neutral -> a = inverse b
+neutralProductInverseR a b prf =
+  cancelRight  b a (inverse b) $
+    trans prf $ sym $ groupInverseIsInverseR b
+
+||| ab = 0 -> a^-1 = b
+neutralProductInverseL : VerifiedGroup ty => (a, b : ty) ->
+  a <+> b = A.neutral -> inverse a = b
+neutralProductInverseL a b prf =
+  cancelLeft a (inverse a) b $
+    trans (groupInverseIsInverseL a) $ sym prf
+
 ||| For any a and b, ax = b and ya = b have solutions.
 latinSquareProperty : VerifiedGroup t => (a, b : t) ->
   ((x : t ** a <+> x = b),
@@ -169,7 +183,7 @@ uniqueSolutionL : VerifiedGroup t => (a, b, x, y : t) ->
 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
diff --git a/libs/contrib/Control/Algebra/NumericImplementations.idr b/libs/contrib/Control/Algebra/NumericImplementations.idr
index 12294cb910..23ea4502d9 100644
--- a/libs/contrib/Control/Algebra/NumericImplementations.idr
+++ b/libs/contrib/Control/Algebra/NumericImplementations.idr
@@ -3,8 +3,6 @@
 module Control.Algebra.NumericImplementations
 
 import Control.Algebra
-import Control.Algebra.VectorSpace
-import Data.Complex
 import Data.ZZ
 
 %access public export
@@ -20,8 +18,6 @@ Monoid Integer where
 Group Integer where
   inverse = (* -1)
 
-AbelianGroup Integer where
-
 Ring Integer where
   (<.>) = (*)
 
@@ -39,8 +35,6 @@ Monoid Int where
 Group Int where
   inverse = (* -1)
 
-AbelianGroup Int where
-
 Ring Int where
   (<.>) = (*)
 
@@ -58,8 +52,6 @@ Monoid Double where
 Group Double where
   inverse = (* -1)
 
-AbelianGroup Double where
-
 Ring Double where
   (<.>) = (*)
 
@@ -94,8 +86,6 @@ Field Double where
 Group ZZ using PlusZZMonoid where
   inverse = (* -1)
 
-AbelianGroup ZZ where
-
 [MultZZSemi] Semigroup ZZ where
   (<+>) = (*)
 
@@ -107,28 +97,3 @@ Ring ZZ where
 
 RingWithUnity ZZ where
   unity = 1
-
--- Complex
-
-Semigroup a => Semigroup (Complex a) where
-  (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
-
-Monoid a => Monoid (Complex a) where
-  neutral = (neutral :+ neutral)
-
-Group a => Group (Complex a) where
-  inverse (r :+ i) = (inverse r :+ inverse i)
-
-Ring a => AbelianGroup (Complex a) where {}
-
-Ring a => Ring (Complex a) where
-  (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
-
-RingWithUnity a => RingWithUnity (Complex a) where
-  unity = (unity :+ neutral)
-
-RingWithUnity a => Module a (Complex a) where
-  (<#>) x = map (x <.>)
-
-RingWithUnity a => InnerProductSpace a (Complex a) where
-  (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z
diff --git a/libs/contrib/Control/Algebra/VectorSpace.idr b/libs/contrib/Control/Algebra/VectorSpace.idr
index 1ae597adc8..aa80a9c3b8 100644
--- a/libs/contrib/Control/Algebra/VectorSpace.idr
+++ b/libs/contrib/Control/Algebra/VectorSpace.idr
@@ -20,7 +20,7 @@ infixr 2 <||>
 ||| + Distributivity of `<#>` and `<+>`:
 |||     forall a v w,  a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
 |||     forall a b v,  (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
-interface (RingWithUnity a, AbelianGroup b) => Module a b where
+interface RingWithUnity a => Module a b where
   (<#>) : a -> b -> b
 
 ||| A vector space is a module over a ring that is also a field
diff --git a/libs/contrib/Control/Algebra/VerifiedImplementations.idr b/libs/contrib/Control/Algebra/VerifiedImplementations.idr
new file mode 100644
index 0000000000..22d017039d
--- /dev/null
+++ b/libs/contrib/Control/Algebra/VerifiedImplementations.idr
@@ -0,0 +1,364 @@
+module Control.VerifiedInterfaces
+
+import Interfaces.Verified
+import Control.Algebra
+import Control.Algebra.CyclicGroup
+import Control.Algebra.Lattice
+import Control.Algebra.NumericImplementations
+import Data.Vect
+import Data.ZZ
+import Data.Sign
+import Data.Bool.Extra
+import Data.Morphisms
+import Control.Monad.Identity
+
+%default total
+%access public export
+
+-- Due to these being basically unused and difficult to implement,
+-- they're in contrib for a bit. Once a design is found that lets them
+-- be implemented for a number of implementations, and we get those
+-- implementations, then some of them can move back to base (or even
+-- prelude, in the cases of Functor, Applicative, Monad, Semigroup,
+-- and Monoid).
+
+-- Functor
+
+functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x
+functorIdentity' {f} = functorIdentity {f} id (\x => Refl)
+
+VerifiedFunctor (Pair a) where
+  functorIdentity g p (a,b) = rewrite p b in Refl
+  functorComposition (a,b) g1 g2 = Refl
+
+VerifiedFunctor (Either a) where
+  functorIdentity _ _ (Left _) = Refl
+  functorIdentity _ p (Right x) = cong (p x)
+  functorComposition (Left _) _ _ = Refl
+  functorComposition (Right _) _ _ = Refl
+
+VerifiedFunctor Maybe where
+  functorIdentity _ _ Nothing = Refl
+  functorIdentity g p (Just x) = rewrite p x in Refl
+  functorComposition Nothing g1 g2 = Refl
+  functorComposition (Just x) g1 g2 = Refl
+
+VerifiedFunctor List where
+  functorIdentity _ _ [] = Refl
+  functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
+  functorComposition [] _ _ = Refl
+  functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
+
+VerifiedFunctor (Vect n) where
+  functorIdentity _ _ [] = Refl
+  functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
+  functorComposition [] _ _ = Refl
+  functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
+
+-- Applicative
+
+VerifiedApplicative (Either a) where
+  applicativeMap (Left x) g = Refl
+  applicativeMap (Right x) g = Refl
+  applicativeIdentity (Left x) = Refl
+  applicativeIdentity (Right x) = Refl
+  applicativeComposition (Left x) (Left y) (Left z) = Refl
+  applicativeComposition (Left x) (Left y) (Right z) = Refl
+  applicativeComposition (Left x) (Right y) (Left z) = Refl
+  applicativeComposition (Left x) (Right y) (Right z) = Refl
+  applicativeComposition (Right x) (Left y) (Left z) = Refl
+  applicativeComposition (Right x) (Left y) (Right z) = Refl
+  applicativeComposition (Right x) (Right y) (Left z) = Refl
+  applicativeComposition (Right x) (Right y) (Right z) = Refl
+  applicativeHomomorphism x g = Refl
+  applicativeInterchange x (Left y) = Refl
+  applicativeInterchange x (Right y) = Refl
+
+private
+foldrConcatEq : (g1 : List (a -> b)) -> (g2 : List (a -> b)) ->
+                (xs : List a) ->
+                foldr (\f, meth => map f xs ++ meth) [] (g1 ++ g2) = foldr (\f, meth => map f xs ++ meth) [] g1 ++ foldr (\f, meth => map f xs ++ meth) [] g2
+foldrConcatEq [] _ _ = Refl
+foldrConcatEq (g1 :: gs1) gs2 xs =
+  trans
+    (cong $ foldrConcatEq gs1 gs2 xs)
+    (appendAssociative
+      (map g1 xs)
+      (foldr (\f, meth => map f xs ++ meth) [] gs1)
+      (foldr (\f, meth => map f xs ++ meth) [] gs2))
+
+private
+foldrConcatEq' : (x1 : List a) -> (x2 : List a) ->
+                 (g : a -> List b) ->
+                 foldr (\x, meth => g x ++ meth) [] (x1 ++ x2) = foldr (\x, meth => g x ++ meth) [] x1 ++ foldr (\x, meth => g x ++ meth) [] x2
+foldrConcatEq' [] _ _ = Refl
+foldrConcatEq' (x1 :: xs1) xs2 g =
+  trans
+    (cong {f=((++) $ g x1)} $ foldrConcatEq' xs1 xs2 g)
+    (appendAssociative
+      (g x1)
+      (foldr (\x, meth => g x ++ meth) [] xs1)
+      (foldr (\x, meth => g x ++ meth) [] xs2))
+
+private
+foldrMapCombine : (xs : List a) -> (gs1 : List (a -> b)) -> (g2 : b -> c) ->
+                  map g2 (foldr (\g, meth => map g xs ++ meth) [] gs1) =
+                  foldr (\g, meth => map g xs ++ meth) [] (map ((.) g2) gs1)
+foldrMapCombine xs [] g2 = Refl
+foldrMapCombine xs (g1 :: gs1) g2 =
+  trans
+    (mapAppendDistributive g2 (map g1 xs) (foldr (\g, meth => map g xs ++ meth) [] gs1))
+    (appendCong2 (sym $ functorComposition xs g1 g2) (foldrMapCombine xs gs1 g2))
+
+VerifiedApplicative List where
+  applicativeMap [] f = Refl
+  applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
+  applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs
+  applicativeComposition _ _ [] = Refl
+  applicativeComposition xs gs1 (g2 :: gs2) = trans
+    (trans
+      (foldrConcatEq (map ((.) g2) gs1) (foldr (\g, meth => map g gs1 ++ meth) [] (map (.) gs2 ++ [])) xs)
+      (cong $ applicativeComposition xs gs1 gs2))
+    (sym $
+      cong {f=(++ foldr (\g, meth => map g (foldr (\g', meth' => map g' xs ++ meth') [] gs1) ++ meth) [] gs2)} $
+        foldrMapCombine xs gs1 g2)
+  applicativeHomomorphism x g = Refl
+  applicativeInterchange x [] = Refl
+  applicativeInterchange x (g :: gs) = cong $ applicativeInterchange x gs
+
+VerifiedApplicative (Vect n) where
+  applicativeMap [] f = Refl
+  applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
+  applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs
+  applicativeComposition [] [] [] = Refl
+  applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl
+  applicativeHomomorphism = prf
+    where prf : with Vect ((x : a) -> (f : a -> b) -> zipWith Basics.apply (replicate m f) (replicate m x) = replicate m (f x))
+          prf {m = Z} x f = Refl
+          prf {m = S k} x f = rewrite prf {m = k} x f in Refl
+  applicativeInterchange = prf
+    where prf : with Vect ((x : a) -> (f : Vect m (a -> b)) -> zipWith Basics.apply f (replicate m x) = zipWith Basics.apply (replicate m (\f' => f' x)) f)
+          prf {m = Z} x [] = Refl
+          prf {m = S k} x (f :: fs) = rewrite prf x fs in Refl
+
+VerifiedApplicative Maybe where
+  applicativeMap Nothing g = Refl
+  applicativeMap (Just x) g = Refl
+  applicativeIdentity Nothing = Refl
+  applicativeIdentity (Just x) = Refl
+  applicativeComposition Nothing Nothing Nothing = Refl
+  applicativeComposition Nothing Nothing (Just x) = Refl
+  applicativeComposition Nothing (Just x) Nothing = Refl
+  applicativeComposition Nothing (Just x) (Just y) = Refl
+  applicativeComposition (Just x) Nothing Nothing = Refl
+  applicativeComposition (Just x) Nothing (Just y) = Refl
+  applicativeComposition (Just x) (Just y) Nothing = Refl
+  applicativeComposition (Just x) (Just y) (Just z) = Refl
+  applicativeHomomorphism x g = Refl
+  applicativeInterchange x Nothing = Refl
+  applicativeInterchange x (Just y) = Refl
+
+-- Monad
+
+VerifiedMonad (Either a) where
+  monadApplicative (Left x) (Left y) = Refl
+  monadApplicative (Left x) (Right y) = Refl
+  monadApplicative (Right x) (Left y) = Refl
+  monadApplicative (Right x) (Right y) = Refl
+  monadLeftIdentity x f = Refl
+  monadRightIdentity (Left x) = Refl
+  monadRightIdentity (Right x) = Refl
+  monadAssociativity (Left x) f g = Refl
+  monadAssociativity (Right x) f g = Refl
+
+VerifiedMonad Maybe where
+  monadApplicative Nothing Nothing = Refl
+  monadApplicative Nothing (Just x) = Refl
+  monadApplicative (Just x) Nothing = Refl
+  monadApplicative (Just x) (Just y) = Refl
+  monadLeftIdentity x f = Refl
+  monadRightIdentity Nothing = Refl
+  monadRightIdentity (Just x) = Refl
+  monadAssociativity Nothing f g = Refl
+  monadAssociativity (Just x) f g = Refl
+
+VerifiedMonad List where
+  monadApplicative [] _ = Refl
+  monadApplicative (x :: xs) [] = Refl
+  monadApplicative (g :: gs) xs = appendCong2 (mapFoldrEq g xs) (monadApplicative gs xs) where
+    mapFoldrEq : (f : a -> b) -> (x : List a) -> map f x = foldr (\x1, meth => f x1 :: meth) [] x
+    mapFoldrEq _ [] = Refl
+    mapFoldrEq f (_ :: x) = cong $ mapFoldrEq f x
+  monadLeftIdentity x f = appendNilRightNeutral (f x)
+  monadRightIdentity [] = Refl
+  monadRightIdentity (x :: xs) = cong $ monadRightIdentity xs
+  monadAssociativity [] _ _ = Refl
+  monadAssociativity (x :: xs) g1 g2 =
+    trans
+      (foldrConcatEq' (g1 x) (foldr (\x1, meth => g1 x1 ++ meth) [] xs) g2)
+      (cong $ monadAssociativity xs g1 g2)
+
+-- Alternative
+
+VerifiedAlternative Maybe where
+  alternativeLeftIdentity _ = Refl
+  alternativeRightIdentity Nothing = Refl
+  alternativeRightIdentity (Just _) = Refl
+  alternativeAssociativity Nothing _ _ = Refl
+  alternativeAssociativity (Just _) _ _ = Refl
+
+VerifiedAlternative List where
+  alternativeLeftIdentity _ = Refl
+  alternativeRightIdentity = appendNilRightNeutral
+  alternativeAssociativity = appendAssociative
+
+-- Semigroup
+
+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
+
+-- Monoid
+
+[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
+
+-- Group
+
+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
+
+-- Every integer can be gotten by repeatedly adding or subtracting 1.
+CyclicGroup ZZ where
+  generator = (1 ** \x => (x **
+    case x of
+      (Pos Z) => Refl
+      (Pos (S k)) => mtimesSuccPos k
+      (NegS k) => mtimesSuccNeg k))
+    where
+    mtimesSuccPos : (k : Nat) -> Pos (S k) = 1 + (mtimes' k 1)
+    mtimesSuccPos Z = Refl
+    mtimesSuccPos (S k) = rewrite sym $ mtimesSuccPos k in Refl
+
+    mtimesSuccNeg : (k : Nat) -> NegS k = -1 + mtimes' k (-1)
+    mtimesSuccNeg Z = Refl
+    mtimesSuccNeg (S k) = rewrite sym $ mtimesSuccNeg k in Refl
+
+-- Ring
+
+VerifiedRing ZZ where
+  ringOpIsAssociative = multAssociativeZ
+  ringOpIsDistributiveL = multDistributesOverPlusRightZ
+  ringOpIsDistributiveR = multDistributesOverPlusLeftZ
+
+VerifiedRingWithUnity ZZ where
+  ringWithUnityIsUnityL = multOneRightNeutralZ
+  ringWithUnityIsUnityR = multOneLeftNeutralZ
+
+-- Lattice
+
+VerifiedJoinSemilattice Nat where
+  joinSemilatticeJoinIsAssociative = maximumAssociative
+  joinSemilatticeJoinIsCommutative = maximumCommutative
+  joinSemilatticeJoinIsIdempotent  = maximumIdempotent
+
+VerifiedJoinSemilattice Bool where
+  joinSemilatticeJoinIsAssociative = orAssociative
+  joinSemilatticeJoinIsCommutative = orCommutative
+  joinSemilatticeJoinIsIdempotent = orSameNeutral
+
+
+VerifiedMeetSemilattice Nat where
+  meetSemilatticeMeetIsAssociative = minimumAssociative
+  meetSemilatticeMeetIsCommutative = minimumCommutative
+  meetSemilatticeMeetIsIdempotent  = minimumIdempotent
+
+VerifiedMeetSemilattice Bool where
+  meetSemilatticeMeetIsAssociative = andAssociative
+  meetSemilatticeMeetIsCommutative = andCommutative
+  meetSemilatticeMeetIsIdempotent = andSameNeutral
+
+VerifiedBoundedJoinSemilattice Nat where
+  joinBottomIsIdentity = maximumZeroNLeft
+
+VerifiedBoundedJoinSemilattice Bool where
+  joinBottomIsIdentity = orFalseNeutral
+
+VerifiedBoundedMeetSemilattice Bool where
+  meetTopIsIdentity = andTrueNeutral
+
+----------------------------------------
+
+VerifiedSemigroup a => VerifiedSemigroup (Identity a) where
+  semigroupOpIsAssociative (Id l) (Id c) (Id r) =
+    rewrite semigroupOpIsAssociative l c r in Refl
+
+VerifiedMonoid a => VerifiedMonoid (Identity a) where
+  monoidNeutralIsNeutralL (Id l) =
+    rewrite monoidNeutralIsNeutralL l in Refl
+  monoidNeutralIsNeutralR (Id r) =
+    rewrite monoidNeutralIsNeutralR r in Refl
+
+VerifiedSemigroup (Endomorphism a) where
+  semigroupOpIsAssociative (Endo _) (Endo _) (Endo _) = Refl
+
+VerifiedMonoid (Endomorphism a) where
+  monoidNeutralIsNeutralL (Endo _) = Refl
+  monoidNeutralIsNeutralR (Endo _) = Refl
+
+VerifiedSemigroup Sign where
+  semigroupOpIsAssociative Zero _ _ = Refl
+  semigroupOpIsAssociative Plus Zero _ = Refl
+  semigroupOpIsAssociative Minus Zero _ = Refl
+  semigroupOpIsAssociative Plus Plus Zero = Refl
+  semigroupOpIsAssociative Plus Minus Zero = Refl
+  semigroupOpIsAssociative Minus Plus Zero = Refl
+  semigroupOpIsAssociative Minus Minus Zero = Refl
+  semigroupOpIsAssociative Plus Plus Plus = Refl
+  semigroupOpIsAssociative Plus Minus Plus = Refl
+  semigroupOpIsAssociative Minus Plus Plus = Refl
+  semigroupOpIsAssociative Minus Minus Plus = Refl
+  semigroupOpIsAssociative Plus Plus Minus = Refl
+  semigroupOpIsAssociative Plus Minus Minus = Refl
+  semigroupOpIsAssociative Minus Plus Minus = Refl
+  semigroupOpIsAssociative Minus Minus Minus = Refl
+
+VerifiedMonoid Sign where
+  monoidNeutralIsNeutralL Plus = Refl
+  monoidNeutralIsNeutralL Zero = Refl
+  monoidNeutralIsNeutralL Minus = Refl
+
+  monoidNeutralIsNeutralR Plus = Refl
+  monoidNeutralIsNeutralR Zero = Refl
+  monoidNeutralIsNeutralR Minus = Refl
diff --git a/libs/contrib/Control/Isomorphism/Vect.idr b/libs/contrib/Control/Isomorphism/Vect.idr
index 611ea0b9fe..1b8db82e08 100644
--- a/libs/contrib/Control/Isomorphism/Vect.idr
+++ b/libs/contrib/Control/Isomorphism/Vect.idr
@@ -2,7 +2,6 @@ module Control.Isomorphism.Vect
 
 import Control.Isomorphism
 import Data.Vect
-import Interfaces.Verified
 
 %default total
 %access public export
diff --git a/libs/contrib/Data/Bool/Algebra.idr b/libs/contrib/Data/Bool/Algebra.idr
index 069b2e7da7..86b0b40670 100644
--- a/libs/contrib/Data/Bool/Algebra.idr
+++ b/libs/contrib/Data/Bool/Algebra.idr
@@ -1,7 +1,8 @@
 module Data.Bool.Algebra
 
 import Control.Algebra
-import Interfaces.Verified
+import Control.Algebra.CyclicGroup
+import Data.ZZ
 
 %access public export
 %default total
@@ -17,10 +18,10 @@ xor True True = False
 xor False False = False
 xor _ _ = True
 
-[PlusBoolSemi] Semigroup Bool where
+Semigroup Bool where
   (<+>) = xor
 
-[PlusBoolSemiV] VerifiedSemigroup Bool using PlusBoolSemi where
+VerifiedSemigroup Bool where
   semigroupOpIsAssociative True True True = Refl
   semigroupOpIsAssociative True True False = Refl
   semigroupOpIsAssociative True False True = Refl
@@ -30,36 +31,34 @@ 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
+VerifiedMonoid Bool 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
+VerifiedGroup Bool where
   groupInverseIsInverseR True = Refl
   groupInverseIsInverseR False = Refl
 
-[PlusBoolAbel] AbelianGroup Bool using PlusBoolGroup where
+CyclicGroup Bool where
+  generator = (True ** \x =>
+    case x of
+      True => (1 ** Refl)
+      False => (0 ** Refl))
 
-[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
+VerifiedRing Bool where
   ringOpIsAssociative True True True = Refl
   ringOpIsAssociative True True False = Refl
   ringOpIsAssociative True False True = Refl
@@ -87,10 +86,10 @@ 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
+VerifiedRingWithUnity Bool where
   ringWithUnityIsUnityL True = Refl
   ringWithUnityIsUnityL False = Refl
 
diff --git a/libs/contrib/Data/BoundedList.idr b/libs/contrib/Data/BoundedList.idr
index 0be89a830e..c48951e105 100644
--- a/libs/contrib/Data/BoundedList.idr
+++ b/libs/contrib/Data/BoundedList.idr
@@ -2,6 +2,7 @@ module Data.BoundedList
 
 import Data.Fin
 import Data.Vect
+import Control.Algebra
 
 %access public export
 %default total
@@ -100,11 +101,30 @@ implementation Semigroup a => Semigroup (BoundedList n a) where
   xs <+> [] = xs
   [] <+> ys = ys
 
+VerifiedSemigroup a => VerifiedSemigroup (BoundedList n a) where
+  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 = []
 
+VerifiedMonoid a => VerifiedMonoid (BoundedList n a) where
+  monoidNeutralIsNeutralL [] = Refl
+  monoidNeutralIsNeutralL (_ :: _) = Refl
+  monoidNeutralIsNeutralR [] = Refl
+  monoidNeutralIsNeutralR (_ :: _) = Refl
+
 --------------------------------------------------------------------------------
 -- Misc
 --------------------------------------------------------------------------------
diff --git a/libs/contrib/Data/Matrix/Algebraic.idr b/libs/contrib/Data/Matrix/Algebraic.idr
index 10a28f90bf..8d0f181d1e 100644
--- a/libs/contrib/Data/Matrix/Algebraic.idr
+++ b/libs/contrib/Data/Matrix/Algebraic.idr
@@ -3,6 +3,7 @@
 ||| and `Control.Algebra.VectorSpace`.
 module Data.Matrix.Algebraic
 
+import public Data.Vect
 import public Control.Algebra
 import public Control.Algebra.VectorSpace
 import public Control.Algebra.NumericImplementations
@@ -35,21 +36,12 @@ implementation Monoid a => Monoid (Vect n a) where
 implementation Group a => Group (Vect n a) where
   inverse = map inverse
 
-implementation AbelianGroup a => AbelianGroup (Vect n a) where {}
-
 implementation Ring a => Ring (Vect n a) where
   (<.>) = zipWith (<.>)
 
 implementation RingWithUnity a => RingWithUnity (Vect n a) where
   unity {n} = replicate n unity
 
-implementation RingWithUnity a => Module a (Vect n a) where
-  (<#>) r = map (r <.>)
-
-implementation 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'
-
 -----------------------------------------------------------------------
 --                        (Ring) Vector functions
 -----------------------------------------------------------------------
@@ -146,4 +138,79 @@ det {n} m = case n of
 --                      Matrix Algebra Properties
 -----------------------------------------------------------------------
 
--- TODO: Prove properties of matrix algebra for 'Verified' algebraic interfaces
+VerifiedSemigroup a => VerifiedSemigroup (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
+
+VerifiedMonoid a => VerifiedMonoid (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
+
+VerifiedGroup a => VerifiedGroup (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
+
+VerifiedRing a => VerifiedRing (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
+
+VerifiedRingWithUnity a => VerifiedRingWithUnity (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
+
+-- Vector spaces -----------------------
+
+-- These need to come after the "verified" implementations because ???
+
+implementation RingWithUnity a => Module a (Vect n a) where
+  (<#>) r = map (r <.>)
+
+implementation 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'
diff --git a/libs/contrib/Data/Monoid.idr b/libs/contrib/Data/Monoid.idr
index f3ee5224c0..595b4a16c2 100644
--- a/libs/contrib/Data/Monoid.idr
+++ b/libs/contrib/Data/Monoid.idr
@@ -2,6 +2,8 @@
 ||| https://hackage.haskell.org/package/base-4.9.0.0/docs/src/Data.Monoid.html
 module Data.Monoid
 
+import Control.Algebra
+
 %access public export
 %default total
 
@@ -11,11 +13,71 @@ module Data.Monoid
 Semigroup () where
   (<+>) _ _ = ()
 
+VerifiedSemigroup () where
+  semigroupOpIsAssociative _ _ _ = Refl
+
 Monoid () where
   neutral = ()
 
+VerifiedMonoid () where
+  monoidNeutralIsNeutralL () = Refl
+  monoidNeutralIsNeutralR () = Refl
+
+-- Direct Products
+
 (Semigroup m, Semigroup n) => Semigroup (m, n) where
   (a, b) <+> (c, d) = (a <+> c, b <+> d)
 
+(VerifiedSemigroup m, VerifiedSemigroup n) => VerifiedSemigroup (m, n) where
+  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)
+
+(VerifiedMonoid m, VerifiedMonoid n) => VerifiedMonoid (m, n) where
+  monoidNeutralIsNeutralL (a, b) =
+    rewrite monoidNeutralIsNeutralL a in
+      rewrite monoidNeutralIsNeutralL b in
+        Refl
+
+  monoidNeutralIsNeutralR (a, b) =
+    rewrite monoidNeutralIsNeutralR a in
+      rewrite monoidNeutralIsNeutralR b in
+        Refl
+
+(Group g, Group h) => Group (g, h) where
+  inverse (a, b) = (inverse a, inverse b)
+
+(VerifiedGroup g, VerifiedGroup h) => VerifiedGroup (g, h) where
+  groupInverseIsInverseR (a, b) =
+    rewrite groupInverseIsInverseR a in
+      rewrite groupInverseIsInverseR b in
+        Refl
+
+(AbelianGroup g, AbelianGroup h) => AbelianGroup (g, h) where
+  abelianGroupOpIsCommutative (a, b) (c, d) =
+    rewrite abelianGroupOpIsCommutative a c in
+      rewrite abelianGroupOpIsCommutative b d in
+        Refl
+
+(Ring r, Ring s) => Ring (r, s) where
+  (<.>) (a, b) (c, d) = ((a <.> c), (b <.> d))
+
+(VerifiedRing r, VerifiedRing s) => VerifiedRing (r, s) where
+  ringOpIsAssociative (a, b) (c, d) (e, f) =
+    rewrite ringOpIsAssociative a c e in
+      rewrite ringOpIsAssociative b d f in
+        Refl
+
+  ringOpIsDistributiveL (a, b) (c, d) (e, f) =
+    rewrite ringOpIsDistributiveL a c e in
+      rewrite ringOpIsDistributiveL b d f in
+        Refl
+
+  ringOpIsDistributiveR (a, b) (c, d) (e, f) =
+    rewrite ringOpIsDistributiveR a c e in
+      rewrite ringOpIsDistributiveR b d f in
+        Refl
diff --git a/libs/contrib/Data/Sign.idr b/libs/contrib/Data/Sign.idr
index 2d35b509ed..5ee010a93f 100644
--- a/libs/contrib/Data/Sign.idr
+++ b/libs/contrib/Data/Sign.idr
@@ -1,20 +1,15 @@
 module Data.Sign
 
+import Prelude.Algebra
+
 %access public export
 
+%default total
+
 ||| A representation of signs for signed datatypes such as `ZZ`
 data Sign = Plus | Zero | Minus
 
-opposite : Sign -> Sign
-opposite Plus  = Minus
-opposite Zero  = Zero
-opposite Minus = Plus
-
-multiply : Sign -> Sign -> Sign
-multiply Zero  _    = Zero
-multiply _     Zero = Zero
-multiply Plus  x    = x
-multiply Minus x    = opposite x
+-- Signed interface --------------------
 
 ||| Discover the sign of some type
 interface Signed t where
@@ -37,3 +32,62 @@ Signed Double where
     | LT = Minus
     | EQ = Zero
     | GT = Plus
+
+-- Implementations ---------------------
+
+Eq Sign where
+  Zero == Zero = True
+  Plus == Plus = True
+  Minus == Minus = True
+  _ == _ = False
+
+Num Sign where
+  (+) Zero x      = x
+  (+) x Zero      = x
+  (+) Plus Minus  = Zero
+  (+) Plus Plus   = Plus
+  (+) Minus Plus  = Zero
+  (+) Minus Minus = Minus
+
+  (*) Zero  _     = Zero
+  (*) _     Zero  = Zero
+  (*) Plus  x     = x
+  (*) x     Plus  = x
+  (*) Minus Minus = Plus
+
+  fromInteger 0 = Zero
+  fromInteger n = if n > 0 then Plus else Minus
+
+Neg Sign where
+  negate Plus  = Minus
+  negate Zero  = Zero
+  negate Minus = Plus
+
+  (-) x y = x + negate y
+
+Abs Sign where
+  abs Zero = Zero
+  abs _    = Plus
+
+Ord Sign where
+  compare Zero Zero   = EQ
+  compare Plus Plus   = EQ
+  compare _ Plus      = LT
+  compare Plus _      = GT
+  compare Minus Minus = EQ
+  compare Minus _     = LT
+  compare _ Minus     = GT
+
+MinBound Sign where
+  minBound = Minus
+
+MaxBound Sign where
+  maxBound = Plus
+
+-- Algebra -----------------------------
+
+Semigroup Sign where
+  (<+>) = (*)
+
+Monoid Sign where
+  neutral = Plus
diff --git a/libs/contrib/Interfaces/Verified.idr b/libs/contrib/Interfaces/Verified.idr
index f7abf35337..e7195563ac 100644
--- a/libs/contrib/Interfaces/Verified.idr
+++ b/libs/contrib/Interfaces/Verified.idr
@@ -1,22 +1,11 @@
 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
 
--- Due to these being basically unused and difficult to implement,
--- they're in contrib for a bit. Once a design is found that lets them
--- be implemented for a number of implementations, and we get those
--- implementations, then some of them can move back to base (or even
--- prelude, in the cases of Functor, Applicative, Monad, Semigroup,
--- and Monoid).
+----------------------------------------
 
 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
@@ -24,37 +13,6 @@ interface Functor f => VerifiedFunctor (f : Type -> Type) where
                        (g1 : a -> b) -> (g2 : b -> c) ->
                        map (g2 . g1) x = (map g2 . map g1) x
 
-functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x
-functorIdentity' {f} = functorIdentity {f} id (\x => Refl)
-
-VerifiedFunctor (Pair a) where
-  functorIdentity g p (a,b) = rewrite p b in Refl
-  functorComposition (a,b) g1 g2 = Refl
-
-VerifiedFunctor (Either a) where
-  functorIdentity _ _ (Left _) = Refl
-  functorIdentity _ p (Right x) = cong (p x)
-  functorComposition (Left _) _ _ = Refl
-  functorComposition (Right _) _ _ = Refl
-
-VerifiedFunctor Maybe where
-  functorIdentity _ _ Nothing = Refl
-  functorIdentity g p (Just x) = rewrite p x in Refl
-  functorComposition Nothing g1 g2 = Refl
-  functorComposition (Just x) g1 g2 = Refl
-
-VerifiedFunctor List where
-  functorIdentity _ _ [] = Refl
-  functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
-  functorComposition [] _ _ = Refl
-  functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
-
-VerifiedFunctor (Vect n) where
-  functorIdentity _ _ [] = Refl
-  functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
-  functorComposition [] _ _ = Refl
-  functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
-
 interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
   applicativeMap : (x : f a) -> (g : a -> b) ->
                    map g x = pure g <*> x
@@ -66,107 +24,6 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
   applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
                            g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
 
-VerifiedApplicative (Either a) where
-  applicativeMap (Left x) g = Refl
-  applicativeMap (Right x) g = Refl
-  applicativeIdentity (Left x) = Refl
-  applicativeIdentity (Right x) = Refl
-  applicativeComposition (Left x) (Left y) (Left z) = Refl
-  applicativeComposition (Left x) (Left y) (Right z) = Refl
-  applicativeComposition (Left x) (Right y) (Left z) = Refl
-  applicativeComposition (Left x) (Right y) (Right z) = Refl
-  applicativeComposition (Right x) (Left y) (Left z) = Refl
-  applicativeComposition (Right x) (Left y) (Right z) = Refl
-  applicativeComposition (Right x) (Right y) (Left z) = Refl
-  applicativeComposition (Right x) (Right y) (Right z) = Refl
-  applicativeHomomorphism x g = Refl
-  applicativeInterchange x (Left y) = Refl
-  applicativeInterchange x (Right y) = Refl
-
-private
-foldrConcatEq : (g1 : List (a -> b)) -> (g2 : List (a -> b)) ->
-                (xs : List a) ->
-                foldr (\f, meth => map f xs ++ meth) [] (g1 ++ g2) = foldr (\f, meth => map f xs ++ meth) [] g1 ++ foldr (\f, meth => map f xs ++ meth) [] g2
-foldrConcatEq [] _ _ = Refl
-foldrConcatEq (g1 :: gs1) gs2 xs =
-  trans
-    (cong $ foldrConcatEq gs1 gs2 xs)
-    (appendAssociative
-      (map g1 xs)
-      (foldr (\f, meth => map f xs ++ meth) [] gs1)
-      (foldr (\f, meth => map f xs ++ meth) [] gs2))
-
-private
-foldrConcatEq' : (x1 : List a) -> (x2 : List a) ->
-                 (g : a -> List b) ->
-                 foldr (\x, meth => g x ++ meth) [] (x1 ++ x2) = foldr (\x, meth => g x ++ meth) [] x1 ++ foldr (\x, meth => g x ++ meth) [] x2
-foldrConcatEq' [] _ _ = Refl
-foldrConcatEq' (x1 :: xs1) xs2 g =
-  trans
-    (cong {f=((++) $ g x1)} $ foldrConcatEq' xs1 xs2 g)
-    (appendAssociative
-      (g x1)
-      (foldr (\x, meth => g x ++ meth) [] xs1)
-      (foldr (\x, meth => g x ++ meth) [] xs2))
-
-private
-foldrMapCombine : (xs : List a) -> (gs1 : List (a -> b)) -> (g2 : b -> c) ->
-                  map g2 (foldr (\g, meth => map g xs ++ meth) [] gs1) =
-                  foldr (\g, meth => map g xs ++ meth) [] (map ((.) g2) gs1)
-foldrMapCombine xs [] g2 = Refl
-foldrMapCombine xs (g1 :: gs1) g2 =
-  trans
-    (mapAppendDistributive g2 (map g1 xs) (foldr (\g, meth => map g xs ++ meth) [] gs1))
-    (appendCong2 (sym $ functorComposition xs g1 g2) (foldrMapCombine xs gs1 g2))
-
-VerifiedApplicative List where
-  applicativeMap [] f = Refl
-  applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
-  applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs
-  applicativeComposition _ _ [] = Refl
-  applicativeComposition xs gs1 (g2 :: gs2) = trans
-    (trans
-      (foldrConcatEq (map ((.) g2) gs1) (foldr (\g, meth => map g gs1 ++ meth) [] (map (.) gs2 ++ [])) xs)
-      (cong $ applicativeComposition xs gs1 gs2))
-    (sym $
-      cong {f=(++ foldr (\g, meth => map g (foldr (\g', meth' => map g' xs ++ meth') [] gs1) ++ meth) [] gs2)} $
-        foldrMapCombine xs gs1 g2)
-  applicativeHomomorphism x g = Refl
-  applicativeInterchange x [] = Refl
-  applicativeInterchange x (g :: gs) = cong $ applicativeInterchange x gs
-
-VerifiedApplicative (Vect n) where
-  applicativeMap [] f = Refl
-  applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
-  applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs
-  applicativeComposition [] [] [] = Refl
-  applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl
-  applicativeHomomorphism = prf
-    where prf : with Vect ((x : a) -> (f : a -> b) -> zipWith Basics.apply (replicate m f) (replicate m x) = replicate m (f x))
-          prf {m = Z} x f = Refl
-          prf {m = S k} x f = rewrite prf {m = k} x f in Refl
-  applicativeInterchange = prf
-    where prf : with Vect ((x : a) -> (f : Vect m (a -> b)) -> zipWith Basics.apply f (replicate m x) = zipWith Basics.apply (replicate m (\f' => f' x)) f)
-          prf {m = Z} x [] = Refl
-          prf {m = S k} x (f :: fs) = rewrite prf x fs in Refl
-
-VerifiedApplicative Maybe where
-  applicativeMap Nothing g = Refl
-  applicativeMap (Just x) g = Refl
-  applicativeIdentity Nothing = Refl
-  applicativeIdentity (Just x) = Refl
-  applicativeComposition Nothing Nothing Nothing = Refl
-  applicativeComposition Nothing Nothing (Just x) = Refl
-  applicativeComposition Nothing (Just x) Nothing = Refl
-  applicativeComposition Nothing (Just x) (Just y) = Refl
-  applicativeComposition (Just x) Nothing Nothing = Refl
-  applicativeComposition (Just x) Nothing (Just y) = Refl
-  applicativeComposition (Just x) (Just y) Nothing = Refl
-  applicativeComposition (Just x) (Just y) (Just z) = Refl
-  applicativeHomomorphism x g = Refl
-  applicativeInterchange x Nothing = Refl
-  applicativeInterchange x (Just y) = Refl
-
 interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
   monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
                      mf <*> mx = mf >>= \f =>
@@ -177,178 +34,26 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
   monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
                        (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
 
-VerifiedMonad (Either a) where
-  monadApplicative (Left x) (Left y) = Refl
-  monadApplicative (Left x) (Right y) = Refl
-  monadApplicative (Right x) (Left y) = Refl
-  monadApplicative (Right x) (Right y) = Refl
-  monadLeftIdentity x f = Refl
-  monadRightIdentity (Left x) = Refl
-  monadRightIdentity (Right x) = Refl
-  monadAssociativity (Left x) f g = Refl
-  monadAssociativity (Right x) f g = Refl
-
-VerifiedMonad Maybe where
-  monadApplicative Nothing Nothing = Refl
-  monadApplicative Nothing (Just x) = Refl
-  monadApplicative (Just x) Nothing = Refl
-  monadApplicative (Just x) (Just y) = Refl
-  monadLeftIdentity x f = Refl
-  monadRightIdentity Nothing = Refl
-  monadRightIdentity (Just x) = Refl
-  monadAssociativity Nothing f g = Refl
-  monadAssociativity (Just x) f g = Refl
-
-VerifiedMonad List where
-  monadApplicative [] _ = Refl
-  monadApplicative (x :: xs) [] = Refl
-  monadApplicative (g :: gs) xs = appendCong2 (mapFoldrEq g xs) (monadApplicative gs xs) where
-    mapFoldrEq : (f : a -> b) -> (x : List a) -> map f x = foldr (\x1, meth => f x1 :: meth) [] x
-    mapFoldrEq _ [] = Refl
-    mapFoldrEq f (_ :: x) = cong $ mapFoldrEq f x
-  monadLeftIdentity x f = appendNilRightNeutral (f x)
-  monadRightIdentity [] = Refl
-  monadRightIdentity (x :: xs) = cong $ monadRightIdentity xs
-  monadAssociativity [] _ _ = Refl
-  monadAssociativity (x :: xs) g1 g2 =
-    trans
-      (foldrConcatEq' (g1 x) (foldr (\x1, meth => g1 x1 ++ meth) [] xs) g2)
-      (cong $ monadAssociativity xs g1 g2)
-
 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
   alternativeAssociativity : (x : f a) -> (y : f a) -> (z : f a) ->
                              x <|> (y <|> z) = (x <|> y) <|> z
 
-VerifiedAlternative Maybe where
-  alternativeLeftIdentity _ = Refl
-  alternativeRightIdentity Nothing = Refl
-  alternativeRightIdentity (Just _) = Refl
-  alternativeAssociativity Nothing _ _ = Refl
-  alternativeAssociativity (Just _) _ _ = Refl
-
-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/contrib.ipkg b/libs/contrib/contrib.ipkg
index 1c29c26a0b..ea3fb9c13b 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -10,7 +10,11 @@ modules = CFFI
         , Control.Algebra.Lattice
         , Control.Algebra.Laws
         , Control.Algebra.NumericImplementations
+        , Control.Algebra.VerifiedImplementations
+        , Control.Algebra.ComplexImplementations
         , Control.Algebra.VectorSpace
+        , Control.Algebra.GroupHomomorphism
+        , Control.Algebra.CyclicGroup
 
         , Control.Delayed
 
@@ -46,6 +50,7 @@ modules = CFFI
         , Data.List.Zipper
         , Data.List.Reverse
 
+        , Data.Monoid
         , Data.Matrix
         , Data.Matrix.Algebraic
         , Data.Matrix.Numeric