@@ -156,10 +156,6 @@ VerifiedRingWithUnity ZZ where
156156 ringWithUnityIsUnityL = multOneRightNeutralZ
157157 ringWithUnityIsUnityR = multOneLeftNeutralZ
158158
159−--interface (VerifiedRingWithUnity a, Field a) => VerifiedField a where
160−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = Algebra.neutral)) -> l <.> (inverseM l notId) = Algebra.unity
161−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = Algebra.neutral)) -> (inverseM r notId) <.> r = Algebra.unity
162−
163159interface JoinSemilattice a => VerifiedJoinSemilattice a where
164160 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
165161 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
@@ -169,31 +165,3 @@ interface MeetSemilattice a => VerifiedMeetSemilattice a where
169165 total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
170166 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
171167 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
172−
173−{- FIXME: Some maintenance required here.
174− Algebra.top and Algebra.bottom don't exist!
175−-}
176−{-
177−
178−interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
179− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e
180−
181−interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
182− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e Algebra.top = e
183−
184−interface (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
185− total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
186− total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
187−
188−interface (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
189−
190−
191−--interface (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
192−-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
193−-- total moduleScalarUnityIsUnity : (v : b) -> Algebra.unity {a} <#> v = v
194−-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
195−-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
196−
197−--interface (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
198−
199−-}