diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Change Log
 
+## 0.5
+
+* Switch to lattices-2
+
 ## 0.4.2
 
 * Allow a wide range of dynamically sorted values (not just expressions)
diff --git a/expressions.cabal b/expressions.cabal
--- a/expressions.cabal
+++ b/expressions.cabal
@@ -1,5 +1,5 @@
 name:                expressions
-version:             0.4.2
+version:             0.5
 synopsis:            Expressions and Formulae a la carte
 description:
   This package is aimed at providing means of fixing a first-order language and
@@ -74,7 +74,7 @@
                        base >=4.11 && <4.13,
                        containers >=0.5.7 && <0.7,
                        free >=4.2 && <5.2,
-                       lattices >=1.6 && <1.8,
+                       lattices >=2 && <2.1,
                        singletons >=2.2 && <2.6,
                        text >=1.2 && <1.3,
                        transformers >=0.5.2 && <0.6
diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs
--- a/src/Data/Expression.hs
+++ b/src/Data/Expression.hs
@@ -58,9 +58,6 @@
                        , QFALia
                        , ALia
 
-                       -- Algebraic view of languages
-                       , ComplementedLattice(..)
-
                        -- Convenient type synonyms
                        , VariableName
 
@@ -124,6 +121,7 @@
                        , Unstore
                        , unstore ) where
 
+import Algebra.Heyting
 import Algebra.Lattice
 import Control.Applicative hiding (Const)
 import Control.Comonad.Trans.Coiter
@@ -191,31 +189,28 @@
 -- | A language obtained as fixpoint of `ALiaF`
 type   ALia  = IFix   ALiaF
 
--- | Bounded lattices that support complementing elements
---
--- prop> complement . complement = id
--- 
-class BoundedLattice a => ComplementedLattice a where
-    complement :: a -> a
 
-instance JoinSemiLattice (QFLogic 'BooleanSort) where a `join` b = a .|. b
-instance JoinSemiLattice (QFLia   'BooleanSort) where a `join` b = a .|. b
-instance JoinSemiLattice (  Lia   'BooleanSort) where a `join` b = a .|. b
-instance JoinSemiLattice (QFALia  'BooleanSort) where a `join` b = a .|. b
-instance JoinSemiLattice (  ALia  'BooleanSort) where a `join` b = a .|. b
+instance Lattice (QFLogic 'BooleanSort) where
+    a /\ b = a .&. b
+    a \/ b = a .|. b
 
-instance MeetSemiLattice (QFLogic 'BooleanSort) where a `meet` b = a .&. b
-instance MeetSemiLattice (QFLia   'BooleanSort) where a `meet` b = a .&. b
-instance MeetSemiLattice (  Lia   'BooleanSort) where a `meet` b = a .&. b
-instance MeetSemiLattice (QFALia  'BooleanSort) where a `meet` b = a .&. b
-instance MeetSemiLattice (  ALia  'BooleanSort) where a `meet` b = a .&. b
+instance Lattice (QFLia   'BooleanSort) where
+    a /\ b = a .&. b
+    a \/ b = a .|. b
 
-instance Lattice (QFLogic 'BooleanSort)
-instance Lattice (QFLia   'BooleanSort)
-instance Lattice (  Lia   'BooleanSort)
-instance Lattice (QFALia  'BooleanSort)
-instance Lattice (  ALia  'BooleanSort)
+instance Lattice (  Lia   'BooleanSort) where
+    a /\ b = a .&. b
+    a \/ b = a .|. b
 
+instance Lattice (QFALia  'BooleanSort) where
+    a /\ b = a .&. b
+    a \/ b = a .|. b
+
+instance Lattice (  ALia  'BooleanSort) where
+    a /\ b = a .&. b
+    a \/ b = a .|. b
+
+
 instance BoundedJoinSemiLattice (QFLogic 'BooleanSort) where bottom = false
 instance BoundedJoinSemiLattice (QFLia   'BooleanSort) where bottom = false
 instance BoundedJoinSemiLattice (  Lia   'BooleanSort) where bottom = false
@@ -228,17 +223,21 @@
 instance BoundedMeetSemiLattice (QFALia  'BooleanSort) where top = true
 instance BoundedMeetSemiLattice (  ALia  'BooleanSort) where top = true
 
-instance BoundedLattice (QFLogic 'BooleanSort)
-instance BoundedLattice (QFLia   'BooleanSort)
-instance BoundedLattice (  Lia   'BooleanSort)
-instance BoundedLattice (QFALia  'BooleanSort)
-instance BoundedLattice (  ALia  'BooleanSort)
+instance Heyting (QFLogic 'BooleanSort) where
+    a ==> b = nnf (not a \/ b)
 
-instance ComplementedLattice (QFLogic 'BooleanSort) where complement = nnf . not
-instance ComplementedLattice (QFLia   'BooleanSort) where complement = nnf . not
-instance ComplementedLattice (  Lia   'BooleanSort) where complement = nnf . not
-instance ComplementedLattice (QFALia  'BooleanSort) where complement = nnf . not
-instance ComplementedLattice (  ALia  'BooleanSort) where complement = nnf . not
+instance Heyting (QFLia   'BooleanSort) where
+    a ==> b = nnf (not a \/ b)
+
+instance Heyting (  Lia   'BooleanSort) where
+    a ==> b = nnf (not a \/ b)
+
+instance Heyting (QFALia  'BooleanSort) where
+    a ==> b = nnf (not a \/ b)
+
+instance Heyting (  ALia  'BooleanSort) where
+    a ==> b = nnf (not a \/ b)
+
 
 -- | Type of names assigned to variables
 type VariableName = String
diff --git a/src/Data/Expression/Array.hs b/src/Data/Expression/Array.hs
--- a/src/Data/Expression/Array.hs
+++ b/src/Data/Expression/Array.hs
@@ -117,8 +117,8 @@
 store :: ( ArrayF :<: f, SingI i, SingI e ) => IFix f ('ArraySort i e) -> IFix f i -> IFix f e -> IFix f ('ArraySort i e)
 store a i v = inject (Store sing sing a i v)
 
-type Array                   f (e :: Sort) (i :: Sort) = IFix f ('ArraySort i e)
-type Index                   f (i :: Sort)             = IFix f i
+type Array f (e :: Sort) (i :: Sort) = IFix f ('ArraySort i e)
+type Index f (i :: Sort)             = IFix f i
 
 newtype ArrayAccess             f (i :: Sort) (e :: Sort) = ArrayAccess             { getAA   :: (Array f e i, Index f i) }            deriving Show via (Array f e i, Index f i)
 newtype DynamicValueArrayAccess f (i :: Sort)             = DynamicValueArrayAccess { getDVAA :: DynamicallySorted (ArrayAccess f i) } deriving Show via (DynamicallySorted (ArrayAccess f i))