diff --git a/Data/Manifold/PseudoAffine.hs b/Data/Manifold/PseudoAffine.hs
--- a/Data/Manifold/PseudoAffine.hs
+++ b/Data/Manifold/PseudoAffine.hs
@@ -55,6 +55,7 @@
             , Semimanifold(..), Needle'
             , PseudoAffine(..)
             , LinearManifold, ScalarManifold
+            , Num', RealFrac', RealFloat'
             , Num'', RealFrac'', RealFloat''
             -- * Type definitions
             -- ** Needles
@@ -327,26 +328,31 @@
   coerceNeedle' _ = LinearFunction $ \(V4 x y z w) -> ((x,y),(z,w))
 
 
-instance ( Semimanifold a, Semimanifold b, Semimanifold c
+instance ∀ a b c .
+         ( Semimanifold a, Semimanifold b, Semimanifold c
          , LSpace (Needle a), LSpace (Needle b), LSpace (Needle c)
          , Scalar (Needle a) ~ Scalar (Needle b), Scalar (Needle b) ~ Scalar (Needle c)
-         , Scalar (Needle' a) ~ Scalar (Needle a), Scalar (Needle' b) ~ Scalar (Needle b)
-         , Scalar (Needle' c) ~ Scalar (Needle c) )
+         )
      => LocallyCoercible (a,(b,c)) ((a,b),c) where
   locallyTrivialDiffeomorphism = regroup
   coerceNeedle _ = regroup
-  coerceNeedle' _ = regroup
+  coerceNeedle' _ = case ( dualSpaceWitness @(Needle a)
+                         , dualSpaceWitness @(Needle b)
+                         , dualSpaceWitness @(Needle c) ) of
+     (DualSpaceWitness, DualSpaceWitness, DualSpaceWitness) -> regroup
   oppositeLocalCoercion = CanonicalDiffeomorphism
 instance ∀ a b c .
          ( Semimanifold a, Semimanifold b, Semimanifold c
          , LSpace (Needle a), LSpace (Needle b), LSpace (Needle c)
          , Scalar (Needle a) ~ Scalar (Needle b), Scalar (Needle b) ~ Scalar (Needle c)
-         , Scalar (Needle' a) ~ Scalar (Needle a), Scalar (Needle' b) ~ Scalar (Needle b)
-         , Scalar (Needle' c) ~ Scalar (Needle c)  )
+         )
      => LocallyCoercible ((a,b),c) (a,(b,c)) where
   locallyTrivialDiffeomorphism = regroup'
   coerceNeedle _ = regroup'
-  coerceNeedle' _ = regroup'
+  coerceNeedle' _ = case ( dualSpaceWitness @(Needle a)
+                         , dualSpaceWitness @(Needle b)
+                         , dualSpaceWitness @(Needle c) ) of
+     (DualSpaceWitness, DualSpaceWitness, DualSpaceWitness) -> regroup'
   oppositeLocalCoercion = CanonicalDiffeomorphism
 
 
diff --git a/Data/Manifold/TreeCover.hs b/Data/Manifold/TreeCover.hs
--- a/Data/Manifold/TreeCover.hs
+++ b/Data/Manifold/TreeCover.hs
@@ -101,7 +101,8 @@
 import Data.Functor.Identity
 import Control.Monad.Trans.State
 import Control.Monad.Trans.Writer
-import Control.Monad.Trans.List
+import ListT (ListT)
+import qualified ListT
 import Control.Monad.Trans.OuterMaybe
 import Control.Monad.Trans.Class
 import qualified Data.Foldable       as Hask
@@ -226,11 +227,12 @@
                return (i₀, st)
 trunkBranches t = pure (0,t)
   
-directionChoices :: WithField ℝ Manifold x
+directionChoices :: ∀ x y . WithField ℝ Manifold x
                => [DBranch x y]
                  -> [ ( (Needle' x, x`Shaded`y)
                       ,[(Needle' x, x`Shaded`y)] ) ]
-directionChoices = map (snd *** map snd) . directionIChoices 0
+directionChoices = case dualSpaceWitness @(Needle x) of
+   DualSpaceWitness -> map (snd *** map snd) . directionIChoices 0
 
 directionIChoices :: (WithField ℝ PseudoAffine x, AdditiveGroup (Needle' x))
                => Int -> [DBranch x y]
@@ -781,7 +783,7 @@
                                               (wall^.wallID._2.swapped) groups
                                          | wall <- levelWalls ]
                                ]
-               where groups = ($[]) <$> Map.fromListWith (.)
+               where groups = ($ []) <$> Map.fromListWith (.)
                                [ (wall^.wallID._2, (i:))
                                | (i,(_, (gsc,_))) <- zip [n₀..] pts
                                , wall <- takeWhile ((==depth) . fst . _wallID) gsc ]
@@ -845,7 +847,7 @@
               => x`Shaded`y -> LeafyTree x y
 entireTree (PlainLeaves lvs)
     = let (ctr,_) = pseudoECM ([]::[x]) $ NE.fromList lvs
-      in  GenericTree [ (ctr, GenericTree . ListT $ Right
+      in  GenericTree [ (ctr, GenericTree $ ListT.fromFoldable
                                 [ (x, GenericTree . lift $ Left y)
                                 | (x,y)<-lvs ] )
                       ]
@@ -855,7 +857,7 @@
                   , (x, GenericTree subt) <- sub ]
 entireTree (OverlappingBranches _ (Shade ctr _) brs)
     = GenericTree [ ( ctr
-                    , GenericTree . ListT . Right
+                    , GenericTree . ListT.fromFoldable
                        $ Hask.foldMap (Hask.foldMap $ treeBranches . entireTree) brs ) ]
 
 
diff --git a/Data/Manifold/Types.hs b/Data/Manifold/Types.hs
--- a/Data/Manifold/Types.hs
+++ b/Data/Manifold/Types.hs
@@ -13,6 +13,7 @@
 
 {-# LANGUAGE FlexibleInstances        #-}
 {-# LANGUAGE UndecidableInstances     #-}
+{-# LANGUAGE InstanceSigs             #-}
 {-# LANGUAGE CPP                      #-}
 {-# LANGUAGE TypeFamilies             #-}
 {-# LANGUAGE FunctionalDependencies   #-}
@@ -26,6 +27,8 @@
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE PatternGuards            #-}
 {-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE TypeApplications         #-}
+{-# LANGUAGE DataKinds                #-}
 {-# LANGUAGE ScopedTypeVariables      #-}
 {-# LANGUAGE UnicodeSyntax            #-}
 {-# LANGUAGE PatternSynonyms          #-}
@@ -85,15 +88,30 @@
 import Data.Manifold.PseudoAffine
 import Data.Manifold.Cone
 import Math.LinearMap.Category
+#if MIN_VERSION_linearmap_category(0,6,0)
+import Math.VectorSpace.DimensionAware
+#if MIN_VERSION_singletons(3,0,0)
+import Prelude.Singletons (SNum(..))
+import GHC.TypeLits.Singletons (withKnownNat, SNat(..))
+#else
+import Data.Singletons.Prelude.Num (SNum(..), SNat(..))
+import Data.Singletons.TypeLits (withKnownNat)
+#endif
+#endif
+#if MIN_VERSION_linearmap_category(0,5,0)
+import Math.LinearMap.Coercion
+#endif
 
 import qualified Prelude
+import GHC.TypeLits (type (+), type (-))
 import qualified Data.Traversable as Hask
 
-import Control.Category.Constrained.Prelude hiding ((^))
+import Control.Category.Constrained.Prelude hiding ((^), type (+))
 import Control.Arrow.Constrained
 import Control.Monad.Constrained
-import Data.Foldable.Constrained
+import Data.Foldable.Constrained hiding (type (+))
 
+import Data.Coerce
 import Data.Type.Coercion
 
 type StiefelScalar s = (RealFloat s, UArr.Unbox s)
@@ -171,6 +189,30 @@
 
 deriveAffine((FiniteFreeSpace v, UArr.Unbox (Scalar v)), Stiefel1Needle v)
 
+#if MIN_VERSION_linearmap_category(0,6,0)
+type family ClipPred n where
+  ClipPred 0 = 0
+  ClipPred n = n-1
+type family FmapClipPred n where
+  FmapClipPred ('Just n) = 'Just (ClipPred n)
+  FmapClipPred 'Nothing = 'Nothing
+
+clipPredSing :: SNat n -> SNat (ClipPred n)
+clipPredSing _ = undefined
+
+instance ∀ v . (FiniteFreeSpace v, DimensionAware v, UArr.Unbox (Scalar v))
+              => DimensionAware (Stiefel1Needle v) where
+  type StaticDimension (Stiefel1Needle v) = FmapClipPred (StaticDimension v) 
+  dimensionalityWitness = case dimensionalityWitness @v of
+    IsStaticDimensional -> withKnownNat (clipPredSing $ dimensionalitySing @v)
+                             IsStaticDimensional
+    IsFlexibleDimensional -> IsFlexibleDimensional
+instance ∀ v n n' . ( FiniteFreeSpace v, n`Dimensional`v, n' ~ ClipPred n
+                    , UArr.Unbox (Scalar v) )
+              => n'`Dimensional`(Stiefel1Needle v) where
+  knownDimensionalitySing = clipPredSing (dimensionalitySing @v)
+#endif
+
 instance ∀ v . (LSpace v, FiniteFreeSpace v, Eq (Scalar v), UArr.Unbox (Scalar v))
               => TensorSpace (Stiefel1Needle v) where
   type TensorProduct (Stiefel1Needle v) w = Array w
@@ -193,13 +235,13 @@
   fmapTensor = bilinearFunction $ \f (Tensor a) -> Tensor $ Arr.map (f$) a
   fzipTensorWith = bilinearFunction $ \f (Tensor a, Tensor b)
                      -> Tensor $ Arr.zipWith (curry $ arr f) a b
-  coerceFmapTensorProduct _ Coercion = Coercion
+#if MIN_VERSION_linearmap_category(0,6,0)
+  coerceFmapTensorProduct _ VSCCoercion = Coercion
+#elif MIN_VERSION_linearmap_category(0,5,0)
+  coerceFmapTensorProduct _ VSCCoercion = VSCCoercion
+#endif
   wellDefinedTensor (Tensor a) = Tensor <$> Hask.traverse wellDefinedVector a
 
-asTensor :: Coercion (LinearMap s a b) (Tensor s (DualVector a) b)
-asTensor = Coercion
-asLinearMap :: Coercion (Tensor s (DualVector a) b) (LinearMap s a b)
-asLinearMap = Coercion
 infixr 0 +$>
 (+$>) :: (LinearSpace a, TensorSpace b, Scalar a ~ s, Scalar b ~ s)
             => LinearMap s a b -> a -> b
@@ -216,11 +258,15 @@
            => DualSpaceWitness w -> (Stiefel1Needle v ⊗ w) +> (Stiefel1Needle v ⊗ w)
          ti DualSpaceWitness = LinearMap . Arr.generate d
            $ \i -> fmap (LinearFunction $ \w -> Tensor . Arr.generate d $
-              \j -> if i==j then w else zeroV) $ asTensor $ id
+              \j -> if i==j then w else zeroV) $ coerce (id :: w+>w)
          d = freeDimension ([]::[v]) - 1
   dualSpaceWitness = case dualSpaceWitness :: DualSpaceWitness v of
          DualSpaceWitness -> DualSpaceWitness
+#if MIN_VERSION_linearmap_category(0,5,0)
+  coerceDoubleDual = VSCCoercion
+#else
   coerceDoubleDual = Coercion
+#endif
   contractTensorMap = LinearFunction $ \(LinearMap m)
                         -> Arr.ifoldl' (\acc i (Tensor t) -> acc ^+^ t Arr.! i) zeroV m
   contractMapTensor = LinearFunction $ \(Tensor m)
@@ -234,8 +280,14 @@
                         -> Arr.ifoldl' (\acc i w -> acc ^+^ v UArr.! i *^ w) zeroV m
   applyTensorFunctional = bilinearFunction $ \(LinearMap f) (Tensor t)
                            -> Arr.ifoldl' (\acc i u -> acc + u <.>^ t Arr.! i) 0 f
-  applyTensorLinMap = bilinearFunction $ \(LinearMap f) (Tensor t)
-         -> Arr.ifoldl' (\w i u -> w ^+^ ((asLinearMap $ f Arr.! i) +$> u)) zeroV t
+  applyTensorLinMap :: ∀ u w . ( LinearSpace u, Scalar u ~ Scalar v
+                               , TensorSpace w, Scalar w ~ Scalar v )
+    => Bilinear (LinearMap (Scalar v) (Tensor (Scalar v) (Stiefel1Needle v) u) w)
+               (Tensor (Scalar v) (Stiefel1Needle v) u)
+               w
+  applyTensorLinMap = case dualSpaceWitness @u of
+     DualSpaceWitness -> bilinearFunction $ \(LinearMap f) (Tensor t)
+         -> Arr.ifoldl' (\w i u -> w ^+^ ((coerce $ f Arr.! i) +$> u)) zeroV t
   composeLinear = bilinearFunction $ \f (LinearMap g)
                      -> LinearMap $ Arr.map (getLinearFunction applyLinear f$) g
   useTupleLinearSpaceComponents _ = undefined
diff --git a/Data/Manifold/Web.hs b/Data/Manifold/Web.hs
--- a/Data/Manifold/Web.hs
+++ b/Data/Manifold/Web.hs
@@ -108,7 +108,6 @@
 import Control.Monad.ST (runST)
 import Data.STRef (newSTRef, modifySTRef, readSTRef)
 import Control.Monad.Trans.State
-import Control.Monad.Trans.List
 import Control.Monad.Trans.Except
 import Control.Monad.Trans.Writer hiding (censor)
 import Data.Functor.Identity (Identity(..))
diff --git a/Data/Manifold/WithBoundary.hs b/Data/Manifold/WithBoundary.hs
--- a/Data/Manifold/WithBoundary.hs
+++ b/Data/Manifold/WithBoundary.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE FlexibleInstances        #-}
 {-# LANGUAGE UndecidableInstances     #-}
 {-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE MultiParamTypeClasses    #-}
 {-# LANGUAGE FlexibleContexts         #-}
 {-# LANGUAGE GADTs                    #-}
 {-# LANGUAGE DefaultSignatures        #-}
@@ -25,6 +26,7 @@
 {-# LANGUAGE LambdaCase               #-}
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE TypeInType               #-}
+{-# LANGUAGE NoStarIsType             #-}
 {-# LANGUAGE CPP                      #-}
 
 
@@ -49,8 +51,21 @@
                                , LinearMap(..), LinearFunction(..), LinearSpace(..)
                                , Num', closedScalarWitness, ClosedScalarWitness(..)
                                , DualSpaceWitness(..), ScalarSpaceWitness(..)
-                               , LinearManifoldWitness(..)
-                               )
+                               , LinearManifoldWitness(..) )
+#if MIN_VERSION_linearmap_category(0,6,0)
+import Math.VectorSpace.DimensionAware
+                ( DimensionAware(..), Dimensional(..), DimensionalityWitness(..)
+                , dimensionality, DimensionalityCases(..)
+                , dimensionalitySing )
+import GHC.TypeLits
+#if MIN_VERSION_singletons(3,0,0)
+import Prelude.Singletons (SNum(..))
+import GHC.TypeLits.Singletons (withKnownNat, SNat(..))
+#else
+import Data.Singletons.Prelude.Num (SNum(..), SNat(..))
+import Data.Singletons.TypeLits (withKnownNat)
+#endif
+#endif
 import Math.VectorSpace.Dual
 import Math.VectorSpace.MiscUtil.MultiConstraints (SameScalar)
 import Data.Monoid.Additive
@@ -70,7 +85,11 @@
 
 
 
-
+interiorSemimanifoldWitness :: ∀ a . SemimanifoldWithBoundary a
+          => SemimanifoldWitness (Interior a)
+interiorSemimanifoldWitness = case smfdWBoundWitness @a of
+  OpenManifoldWitness -> semimanifoldWitness
+  SmfdWBoundWitness -> semimanifoldWitness
 
 #define VectorSpaceSansBoundary(v, s)                         \
 instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
@@ -167,6 +186,49 @@
         NBoundOfL x y v -> NBoundOfL (μ*^x) (μ*^y) (μ*^v)
         NBoundOfR x y v -> NBoundOfR (μ*^x) (μ*^y) (μ*^v)
     ))
+
+#if MIN_VERSION_linearmap_category(0,6,0)
+type family ProductBoundaryNeedleTDimension dna dnb dv where
+  ProductBoundaryNeedleTDimension 
+    ('Just n) ('Just m) ('Just o) = 'Just (n*m*o - 1)
+  ProductBoundaryNeedleTDimension _ _ _ = 'Nothing
+
+instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
+         , SameScalar LinearSpace
+           '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
+         , AdditiveGroup (dn`Space`Needle (Boundary a))
+         , AdditiveGroup (dn`Space`Needle (Boundary b))
+         , ValidDualness dn )
+    => DimensionAware (ProductBoundaryNeedleT dn a b v) where
+  type StaticDimension (ProductBoundaryNeedleT dn a b v)
+          = ProductBoundaryNeedleTDimension (StaticDimension (dn`Space`Needle (Interior a)))
+                                            (StaticDimension (dn`Space`Needle (Interior b)))
+                                            (StaticDimension v)
+  dimensionalityWitness = case ( interiorSemimanifoldWitness @a
+                               , interiorSemimanifoldWitness @b ) of
+      (SemimanifoldWitness, SemimanifoldWitness)
+                -> case ( dimensionality @(dn`Space`Needle (Interior a))
+                        , dimensionality @(dn`Space`Needle (Interior b))
+                        , dimensionality @v ) of
+       (StaticDimensionalCase, StaticDimensionalCase, StaticDimensionalCase)
+            -> withKnownNat (dimensionalitySing @(dn`Space`Needle (Interior a))
+                               %* dimensionalitySing @(dn`Space`Needle (Interior b))
+                               %* dimensionalitySing @v
+                               %- SNat @1
+                            )
+                IsStaticDimensional
+instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
+         , SameScalar LinearSpace
+           '[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
+         , AdditiveGroup (dn`Space`Needle (Boundary a))
+         , AdditiveGroup (dn`Space`Needle (Boundary b))
+         , n`Dimensional`(dn`Space`Needle (Interior a))
+         , m`Dimensional`(dn`Space`Needle (Interior b))
+         , o`Dimensional`v
+         , KnownNat d, d ~ (n*m*o-1)
+         , ValidDualness dn )
+    => d`Dimensional`(ProductBoundaryNeedleT dn a b v) where
+#endif
 
 instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
          , SameScalar LinearSpace
diff --git a/Data/Manifold/WithBoundary/Class.hs b/Data/Manifold/WithBoundary/Class.hs
--- a/Data/Manifold/WithBoundary/Class.hs
+++ b/Data/Manifold/WithBoundary/Class.hs
@@ -61,6 +61,7 @@
 
 type OpenManifold m = ( SemimanifoldWithBoundary m
                       , SemimanifoldWithBoundary (Needle m)
+                      , Semimanifold m
                       , LinearSpace (Needle m)
                       , SemimanifoldWithBoundary (Scalar (Needle m))
                       , Interior m ~ m
diff --git a/Math/Manifold/Homogeneous.hs b/Math/Manifold/Homogeneous.hs
new file mode 100644
--- /dev/null
+++ b/Math/Manifold/Homogeneous.hs
@@ -0,0 +1,185 @@
+-- |
+-- Module      : Math.Manifold.Homogeneous
+-- Copyright   : (c) Justus Sagemüller 2022
+-- License     : GPL v3
+-- 
+-- Maintainer  : (@) jsag $ hvl.no
+-- Stability   : experimental
+-- Portability : portable
+-- 
+
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE UndecidableInstances       #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE DefaultSignatures          #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE ConstraintKinds            #-}
+{-# LANGUAGE UnicodeSyntax              #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE AllowAmbiguousTypes        #-}
+{-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE EmptyCase                  #-}
+{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE TypeInType                 #-}
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE TemplateHaskell            #-}
+
+
+module Math.Manifold.Homogeneous
+    ( LieGroup(..), LieAlgebra, ActsOn(..)
+    , SO
+    ) where
+
+import Data.VectorSpace
+import Data.AffineSpace
+import Data.Basis
+
+import Math.Manifold.Core.PseudoAffine
+import Data.Manifold.PseudoAffine
+import Math.Manifold.Core.Types
+import Data.Manifold.Types.Primitive
+import Math.Manifold.VectorSpace.ZeroDimensional
+import Math.LinearMap.Category
+import Math.VectorSpace.Dual
+import Data.Complex as ℂ
+import Linear (V0, V1, V2, V3(..), V4, Quaternion(..), cross)
+import qualified Linear.Affine as LinAff
+import Data.Monoid.Additive
+
+import Prelude hiding (($), (^))
+import Control.Arrow.Constrained ((<<<), ($))
+import Control.Applicative
+
+import Data.Semigroup hiding (Dual)
+
+import qualified Test.QuickCheck as QC
+
+import Data.Kind (Type)
+import GHC.TypeLits (Nat)
+import Data.Coerce
+import Data.Type.Coercion
+
+
+newtype LieAlgebra g
+    = LieAlgebra { getLieNeedle :: Needle g }
+
+copyNewtypeInstances [t| ∀ g . (Semimanifold g) => LieAlgebra g |]
+    [''AdditiveGroup]
+
+
+
+-- | Manifolds with a continuous group structure, whose 'Needle' space
+--   is isomorphic to the associated Lie algebra.
+--
+--   Laws:
+--
+--   @
+--   expMap zeroV ≡ mempty
+--   lieBracket w v ≡ negateV (lieBracket v w)
+--   ...
+--   @
+class (Semimanifold g, Monoid g) => LieGroup g where
+  expMap :: LieAlgebra g -> g
+  lieBracket :: Bilinear (LieAlgebra g) (LieAlgebra g) (LieAlgebra g)
+
+
+data family SO_ (n :: Nat) (r :: Type)
+
+type SO n = SO_ n Double
+
+data instance SO_ 1 r = SO1Identity
+ deriving (Eq, Show)
+
+instance (QC.Arbitrary r, Floating r) => QC.Arbitrary (SO_ 1 r) where
+  arbitrary = pure SO1Identity
+
+instance Semigroup (SO_ 1 r) where
+  SO1Identity <> SO1Identity = SO1Identity
+instance Monoid (SO_ 1 r) where
+  mempty = SO1Identity
+  mappend = (<>)
+
+instance RealFloat' r => Semimanifold (SO_ 1 r) where
+  type Needle (SO_ 1 r) = ZeroDim r
+  SO1Identity .+~^ Origin = SO1Identity
+  semimanifoldWitness = case linearManifoldWitness @r of
+    LinearManifoldWitness -> SemimanifoldWitness
+
+newtype instance SO_ 2 r = SO2 { unitReprSO2 :: Complex r }
+ deriving (Eq, Show)
+
+instance (QC.Arbitrary r, Floating r) => QC.Arbitrary (SO_ 2 r) where
+  arbitrary = SO2 . ℂ.cis <$> QC.arbitrary
+
+instance RealFloat r => Semigroup (SO_ 2 r) where
+  SO2 a <> SO2 b = SO2 $ a*b  -- perhaps should normalize?
+instance RealFloat r => Monoid (SO_ 2 r) where
+  mempty = SO2 1
+  mappend = (<>)
+
+instance RealFloat' r => Semimanifold (SO_ 2 r) where
+  type Needle (SO_ 2 r) = r
+  p .+~^ d = p <> expMap (LieAlgebra d)
+  semimanifoldWitness = case linearManifoldWitness @r of
+    LinearManifoldWitness -> SemimanifoldWitness
+
+instance RealFloat' r => LieGroup (SO_ 2 r) where
+  expMap = SO2 . cis . getLieNeedle
+  lieBracket = zeroV
+
+
+newtype instance SO_ 3 r = SO3 { unitReprSO3 :: Quaternion r }
+ deriving (Eq, Show)
+
+instance (QC.Arbitrary r, RealFloat r) => QC.Arbitrary (SO_ 3 r) where
+  arbitrary = do
+    (a,b,c,d) <- QC.arbitrary
+    pure . SO3 $ case sqrt . sum $ (^2)<$>[a,b,c,d] of
+      l | l>0       -> Quaternion (a/l) (V3 b c d ^/ l)
+        | otherwise -> 1
+
+instance RealFloat r => Semigroup (SO_ 3 r) where
+  SO3 a <> SO3 b = SO3 $ a*b  -- perhaps should normalize?
+instance RealFloat r => Monoid (SO_ 3 r) where
+  mempty = SO3 1
+  mappend = (<>)
+
+instance RealFloat' r => Semimanifold (SO_ 3 r) where
+  type Needle (SO_ 3 r) = V3 r
+  p .+~^ d = p <> expMap (LieAlgebra d)
+  semimanifoldWitness = case linearManifoldWitness @r of
+    LinearManifoldWitness -> SemimanifoldWitness
+
+instance ∀ r . RealFloat' r => LieGroup (SO_ 3 r) where
+  expMap (LieAlgebra a) = SO3 . exp $ Quaternion 0 a
+  lieBracket = coerce (cross :: V3 r -> V3 r -> V3 r)
+
+embedPureImagUnitQuaternion :: RealFloat r => S²_ r -> Quaternion r
+embedPureImagUnitQuaternion = Quaternion 0 . embed
+
+projectPureImagUnitQuaternion :: RealFloat r => Quaternion r -> S²_ r
+projectPureImagUnitQuaternion (Quaternion _ p) = coEmbed p
+
+-- | Manifolds that are homogeneous with respect to action by a Lie group.
+--   Laws:
+--
+--   @
+--   action mempty ≡ id                  (Identity)
+--   action (a<>b) ≡ action a . action b (Compatibility)
+--   @
+class (Semimanifold m, LieGroup g) => g `ActsOn` m where
+  action :: g -> m -> m
+
+instance RealFloat' r => SO_ 2 r`ActsOn`S¹_ r where
+  action (SO2 β) p = p .+~^ ℂ.phase β
+
+instance RealFloat' r => SO_ 3 r`ActsOn`S²_ r where
+  action (SO3 γ) p = projectPureImagUnitQuaternion $ γ * α * recip γ
+   where α = embedPureImagUnitQuaternion p
+
diff --git a/manifolds.cabal b/manifolds.cabal
--- a/manifolds.cabal
+++ b/manifolds.cabal
@@ -1,5 +1,5 @@
 Name:                manifolds
-Version:             0.6.0.0
+Version:             0.6.1.0
 Category:            Math
 Synopsis:            Coordinate-free hypersurfaces
 Description:         Manifolds, a generalisation of the notion of &#x201c;smooth curves&#x201d; or surfaces,
@@ -34,13 +34,19 @@
                      images/examples/TreesAndWebs/*.png
                      images/examples/DiffableFunction-plots/*.png
 
+flag staticDimensionalLinmapCategory
+  description: Whether to use linearmap-category-0.6 with its fixed-dimension classes.
+               This requires also the singletons package.
+  default: True
+  manual: False
+
 Source-Repository head
     type: git
     location: git://github.com/leftaroundabout/manifolds.git
 
 Library
   Build-Depends:     base>=4.5 && < 6
-                     , manifolds-core == 0.6.0.0
+                     , manifolds-core == 0.6.1.0
                      , transformers
                      , vector-space>=0.8
                      , free-vector-spaces>=0.1.5
@@ -48,7 +54,7 @@
                      , linear
                      , MemoTrie
                      , vector
-                     , linearmap-category >= 0.4.2.0 && < 0.5
+                     , linearmap-category >= 0.4.3.0 && < 0.7
                      , spatial-rotations >= 0.1 && < 0.2
                      , containers
                      , array
@@ -57,6 +63,7 @@
                      , free
                      , semigroups
                      , void
+                     , list-t >=1.0 && <1.1
                      , number-show >= 0.1 && < 0.2
                      , ieee754 >= 0.8 && < 1
                      , tagged
@@ -68,6 +75,14 @@
                      , constrained-categories >= 0.3.1 && < 0.5
                      , pragmatic-show
                      , QuickCheck >=2.8 && <3
+  if flag(staticDimensionalLinmapCategory)
+    build-depends:
+                       linearmap-category >=0.6
+                     , singletons >=3.0 && <3.3
+                     , singletons-base >=3.0 && <3.3
+  else
+    build-depends:
+                       linearmap-category <0.6
   other-extensions:  FlexibleInstances
                      , TypeFamilies
                      , FlexibleContexts
@@ -101,6 +116,7 @@
                      Data.Manifold.Riemannian
                      Math.Manifold.Real.Coordinates
                      Math.Manifold.Embedding.Simple.Class
+                     Math.Manifold.Homogeneous
   Other-modules:   Data.List.FastNub
                    Data.Manifold.Types.Primitive
                    Data.Manifold.WithBoundary.Class
diff --git a/test/tasty/test.hs b/test/tasty/test.hs
--- a/test/tasty/test.hs
+++ b/test/tasty/test.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE OverloadedLists, TypeFamilies, FlexibleContexts, UndecidableInstances #-}
 {-# LANGUAGE FlexibleInstances, AllowAmbiguousTypes  #-}
 {-# LANGUAGE TypeOperators, TypeApplications, ScopedTypeVariables, UnicodeSyntax #-}
+{-# LANGUAGE DataKinds #-}
 
 module Main where
 
@@ -23,6 +24,7 @@
 import Data.Manifold.Web.Internal
 import Data.Manifold.Function.LocalModel
 import Math.Manifold.Embedding.Simple.Class
+import Math.Manifold.Homogeneous
 import Data.VectorSpace
 import Data.Cross (cross3)
 import Linear.V2 (V2(V2))
@@ -198,6 +200,25 @@
   , QC.testProperty "Undo – arbitrary axis / angle and points in 𝑇S²."
            $ \ax ψ p -> rotateAboutThenUndo @(TangentBundle S²) ax ψ p ≈ p
   ]
+ , testGroup "Homogeneous spaces"
+  $ let lieGroupTests :: ∀ m g . ( g`ActsOn`m
+                                 , QC.Arbitrary m
+                                 , AEq m, Show m, SP.Show m
+                                 , QC.Arbitrary g, Show g )
+           => String -> TestTree
+        lieGroupTests descr = testGroup descr $
+         [ QC.testProperty "`mempty` acts as identity"
+          $ \(p :: m) -> action (mempty :: g) p ?≈! p
+         , QC.testProperty "There are non-identic elements" -- This is strictly speaking
+          . QC.expectFailure                                -- not true for all homogeneous
+          $ \a (p :: m) -> action (a :: g) p ?≈! p          -- spaces, but the trivial
+                                                            -- ones don't need testing.
+         , QC.testProperty "Compatibility of action"
+          $ \a b (p :: m) -> action (a<>b :: g) p ?≈! action a (action b p)
+         ]
+    in [ lieGroupTests @S¹ @(SO 2) "SO(2) acting on S¹"
+       , lieGroupTests @S² @(SO 3) "SO(3) acting on S²"
+       ]
  , testGroup "Coordinates"
   [ testGroup "Single dimension"
    [ QC.testProperty "Access" $ \x -> x^.xCoord ≈ x