From 3f985bcefad396a0a7699f18463554393ec527d9 Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Mon, 17 Jun 2024 13:45:16 +0100
Subject: [PATCH] [ fix #72 ] remove the broken modules (#3319)

* [ fix #72 ] remove the broken modules

People are still hitting the same issueT
There has been no movement towards fixing it
It is IMO unfixable

Let's drop it.

* [ fix #72 ] Remove dependencies of Control.Algebra

Follow-up to the commit by gallais, this removes the contrib libraries
which were using `Control.Algebra`.

* [ fix #72 ] Record changes in CHANGELOG_NEXT

* [ lint ] Move Algebra changes to existing header

---------

Co-authored-by: Thomas E. Hansen <teh6@st-andrews.ac.uk>
---
 CHANGELOG_NEXT.md                             |  17 +
 libs/contrib/Control/Algebra.idr              | 154 ----------
 .../Control/Algebra/Implementations.idr       |  22 --
 libs/contrib/Control/Algebra/Laws.idr         | 290 ------------------
 libs/contrib/Control/Monad/Algebra.idr        |  18 --
 libs/contrib/Data/Bool/Algebra.idr            |  77 -----
 libs/contrib/Data/List/Algebra.idr            |  15 -
 libs/contrib/Data/Morphisms/Algebra.idr       |  15 -
 libs/contrib/Data/Nat/Algebra.idr             |  19 --
 libs/contrib/contrib.ipkg                     |  12 -
 10 files changed, 17 insertions(+), 622 deletions(-)
 delete mode 100644 libs/contrib/Control/Algebra.idr
 delete mode 100644 libs/contrib/Control/Algebra/Implementations.idr
 delete mode 100644 libs/contrib/Control/Algebra/Laws.idr
 delete mode 100644 libs/contrib/Control/Monad/Algebra.idr
 delete mode 100644 libs/contrib/Data/Bool/Algebra.idr
 delete mode 100644 libs/contrib/Data/List/Algebra.idr
 delete mode 100644 libs/contrib/Data/Morphisms/Algebra.idr
 delete mode 100644 libs/contrib/Data/Nat/Algebra.idr

diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index c75980661b..a5e69e3c98 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -199,6 +199,23 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Function `invFin` from `Data.Fin.Extra` was deprecated in favour of
   `Data.Fin.complement` from `base`.
 
+* The `Control.Algebra` library from `contrib` has been removed due to being
+    broken, unfixed for years, and on several independent occasions causing
+    confusion with people picking up Idris and trying to use it.
+  - Detailed discussion can be found in
+      [Idris2#72](https://github.com/idris-lang/Idris2/issues/72).
+  - For reasoning about algebraic structures and proofs, please see
+      [Frex](https://github.com/frex-project/idris-frex/) and
+      [idris2-algebra](https://github.com/stefan-hoeck/idris2-algebra/).
+
+* Since they depend on `Control.Algebra`, the following `contrib` libraries have
+    also been removed:
+  - `Control/Monad/Algebra.idr`
+  - `Data/Bool/Algebra.idr`
+  - `Data/List/Algebra.idr`
+  - `Data/Morphisms/Algebra.idr`
+  - `Data/Nat/Algebra.idr`
+
 #### Network
 
 * Add a missing function parameter (the flag) in the C implementation of `idrnet_recv_bytes`
diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
deleted file mode 100644
index 6fa1fc9eb8..0000000000
--- a/libs/contrib/Control/Algebra.idr
+++ /dev/null
@@ -1,154 +0,0 @@
-module Control.Algebra
-
-export infixl 6 <->
-export infixl 7 <.>
-
-public export
-interface Semigroup ty => SemigroupV ty where
-  semigroupOpIsAssociative : (l, c, r : ty) ->
-    l <+> (c <+> r) = (l <+> c) <+> r
-
-public export
-interface (Monoid ty, SemigroupV ty) => MonoidV ty where
-  monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral {ty} = l
-  monoidNeutralIsNeutralR : (r : ty) -> neutral {ty} <+> r = r
-
-||| Sets equipped with a single binary operation that is associative,
-||| along with a neutral element for that binary operation and
-||| inverses for all elements. Satisfies the following laws:
-|||
-||| + Associativity of `<+>`:
-|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-||| + Neutral for `<+>`:
-|||     forall a,     a <+> neutral   == a
-|||     forall a,     neutral <+> a   == a
-||| + Inverse for `<+>`:
-|||     forall a,     a <+> inverse a == neutral
-|||     forall a,     inverse a <+> a == neutral
-public export
-interface MonoidV ty => Group ty where
-  inverse : ty -> ty
-
-  groupInverseIsInverseR : (r : ty) -> inverse r <+> r = neutral {ty}
-
-(<->) : Group ty => ty -> ty -> ty
-(<->) 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. Satisfies the following
-||| laws:
-|||
-||| + Associativity of `<+>`:
-|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-||| + Commutativity of `<+>`:
-|||     forall a b,   a <+> b         == b <+> a
-||| + Neutral for `<+>`:
-|||     forall a,     a <+> neutral   == a
-|||     forall a,     neutral <+> a   == a
-||| + Inverse for `<+>`:
-|||     forall a,     a <+> inverse a == neutral
-|||     forall a,     inverse a <+> a == neutral
-public export
-interface Group ty => AbelianGroup ty where
-  groupOpIsCommutative : (l, r : ty) -> l <+> r = r <+> l
-
-||| A homomorphism is a mapping that preserves group structure.
-public export
-interface (Group a, Group b) => GroupHomomorphism a b where
-  to : a -> b
-
-  toGroup : (x, y : a) ->
-    to (x <+> y) = (to x) <+> (to y)
-
-||| Sets equipped with two binary operations, one associative and
-||| commutative supplied with a neutral element, and the other
-||| associative, with distributivity laws relating the two operations.
-||| Satisfies the following laws:
-|||
-||| + Associativity of `<+>`:
-|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-||| + Commutativity of `<+>`:
-|||     forall a b,   a <+> b         == b <+> a
-||| + Neutral for `<+>`:
-|||     forall a,     a <+> neutral   == a
-|||     forall a,     neutral <+> a   == a
-||| + Inverse for `<+>`:
-|||     forall a,     a <+> inverse a == neutral
-|||     forall a,     inverse a <+> a == neutral
-||| + Associativity of `<.>`:
-|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
-||| + Distributivity of `<.>` and `<+>`:
-|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
-|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
-public export
-interface Group ty => Ring ty where
-  (<.>) : ty -> ty -> ty
-
-  ringOpIsAssociative   : (l, c, r : ty) ->
-    l <.> (c <.> r) = (l <.> c) <.> r
-  ringOpIsDistributiveL : (l, c, r : ty) ->
-    l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
-  ringOpIsDistributiveR : (l, c, r : ty) ->
-    (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. Satisfies the following laws:
-|||
-||| +  Associativity of `<+>`:
-|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-||| + Commutativity of `<+>`:
-|||     forall a b,   a <+> b         == b <+> a
-||| + Neutral for `<+>`:
-|||     forall a,     a <+> neutral   == a
-|||     forall a,     neutral <+> a   == a
-||| + Inverse for `<+>`:
-|||     forall a,     a <+> inverse a == neutral
-|||     forall a,     inverse a <+> a == neutral
-||| + Associativity of `<.>`:
-|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
-||| + Neutral for `<.>`:
-|||     forall a,     a <.> unity     == a
-|||     forall a,     unity <.> a     == a
-||| + Distributivity of `<.>` and `<+>`:
-|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
-|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
-public export
-interface Ring ty => RingWithUnity ty where
-  unity : ty
-
-  unityIsRingIdL : (l : ty) -> l <.> unity = l
-  unityIsRingIdR : (r : ty) -> unity <.> r = r
-
-||| Sets equipped with two binary operations – both associative,
-||| commutative and possessing a neutral element – and distributivity
-||| laws relating the two operations. All elements except the additive
-||| identity should have a multiplicative inverse. Should (but may
-||| not) satisfy the following laws:
-|||
-||| + Associativity of `<+>`:
-|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
-||| + Commutativity of `<+>`:
-|||     forall a b,   a <+> b         == b <+> a
-||| + Neutral for `<+>`:
-|||     forall a,     a <+> neutral   == a
-|||     forall a,     neutral <+> a   == a
-||| + Inverse for `<+>`:
-|||     forall a,     a <+> inverse a == neutral
-|||     forall a,     inverse a <+> a == neutral
-||| + Associativity of `<.>`:
-|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
-||| + Unity for `<.>`:
-|||     forall a,     a <.> unity     == a
-|||     forall a,     unity <.> a     == a
-||| + InverseM of `<.>`, except for neutral
-|||     forall a /= neutral,  a <.> inverseM a == unity
-|||     forall a /= neutral,  inverseM a <.> a == unity
-||| + Distributivity of `<.>` and `<+>`:
-|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
-|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
-public export
-interface RingWithUnity ty => Field ty where
-  inverseM : (x : ty) -> Not (x = neutral {ty}) -> ty
diff --git a/libs/contrib/Control/Algebra/Implementations.idr b/libs/contrib/Control/Algebra/Implementations.idr
deleted file mode 100644
index fbb88e0848..0000000000
--- a/libs/contrib/Control/Algebra/Implementations.idr
+++ /dev/null
@@ -1,22 +0,0 @@
-module Control.Algebra.Implementations
-
-import Control.Algebra
-
--- This file is for algebra implementations with nowhere else to go.
-
-%default total
-
--- Functions ---------------------------
-
-Semigroup (ty -> ty) where
-  (<+>) = (.)
-
-SemigroupV (ty -> ty) where
-  semigroupOpIsAssociative _ _ _ = Refl
-
-Monoid (ty -> ty) where
-  neutral = id
-
-MonoidV (ty -> ty) where
-  monoidNeutralIsNeutralL _ = Refl
-  monoidNeutralIsNeutralR _ = Refl
diff --git a/libs/contrib/Control/Algebra/Laws.idr b/libs/contrib/Control/Algebra/Laws.idr
deleted file mode 100644
index 66b1d82017..0000000000
--- a/libs/contrib/Control/Algebra/Laws.idr
+++ /dev/null
@@ -1,290 +0,0 @@
-module Control.Algebra.Laws
-
-import Control.Algebra
-
-%default total
-
--- Monoids
-
-||| Inverses are unique.
-public export
-uniqueInverse : MonoidV ty => (x, y, z : ty) ->
-  y <+> x = neutral {ty} -> x <+> z = neutral {ty} -> y = z
-uniqueInverse x y z p q =
-  rewrite sym $ monoidNeutralIsNeutralL y in
-    rewrite sym q in
-      rewrite semigroupOpIsAssociative y x z in
-  rewrite p in
-    rewrite monoidNeutralIsNeutralR z in
-      Refl
-
--- Groups
-
-||| Only identity is self-squaring.
-public export
-selfSquareId : Group ty => (x : ty) ->
-  x <+> x = x -> x = neutral {ty}
-selfSquareId x p =
-  rewrite sym $ monoidNeutralIsNeutralR x in
-    rewrite sym $ groupInverseIsInverseR x in
-  rewrite sym $ semigroupOpIsAssociative (inverse x) x x in
-    rewrite p in
-      Refl
-
-||| Inverse elements commute.
-public export
-inverseCommute : Group ty => (x, y : ty) ->
-  y <+> x = neutral {ty} -> x <+> y = neutral {ty}
-inverseCommute x y p = selfSquareId (x <+> y) prop where
-  prop : (x <+> y) <+> (x <+> y) = x <+> y
-  prop =
-    rewrite sym $ semigroupOpIsAssociative x y (x <+> y) in
-      rewrite semigroupOpIsAssociative y x y in
-    rewrite p in
-      rewrite monoidNeutralIsNeutralR y in
-        Refl
-
-||| Every element has a right inverse.
-public export
-groupInverseIsInverseL : Group ty => (x : ty) ->
-  x <+> inverse x = neutral {ty}
-groupInverseIsInverseL x =
-  inverseCommute x (inverse x) (groupInverseIsInverseR x)
-
-||| -(-x) = x
-public export
-inverseSquaredIsIdentity : Group ty => (x : ty) ->
-  inverse (inverse x) = x
-inverseSquaredIsIdentity {ty} x =
-  uniqueInverse
-    (inverse x)
-    (inverse $ inverse x)
-    x
-    (groupInverseIsInverseR $ inverse x)
-    (groupInverseIsInverseR x)
-
-||| If every square in a group is identity, the group is commutative.
-public export
-squareIdCommutative : Group ty => (x, y : ty) ->
-  ((a : ty) -> a <+> a = neutral {ty}) ->
-  x <+> y = y <+> x
-squareIdCommutative x y p =
-  uniqueInverse (x <+> y) (x <+> y) (y <+> x) (p (x <+> y)) prop where
-    prop : (x <+> y) <+> (y <+> x) = neutral {ty}
-    prop =
-      rewrite sym $ semigroupOpIsAssociative x y (y <+> x) in
-        rewrite semigroupOpIsAssociative y y x in
-      rewrite p y in
-        rewrite monoidNeutralIsNeutralR x in
-          p x
-
-||| -0 = 0
-public export
-inverseNeutralIsNeutral : Group ty =>
-  inverse (neutral {ty}) = neutral {ty}
-inverseNeutralIsNeutral {ty} =
-  rewrite sym $ cong inverse (groupInverseIsInverseL (neutral {ty})) in
-    rewrite monoidNeutralIsNeutralR $ inverse (neutral {ty}) in
-      inverseSquaredIsIdentity (neutral {ty})
-
--- ||| -(x + y) = -y + -x
--- public export
--- inverseOfSum : Group ty => (l, r : ty) ->
---   inverse (l <+> r) = inverse r <+> inverse l
--- inverseOfSum {ty} l r =
---   -- expand
---   rewrite sym $ monoidNeutralIsNeutralR $ inverse $ l <+> r in
---     rewrite sym $ groupInverseIsInverseR r in
---       rewrite sym $ monoidNeutralIsNeutralL $ inverse r in
---         rewrite sym $ groupInverseIsInverseR l in
---   -- shuffle
---   rewrite semigroupOpIsAssociative (inverse r) (inverse l) l in
---     rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) l r in
---       rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse $ l <+> r) in
---   -- contract
---   rewrite sym $ monoidNeutralIsNeutralL $ inverse l in
---     rewrite groupInverseIsInverseL $ l <+> r in
---       rewrite sym $ semigroupOpIsAssociative (inverse r <+> (inverse l <+> neutral)) l (inverse l <+> neutral) in
---         rewrite semigroupOpIsAssociative l (inverse l) neutral in
---           rewrite groupInverseIsInverseL l in
---             rewrite monoidNeutralIsNeutralL $ the ty neutral in
---               Refl
-
-||| y = z if x + y = x + z
-public export
-cancelLeft : Group ty => (x, y, z : ty) ->
-  x <+> y = x <+> z -> y = z
-cancelLeft x y z p =
-  rewrite sym $ monoidNeutralIsNeutralR y in
-    rewrite sym $ groupInverseIsInverseR x in
-      rewrite sym $ semigroupOpIsAssociative (inverse x) x y in
-        rewrite p in
-      rewrite semigroupOpIsAssociative (inverse x) x z in
-    rewrite groupInverseIsInverseR x in
-  monoidNeutralIsNeutralR z
-
-||| y = z if y + x = z + x.
-public export
-cancelRight : Group ty => (x, y, z : ty) ->
-  y <+> x = z <+> x -> y = z
-cancelRight x y z p =
-  rewrite sym $ monoidNeutralIsNeutralL y in
-    rewrite sym $ groupInverseIsInverseL x in
-      rewrite semigroupOpIsAssociative y x (inverse x) in
-        rewrite p in
-      rewrite sym $ semigroupOpIsAssociative z x (inverse x) in
-    rewrite groupInverseIsInverseL x in
-  monoidNeutralIsNeutralL z
-
-||| ab = 0 -> a = b^-1
-public export
-neutralProductInverseR : Group ty => (a, b : ty) ->
-  a <+> b = neutral {ty} -> a = inverse b
-neutralProductInverseR a b prf =
-  cancelRight  b a (inverse b) $
-    trans prf $ sym $ groupInverseIsInverseR b
-
-||| ab = 0 -> a^-1 = b
-public export
-neutralProductInverseL : Group ty => (a, b : ty) ->
-  a <+> b = neutral {ty} -> 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.
-public export
-latinSquareProperty : Group ty => (a, b : ty) ->
-  ((x : ty ** a <+> x = b),
-    (y : ty ** y <+> a = b))
-latinSquareProperty a b =
-  ((((inverse a) <+> b) **
-    rewrite semigroupOpIsAssociative a (inverse a) b in
-      rewrite groupInverseIsInverseL a in
-        monoidNeutralIsNeutralR b),
-  (b <+> (inverse a) **
-    rewrite sym $ semigroupOpIsAssociative b (inverse a) a in
-      rewrite groupInverseIsInverseR a in
-        monoidNeutralIsNeutralL b))
-
-||| For any a, b, x, the solution to ax = b is unique.
-public export
-uniqueSolutionR : Group ty => (a, b, x, y : ty) ->
-  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.
-public export
-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
--- public export
--- inverseDistributesOverGroupOp : AbelianGroup ty => (l, r : ty) ->
---   inverse (l <+> r) = inverse l <+> inverse r
--- inverseDistributesOverGroupOp l r =
---   rewrite groupOpIsCommutative (inverse l) (inverse r) in
---     inverseOfSum l r
-
-||| Homomorphism preserves neutral.
-public export
-homoNeutral : GroupHomomorphism a b =>
-  to (neutral {ty=a}) = neutral {ty=b}
-homoNeutral =
-  selfSquareId (to neutral) $
-    trans (sym $ toGroup neutral neutral) $
-      cong to $ monoidNeutralIsNeutralL neutral
-
-||| Homomorphism preserves inverses.
-public export
-homoInverse : GroupHomomorphism a b => (x : a) ->
-  the b (to $ inverse x) = the b (inverse $ to x)
-homoInverse x =
-  cancelRight (to x) (to $ inverse x) (inverse $ to x) $
-    trans (sym $ toGroup (inverse x) x) $
-      trans (cong to $ groupInverseIsInverseR x) $
-        trans homoNeutral $
-          sym $ groupInverseIsInverseR (to x)
-
--- Rings
-
-||| 0x = x
-public export
-multNeutralAbsorbingL : Ring ty => (r : ty) ->
-  neutral {ty} <.> r = neutral {ty}
-multNeutralAbsorbingL {ty} r =
-  rewrite sym $ monoidNeutralIsNeutralR $ neutral <.> r in
-    rewrite sym $ groupInverseIsInverseR $ neutral <.> r in
-  rewrite sym $ semigroupOpIsAssociative (inverse $ neutral <.> r) (neutral <.> r) (((inverse $ neutral <.> r) <+> (neutral <.> r)) <.> r) in
-    rewrite groupInverseIsInverseR $ neutral <.> r in
-  rewrite sym $ ringOpIsDistributiveR neutral neutral r in
-    rewrite monoidNeutralIsNeutralR $ the ty neutral in
-  groupInverseIsInverseR $ neutral <.> r
-
-||| x0 = 0
-public export
-multNeutralAbsorbingR : Ring ty => (l : ty) ->
-  l <.> neutral {ty} = neutral {ty}
-multNeutralAbsorbingR {ty} l =
-  rewrite sym $ monoidNeutralIsNeutralL $ l <.> neutral in
-    rewrite sym $ groupInverseIsInverseL $ l <.> neutral in
-  rewrite semigroupOpIsAssociative (l <.> ((l <.> neutral) <+> (inverse $ l <.> neutral))) (l <.> neutral) (inverse $ l <.> neutral) in
-    rewrite groupInverseIsInverseL $ l <.> neutral in
-  rewrite sym $ ringOpIsDistributiveL l neutral neutral in
-    rewrite monoidNeutralIsNeutralL $ the ty neutral in
-  groupInverseIsInverseL $ l <.> neutral
-
-||| (-x)y = -(xy)
-public export
-multInverseInversesL : Ring ty => (l, r : ty) ->
-  inverse l <.> r = inverse (l <.> r)
-multInverseInversesL l r =
-  rewrite sym $ monoidNeutralIsNeutralR $ inverse l <.> r in
-    rewrite sym $ groupInverseIsInverseR $ l <.> r in
-      rewrite sym $ semigroupOpIsAssociative (inverse $ l <.> r) (l <.> r) (inverse l <.> r) in
-  rewrite sym $ ringOpIsDistributiveR l (inverse l) r in
-    rewrite groupInverseIsInverseL l in
-  rewrite multNeutralAbsorbingL r in
-    monoidNeutralIsNeutralL $ inverse $ l <.> r
-
-||| x(-y) = -(xy)
-public export
-multInverseInversesR : Ring ty => (l, r : ty) ->
-  l <.> inverse r = inverse (l <.> r)
-multInverseInversesR l r =
-  rewrite sym $ monoidNeutralIsNeutralL $ l <.> (inverse r) in
-    rewrite sym $ groupInverseIsInverseL (l <.> r) in
-      rewrite semigroupOpIsAssociative (l <.> (inverse r)) (l <.> r) (inverse $ l <.> r) in
-  rewrite sym $ ringOpIsDistributiveL l (inverse r) r in
-    rewrite groupInverseIsInverseR r in
-  rewrite multNeutralAbsorbingR l in
-    monoidNeutralIsNeutralR $ inverse $ l <.> r
-
-||| (-x)(-y) = xy
-public export
-multNegativeByNegativeIsPositive : Ring ty => (l, r : ty) ->
-  inverse l <.> inverse r = l <.> r
-multNegativeByNegativeIsPositive l r =
-    rewrite multInverseInversesR (inverse l) r in
-    rewrite sym $ multInverseInversesL (inverse l) r in
-    rewrite inverseSquaredIsIdentity l in
-    Refl
-
-||| (-1)x = -x
-public export
-inverseOfUnityR : RingWithUnity ty => (x : ty) ->
-  inverse (unity {ty}) <.> x = inverse x
-inverseOfUnityR x =
-  rewrite multInverseInversesL unity x in
-    rewrite unityIsRingIdR x in
-      Refl
-
-||| x(-1) = -x
-public export
-inverseOfUnityL : RingWithUnity ty => (x : ty) ->
-  x <.> inverse (unity {ty}) = inverse x
-inverseOfUnityL x =
-  rewrite multInverseInversesR x unity in
-    rewrite unityIsRingIdL x in
-      Refl
diff --git a/libs/contrib/Control/Monad/Algebra.idr b/libs/contrib/Control/Monad/Algebra.idr
deleted file mode 100644
index 82189bf249..0000000000
--- a/libs/contrib/Control/Monad/Algebra.idr
+++ /dev/null
@@ -1,18 +0,0 @@
-module Control.Monad.Algebra
-
-import Control.Algebra
-import Control.Monad.Identity
-
-%default total
-
-public export
-SemigroupV ty => SemigroupV (Identity ty) where
-  semigroupOpIsAssociative (Id l) (Id c) (Id r) =
-    rewrite semigroupOpIsAssociative l c r in Refl
-
-public export
-MonoidV ty => MonoidV (Identity ty) where
-  monoidNeutralIsNeutralL (Id l) =
-    rewrite monoidNeutralIsNeutralL l in Refl
-  monoidNeutralIsNeutralR (Id r) =
-    rewrite monoidNeutralIsNeutralR r in Refl
diff --git a/libs/contrib/Data/Bool/Algebra.idr b/libs/contrib/Data/Bool/Algebra.idr
deleted file mode 100644
index 4321d347c9..0000000000
--- a/libs/contrib/Data/Bool/Algebra.idr
+++ /dev/null
@@ -1,77 +0,0 @@
-module Data.Bool.Algebra
-
-import Control.Algebra
-import Data.Bool.Xor
-
-%default total
-
--- && is Bool -> Lazy Bool -> Bool,
--- but Bool -> Bool -> Bool is required
-and : Bool -> Bool -> Bool
-and True True = True
-and _ _ = False
-
-Semigroup Bool where
-  (<+>) = xor
-
-SemigroupV Bool where
-  semigroupOpIsAssociative = xorAssociative
-
-Monoid Bool where
-  neutral = False
-
-MonoidV Bool where
-  monoidNeutralIsNeutralL True = Refl
-  monoidNeutralIsNeutralL False = Refl
-
-  monoidNeutralIsNeutralR True = Refl
-  monoidNeutralIsNeutralR False = Refl
-
-Group Bool where
-  -- Each Bool is its own additive inverse.
-  inverse = id
-
-  groupInverseIsInverseR True = Refl
-  groupInverseIsInverseR False = Refl
-
-AbelianGroup Bool where
-  groupOpIsCommutative = xorCommutative
-
-Ring Bool where
-  (<.>) = and
-
-  ringOpIsAssociative True True True = Refl
-  ringOpIsAssociative True True False = Refl
-  ringOpIsAssociative True False True = Refl
-  ringOpIsAssociative True False False = Refl
-  ringOpIsAssociative False True True = Refl
-  ringOpIsAssociative False False True = Refl
-  ringOpIsAssociative False True False = Refl
-  ringOpIsAssociative False False False = Refl
-
-  ringOpIsDistributiveL True True True = Refl
-  ringOpIsDistributiveL True True False = Refl
-  ringOpIsDistributiveL True False True = Refl
-  ringOpIsDistributiveL True False False = Refl
-  ringOpIsDistributiveL False True True = Refl
-  ringOpIsDistributiveL False False True = Refl
-  ringOpIsDistributiveL False True False = Refl
-  ringOpIsDistributiveL False False False = Refl
-
-  ringOpIsDistributiveR True True True = Refl
-  ringOpIsDistributiveR True True False = Refl
-  ringOpIsDistributiveR True False True = Refl
-  ringOpIsDistributiveR True False False = Refl
-  ringOpIsDistributiveR False True True = Refl
-  ringOpIsDistributiveR False False True = Refl
-  ringOpIsDistributiveR False True False = Refl
-  ringOpIsDistributiveR False False False = Refl
-
-RingWithUnity Bool where
-  unity = True
-
-  unityIsRingIdL True = Refl
-  unityIsRingIdL False = Refl
-
-  unityIsRingIdR True = Refl
-  unityIsRingIdR False = Refl
diff --git a/libs/contrib/Data/List/Algebra.idr b/libs/contrib/Data/List/Algebra.idr
deleted file mode 100644
index c190dbb217..0000000000
--- a/libs/contrib/Data/List/Algebra.idr
+++ /dev/null
@@ -1,15 +0,0 @@
-module Data.List.Algebra
-
-import Control.Algebra
-import Data.List
-
-%default total
-
-public export
-SemigroupV (List ty) where
-  semigroupOpIsAssociative = appendAssociative
-
-public export
-MonoidV (List ty) where
-  monoidNeutralIsNeutralL = appendNilRightNeutral
-  monoidNeutralIsNeutralR _ = Refl
diff --git a/libs/contrib/Data/Morphisms/Algebra.idr b/libs/contrib/Data/Morphisms/Algebra.idr
deleted file mode 100644
index 39c385a473..0000000000
--- a/libs/contrib/Data/Morphisms/Algebra.idr
+++ /dev/null
@@ -1,15 +0,0 @@
-module Data.Morphisms.Algebra
-
-import Control.Algebra
-import Data.Morphisms
-
-%default total
-
-public export
-SemigroupV (Endomorphism ty) where
-  semigroupOpIsAssociative (Endo _) (Endo _) (Endo _) = Refl
-
-public export
-MonoidV (Endomorphism ty) where
-  monoidNeutralIsNeutralL (Endo _) = Refl
-  monoidNeutralIsNeutralR (Endo _) = Refl
diff --git a/libs/contrib/Data/Nat/Algebra.idr b/libs/contrib/Data/Nat/Algebra.idr
deleted file mode 100644
index 3b19e2bbf7..0000000000
--- a/libs/contrib/Data/Nat/Algebra.idr
+++ /dev/null
@@ -1,19 +0,0 @@
-module Data.Nat.Algebra
-
-import Control.Algebra
-import Data.Nat
-
-%default total
-
-namespace SemigroupV
-
-  public export
-  [Additive] SemigroupV Nat using Semigroup.Additive where
-    semigroupOpIsAssociative = plusAssociative
-
-namespace MonoidV
-
-  public export
-  [Additive] MonoidV Nat using Monoid.Additive SemigroupV.Additive where
-    monoidNeutralIsNeutralL = plusZeroRightNeutral
-    monoidNeutralIsNeutralR = plusZeroLeftNeutral
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index b02d1dee94..5454957a37 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -9,12 +9,6 @@ modules = Control.ANSI,
 
           Control.Delayed,
 
-          Control.Monad.Algebra,
-
-          Control.Algebra,
-          Control.Algebra.Laws,
-          Control.Algebra.Implementations,
-
           Control.Arrow,
           Control.Category,
 
@@ -23,8 +17,6 @@ modules = Control.ANSI,
           Data.Binary.Digit,
           Data.Binary,
 
-          Data.Bool.Algebra,
-
           Data.Fin.Extra,
 
           Data.Fun.Extra,
@@ -40,7 +32,6 @@ modules = Control.ANSI,
 
           Data.Linear.Array,
 
-          Data.List.Algebra,
           Data.List.TailRec,
           Data.List.Equalities,
           Data.List.Extra,
@@ -56,9 +47,6 @@ modules = Control.ANSI,
 
           Data.Monoid.Exponentiation,
 
-          Data.Morphisms.Algebra,
-
-          Data.Nat.Algebra,
           Data.Nat.Ack,
           Data.Nat.Division,
           Data.Nat.Equational,