diff --git a/Data/Function/Affine.hs b/Data/Function/Affine.hs
--- a/Data/Function/Affine.hs
+++ b/Data/Function/Affine.hs
@@ -22,6 +22,7 @@
 {-# LANGUAGE PatternSynonyms          #-}
 {-# LANGUAGE ViewPatterns             #-}
 {-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE TypeApplications         #-}
 {-# LANGUAGE UnicodeSyntax            #-}
 {-# LANGUAGE MultiWayIf               #-}
 {-# LANGUAGE ScopedTypeVariables      #-}
@@ -47,6 +48,7 @@
 import Data.Tagged
 import Data.Manifold.Types.Primitive
 import Data.Manifold.PseudoAffine
+import Data.Manifold.WithBoundary
 import Data.Manifold.Atlas
 import Data.Embedding
 
@@ -71,16 +73,16 @@
                -> Affine s d c
 
 instance Category (Affine s) where
-  type Object (Affine s) x = ( Manifold x, Interior x ~ x
-                             , Atlas x, LinearSpace (Needle x)
-                             , Scalar (Needle x) ~ s, HasTrie (ChartIndex x) )
+  type Object (Affine s) x = ( Manifold x
+                             , Atlas' x
+                             , Scalar (Needle x) ~ s )
   id = Affine . trie $ chartReferencePoint >>> id &&& const id
   Affine f . Affine g = Affine . trie
       $ \ixa -> case untrie g ixa of
            (b, ða'b) -> case untrie f $ lookupAtlas b of
             (c, ðb'c) -> (c, ðb'c . ða'b)
 
-instance ∀ s . Num' s => Cartesian (Affine s) where
+instance ∀ s . (ScalarManifold s, Eq s) => Cartesian (Affine s) where
   type UnitObject (Affine s) = ZeroDim s
   swap = Affine . trie $ chartReferencePoint >>> swap &&& const swap
   attachUnit = Affine . trie $ chartReferencePoint >>> \a -> ((a,Origin), attachUnit)
@@ -89,32 +91,32 @@
   regroup = Affine . trie $ chartReferencePoint >>> regroup &&& const regroup
   regroup' = Affine . trie $ chartReferencePoint >>> regroup' &&& const regroup'
 
-instance ∀ s . Num' s => Morphism (Affine s) where
+instance ∀ s . (ScalarManifold s, Eq s) => Morphism (Affine s) where
   Affine f *** Affine g = Affine . trie
       $ \(ixα,ixβ) -> case (untrie f ixα, untrie g ixβ) of
             ((fα, ðα'f), (gβ,ðβ'g)) -> ((fα,gβ), ðα'f***ðβ'g)
   
-instance ∀ s . Num' s => PreArrow (Affine s) where
+instance ∀ s . (ScalarManifold s, Eq s) => PreArrow (Affine s) where
   Affine f &&& Affine g = Affine . trie
       $ \ix -> case (untrie f ix, untrie g ix) of
             ((fα, ðα'f), (gβ,ðβ'g)) -> ((fα,gβ), ðα'f&&&ðβ'g)
   terminal = Affine . trie $ \_ -> (Origin, zeroV)
   fst = afst
-   where afst :: ∀ x y . ( Atlas x, Atlas y
+   where afst :: ∀ x y . ( Manifold (x, y), Atlas (x, y)
                          , LinearSpace (Needle x), LinearSpace (Needle y)
                          , Scalar (Needle x) ~ s, Scalar (Needle y) ~ s
                          , HasTrie (ChartIndex x), HasTrie (ChartIndex y) )
                    => Affine s (x,y) x
-         afst = Affine . trie $ chartReferencePoint >>> \(x,_::y) -> (x, fst)
+         afst = Affine . trie $ chartReferencePoint @(x,y) >>> \(x,_::y) -> (x, fst)
   snd = asnd
-   where asnd :: ∀ x y . ( Atlas x, Atlas y
+   where asnd :: ∀ x y . ( Manifold (x, y), Atlas (x, y)
                          , LinearSpace (Needle x), LinearSpace (Needle y)
                          , Scalar (Needle x) ~ s, Scalar (Needle y) ~ s
                          , HasTrie (ChartIndex x), HasTrie (ChartIndex y) )
                    => Affine s (x,y) y
          asnd = Affine . trie $ chartReferencePoint >>> \(_::x,y) -> (y, snd)
   
-instance ∀ s . Num' s => WellPointed (Affine s) where
+instance ∀ s . (ScalarManifold s, Eq s) => WellPointed (Affine s) where
   const x = Affine . trie $ const (x, zeroV)
   unit = Tagged Origin
   
@@ -128,79 +130,77 @@
                           , Scalar x ~ s, Scalar y ~ s )
              => (LinearManifoldWitness x, LinearManifoldWitness y)
                   -> LinearMap s x y -> Affine s x y
-         alarr (LinearManifoldWitness _, LinearManifoldWitness _) f
+         alarr (LinearManifoldWitness, LinearManifoldWitness) f
              = Affine . trie $ chartReferencePoint
                    >>> \x₀ -> let y₀ = f $ x₀
                               in (negateV y₀, f)
 
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , Manifold y, Scalar (Needle y) ~ s )
-              => Semimanifold (Affine s x y) where
+instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold (Needle y), Scalar (Needle y) ~ s
+         ) => Semimanifold (Affine s x y) where
   type Needle (Affine s x y) = Affine s x (Needle y)
-  toInterior = pure
-  fromInterior = id
-  (.+~^) = case ( semimanifoldWitness :: SemimanifoldWitness y
-                , boundarylessWitness :: BoundarylessWitness y ) of
-    (SemimanifoldWitness _, BoundarylessWitness) -> \(Affine f) (Affine g)
+  (.+~^) = case ( semimanifoldWitness :: SemimanifoldWitness y ) of
+    (SemimanifoldWitness) -> \(Affine f) (Affine g)
       -> Affine . trie $ \ix -> case (untrie f ix, untrie g ix) of
           ((fx₀,f'), (gx₀,g')) -> (fx₀.+~^gx₀, f'^+^g')
-  translateP = Tagged (.+~^)
-  semimanifoldWitness = case semimanifoldWitness :: SemimanifoldWitness y of
-    SemimanifoldWitness _ -> SemimanifoldWitness BoundarylessWitness
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , Manifold y, Scalar (Needle y) ~ s )
-              => PseudoAffine (Affine s x y) where
-  (.-~!) = case ( semimanifoldWitness :: SemimanifoldWitness y
-                , boundarylessWitness :: BoundarylessWitness y ) of
-    (SemimanifoldWitness _, BoundarylessWitness) -> \(Affine f) (Affine g)
+  semimanifoldWitness = case smfdWBoundWitness @y of
+    OpenManifoldWitness -> case semimanifoldWitness @y of
+        SemimanifoldWitness -> needleIsOpenMfd @y SemimanifoldWitness
+instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold (Needle y), Scalar (Needle y) ~ s
+         ) => PseudoAffine (Affine s x y) where
+  p.-~.q = pure (p.-~!q)
+  (.-~!) = case ( semimanifoldWitness :: SemimanifoldWitness y ) of
+    (SemimanifoldWitness) -> \(Affine f) (Affine g)
       -> Affine . trie $ \ix -> case (untrie f ix, untrie g ix) of
           ((fx₀,f'), (gx₀,g')) -> (fx₀.-~!gx₀, f'^-^g')
   pseudoAffineWitness = case semimanifoldWitness :: SemimanifoldWitness y of
-    SemimanifoldWitness _ -> PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
+    SemimanifoldWitness -> PseudoAffineWitness (SemimanifoldWitness)
+instance ( Atlas x, HasTrie (ChartIndex x)
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold (Needle y), Scalar (Needle y) ~ s
          , Manifold y, Scalar (Needle y) ~ s )
               => AffineSpace (Affine s x y) where
   type Diff (Affine s x y) = Affine s x (Needle y)
   (.+^) = (.+~^); (.-.) = (.-~!)
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , LinearSpace y, Scalar y ~ s, Num' s )
+instance ( Atlas x, HasTrie (ChartIndex x)
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold y, Scalar y ~ s, Num' s )
             => AdditiveGroup (Affine s x y) where
   zeroV = case linearManifoldWitness :: LinearManifoldWitness y of
-       LinearManifoldWitness _ -> Affine . trie $ const (zeroV, zeroV)
+       LinearManifoldWitness -> Affine . trie $ const (zeroV, zeroV)
   (^+^) = case ( linearManifoldWitness :: LinearManifoldWitness y
                , dualSpaceWitness :: DualSpaceWitness y ) of
-      (LinearManifoldWitness BoundarylessWitness, DualSpaceWitness) -> (.+~^)
+      (LinearManifoldWitness, DualSpaceWitness) -> (.+~^)
   negateV = case linearManifoldWitness :: LinearManifoldWitness y of
-       LinearManifoldWitness _ -> \(Affine f) -> Affine . trie $
+       LinearManifoldWitness -> \(Affine f) -> Affine . trie $
              untrie f >>> negateV***negateV
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , LinearSpace y, Scalar y ~ s, Num' s )
+instance ( Atlas x, HasTrie (ChartIndex x)
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold y, Scalar y ~ s, Num' s )
             => VectorSpace (Affine s x y) where
   type Scalar (Affine s x y) = s
   (*^) = case linearManifoldWitness :: LinearManifoldWitness y of
-       LinearManifoldWitness _ -> \μ (Affine f) -> Affine . trie $
+       LinearManifoldWitness -> \μ (Affine f) -> Affine . trie $
              untrie f >>> (μ*^)***(μ*^)
 
-evalAffine :: ∀ s x y . ( Manifold x, Atlas x, HasTrie (ChartIndex x)
+evalAffine :: ∀ x y s . ( Manifold x, Atlas x, HasTrie (ChartIndex x)
                         , Manifold y
                         , s ~ Scalar (Needle x), s ~ Scalar (Needle y) )
                => Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
-evalAffine = ea (boundarylessWitness, boundarylessWitness)
- where ea :: (BoundarylessWitness x, BoundarylessWitness y)
-             -> Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
-       ea (BoundarylessWitness, BoundarylessWitness)
-          (Affine f) x = (fx₀.+~^(ðx'f $ v), ðx'f)
-        where Just v = x .-~. chartReferencePoint chIx
-              chIx = lookupAtlas x
-              (fx₀, ðx'f) = untrie f chIx
+evalAffine (Affine f) x = (fx₀.+~^(ðx'f $ v), ðx'f)
+ where Just v = x .-~. chartReferencePoint chIx
+       chIx = lookupAtlas x
+       (fx₀, ðx'f) = untrie f chIx
 
-fromOffsetSlope :: ∀ s x y . ( LinearSpace x, Atlas x, HasTrie (ChartIndex x)
+fromOffsetSlope :: ∀ x y s . ( LinearSpace x, Atlas x, HasTrie (ChartIndex x)
                              , Manifold y
                              , s ~ Scalar x, s ~ Scalar (Needle y) )
                => y -> LinearMap s x (Needle y) -> Affine s x y
-fromOffsetSlope = case ( linearManifoldWitness :: LinearManifoldWitness x
-                       , boundarylessWitness :: BoundarylessWitness y ) of
-   (LinearManifoldWitness _, BoundarylessWitness)
+fromOffsetSlope = case ( linearManifoldWitness :: LinearManifoldWitness x ) of
+   (LinearManifoldWitness)
        -> \y0 ðx'y -> Affine . trie $ chartReferencePoint
                     >>> \x₀ -> let δy = ðx'y $ x₀
                                in (y0.+~^δy, ðx'y)
@@ -210,7 +210,7 @@
   arr (Embedding e p) = Embedding (arr e) (arr p)
 
 
-lensEmbedding :: ∀ k s x c .
+lensEmbedding :: ∀ k x c s .
                  ( Num' s
                  , LinearSpace x, LinearSpace c, Object k x, Object k c
                  , Scalar x ~ s, Scalar c ~ s
@@ -222,32 +222,30 @@
                                      :: LinearMap s x c) )
 
 
-correspondingDirections :: ∀ s x c t
+correspondingDirections :: ∀ x c t s
                         . ( WithField s AffineManifold c
                           , WithField s AffineManifold x
                           , SemiInner (Needle c), SemiInner (Needle x)
                           , RealFrac' s
                           , Traversable t )
-              => (Interior c, Interior x)
-                  -> t (Needle c, Needle x) -> Maybe (Embedding (Affine s) c x)
+         => (c, x) -> t (Needle c, Needle x) -> Maybe (Embedding (Affine s) c x)
 correspondingDirections (c₀, x₀) dirMap
-   = freeEmbeddings $> Embedding (Affine . trie $ c2x boundarylessWitness)
-                                 (Affine . trie $ x2c boundarylessWitness)
+   = freeEmbeddings $> Embedding (Affine . trie $ c2x)
+                                 (Affine . trie $ x2c)
  where freeEmbeddings = fzip ( embedFreeSubspace $ fst<$>dirMap
                              , embedFreeSubspace $ snd<$>dirMap )
        c2t :: Lens' (Needle c) (t s)
        c2t = case freeEmbeddings of Just (Lens ct, _) -> ct
        x2t :: Lens' (Needle x) (t s)
        x2t = case freeEmbeddings of Just (_, Lens xt) -> xt
-       c2x :: BoundarylessWitness c -> ChartIndex c
-                            -> (x, LinearMap s (Needle c) (Needle x))
-       c2x BoundarylessWitness ιc
+       c2x :: ChartIndex c -> (x, LinearMap s (Needle c) (Needle x))
+       c2x ιc
               = ( x₀ .+~^ (zeroV & x2t .~ δc^.c2t)
                 , arr . LinearFunction $ \dc -> zeroV & x2t .~ dc^.c2t )
         where Just δc = chartReferencePoint ιc .-~. c₀
-       x2c :: BoundarylessWitness x -> ChartIndex x
+       x2c :: ChartIndex x
                             -> (c, LinearMap s (Needle x) (Needle c))
-       x2c BoundarylessWitness ιx
+       x2c ιx
               = ( c₀ .+~^ (zeroV & c2t .~ δx^.x2t)
                 , arr . LinearFunction $ \dx -> zeroV & c2t .~ dx^.x2t )
         where Just δx = chartReferencePoint ιx .-~. x₀
diff --git a/Data/Function/Differentiable.hs b/Data/Function/Differentiable.hs
--- a/Data/Function/Differentiable.hs
+++ b/Data/Function/Differentiable.hs
@@ -20,6 +20,7 @@
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE PatternGuards            #-}
 {-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE TypeApplications         #-}
 {-# LANGUAGE UnicodeSyntax            #-}
 {-# LANGUAGE MultiWayIf               #-}
 {-# LANGUAGE LambdaCase               #-}
@@ -65,6 +66,8 @@
 import Data.Tagged
 import Data.Manifold.Types.Primitive
 import Data.Manifold.PseudoAffine
+import Data.Manifold.WithBoundary
+import Data.Manifold.WithBoundary.Class
 import Data.Manifold.Atlas
 
 import qualified Prelude
@@ -78,8 +81,8 @@
 
 
 type RealDimension s
-       = ( RealFloat' s, SimpleSpace s, Show s, Atlas s, HasTrie (ChartIndex s)
-         , s ~ Needle s, s ~ Interior s, s ~ Scalar s, s ~ DualVector s )
+       = ( RealFloat' s, Manifold s, SimpleSpace s, Atlas' s
+         , s ~ Needle s, s ~ Scalar s, s ~ DualVector s )
 
 
 discretisePathIn :: (WithField ℝ Manifold y, SimpleSpace (Needle y))
@@ -215,7 +218,8 @@
 
 -- | Represent a 'Region' by a smooth function which is positive within the region,
 --   and crosses zero at the boundary.
-smoothIndicator :: LocallyScalable ℝ q => Region ℝ q -> Differentiable ℝ q ℝ
+smoothIndicator :: (LocallyScalable ℝ q, Manifold q, Atlas' q, SimpleSpace (Needle q))
+                       => Region ℝ q -> Differentiable ℝ q ℝ
 smoothIndicator (Region _ r₀) = let (PreRegion r) = genericisePreRegion r₀
                                 in  r
 
@@ -265,14 +269,15 @@
 
 
 
-
+showℝ :: RealFloat r => r -> String
+showℝ x = show (realToFrac x :: Double)
 
 
 unsafe_dev_ε_δ :: ∀ a . RealDimension a
                 => String -> (a -> a) -> LinDevPropag a a
 unsafe_dev_ε_δ = case ( linearManifoldWitness :: LinearManifoldWitness a
                       , closedScalarWitness :: ClosedScalarWitness a ) of
- (LinearManifoldWitness _, ClosedScalarWitness) -> \errHint f d
+ (LinearManifoldWitness, ClosedScalarWitness) -> \errHint f d
            -> let ε'² = normSq d 1
               in if ε'²>0
                   then let δ = f . sqrt $ recip ε'²
@@ -280,14 +285,15 @@
                            then spanNorm [recip δ]
                            else error $ "ε-δ propagator function for "
                                     ++errHint++", with ε="
-                                    ++show(sqrt $ recip ε'²)
-                                    ++ " gives non-positive δ="++show δ++"."
+                                    ++showℝ (sqrt $ recip ε'²)
+                                    ++ " gives non-positive δ="
+                                    ++showℝ (realToFrac δ)++"."
                   else mempty
 dev_ε_δ :: ∀ a . RealDimension a
          => (a -> a) -> Metric a -> Maybe (Metric a)
 dev_ε_δ = case ( linearManifoldWitness :: LinearManifoldWitness a
                       , closedScalarWitness :: ClosedScalarWitness a ) of
- (LinearManifoldWitness _, ClosedScalarWitness) -> \f d
+ (LinearManifoldWitness, ClosedScalarWitness) -> \f d
            -> let ε'² = normSq d 1
               in if ε'²>0
                   then let δ = f . sqrt $ recip ε'²
@@ -299,7 +305,7 @@
 as_devεδ :: ∀ a . RealDimension a => LinDevPropag a a -> a -> a
 as_devεδ = asdevεδ linearManifoldWitness closedScalarWitness where
  asdevεδ :: LinearManifoldWitness a -> ClosedScalarWitness a -> LinDevPropag a a -> a -> a
- asdevεδ (LinearManifoldWitness _) ClosedScalarWitness
+ asdevεδ LinearManifoldWitness ClosedScalarWitness
          ldp ε | ε>0
                , δ'² <- normSq (ldp $ spanNorm [recip ε]) 1
                , δ'² > 0
@@ -316,7 +322,8 @@
 
 
 instance RealFrac' s => Category (Differentiable s) where
-  type Object (Differentiable s) o = LocallyScalable s o
+  type Object (Differentiable s) o = ( Manifold o, Atlas' o
+                                     , LocallyScalable s o, SimpleSpace (Needle o) )
   id = Differentiable $ \x -> (x, id, const mempty)
   Differentiable f . Differentiable g = Differentiable $
      \x -> let (y, g', devg) = g x
@@ -336,7 +343,7 @@
   arr (Differentiable f) x = let (y,_,_) = f x in y
   arr (AffinDiffable _ f) x = f $ x
 
-instance (RealFrac' s) => Cartesian (Differentiable s) where
+instance (RealFrac'' s, SimpleSpace s) => Cartesian (Differentiable s) where
   type UnitObject (Differentiable s) = ZeroDim s
   swap = Differentiable $ \(x,y) -> ((y,x), swap, const mempty)
   attachUnit = Differentiable $ \x -> ((x, Origin), attachUnit, const mempty)
@@ -345,22 +352,48 @@
   regroup' = Differentiable $ \((x,y),z) -> ((x,(y,z)), regroup', const mempty)
 
 
-instance (RealFrac' s) => Morphism (Differentiable s) where
-  Differentiable f *** Differentiable g = Differentiable h
-   where h (x,y) = ((fx, gy), f'***g', devfg)
-          where (fx, f', devf) = f x
-                (gy, g', devg) = g y
-                devfg δs = transformNorm fst δx 
-                           <> transformNorm snd δy
-                  where δx = devf $ transformNorm (id&&&zeroV) δs
-                        δy = devg $ transformNorm (zeroV&&&id) δs
-  AffinDiffable IsDiffableEndo f *** AffinDiffable IsDiffableEndo g
-         = AffinDiffable IsDiffableEndo $ f *** g
-  AffinDiffable _ f *** AffinDiffable _ g = AffinDiffable NotDiffableEndo $ f *** g
-  f *** g = genericiseDifferentiable f *** genericiseDifferentiable g
+instance ∀ s . (RealFrac'' s, SimpleSpace s) => Morphism (Differentiable s) where
+  (***) = prll
+   where prll :: ∀ b β c γ . ( ObjectPair (Differentiable s) b β
+                             , ObjectPair (Differentiable s) c γ )
+                   => Differentiable s b c -> Differentiable s β γ
+                        -> Differentiable s (b,β) (c,γ)
+         prll (Differentiable f) (Differentiable g) = Differentiable h
+          where h (x,y) = ((fx, gy), f'***g', devfg)
+                 where (fx, f', devf) = f x
+                       (gy, g', devg) = g y
+                       devfg δs = transformNorm fst δx 
+                                  <> transformNorm snd δy
+                         where δx = devf $ transformNorm (id&&&zeroV) δs
+                               δy = devg $ transformNorm (zeroV&&&id) δs
+         prll (AffinDiffable IsDiffableEndo f) (AffinDiffable IsDiffableEndo g)
+                 = case ( semimanifoldWitness @b, semimanifoldWitness @β
+                        , smfdWBoundWitness @b, smfdWBoundWitness @β
+                        , dualSpaceWitness @(Needle b), dualSpaceWitness @(Needle β)
+                        , smfdWBoundWitness @s
+                        ) of
+           ( SemimanifoldWitness, SemimanifoldWitness
+            ,OpenManifoldWitness, OpenManifoldWitness
+            ,DualSpaceWitness, DualSpaceWitness
+            ,OpenManifoldWitness )
+             -> boundaryHasSameScalar @(Needle b)
+                 ( boundaryHasSameScalar @(Needle β)
+                 ( AffinDiffable IsDiffableEndo $ f *** g ))
+         prll (AffinDiffable _ f) (AffinDiffable _ g)
+          = boundaryHasSameScalar @(Needle β) (
+             boundaryHasSameScalar @(Needle γ) (
+              boundaryHasSameScalar @(Needle b) (
+               boundaryHasSameScalar @(Needle c) (
+              case ( semimanifoldWitness @β, semimanifoldWitness @γ
+                   , semimanifoldWitness @b, semimanifoldWitness @c ) of
+                 (SemimanifoldWitness, SemimanifoldWitness
+                  , SemimanifoldWitness, SemimanifoldWitness)
+                   -> AffinDiffable NotDiffableEndo $ f *** g
+             ))))
+         prll f g = genericiseDifferentiable f *** genericiseDifferentiable g
 
 
-instance (RealFrac' s) => PreArrow (Differentiable s) where
+instance (RealFrac'' s, SimpleSpace s) => PreArrow (Differentiable s) where
   terminal = Differentiable $ \_ -> (Origin, zeroV, const mempty)
   fst = Differentiable $ \(x,_) -> (x, fst, const mempty)
   snd = Differentiable $ \(_,y) -> (y, snd, const mempty)
@@ -373,7 +406,7 @@
   f &&& g = genericiseDifferentiable f &&& genericiseDifferentiable g
 
 
-instance (RealFrac' s) => WellPointed (Differentiable s) where
+instance (RealFrac'' s, SimpleSpace s) => WellPointed (Differentiable s) where
   unit = Tagged Origin
   globalElement x = Differentiable $ \Origin -> (x, zeroV, const mempty)
   const x = Differentiable $ \_ -> (x, zeroV, const mempty)
@@ -382,33 +415,74 @@
 
 type DfblFuncValue s = GenericAgent (Differentiable s)
 
-instance (RealFrac' s) => HasAgent (Differentiable s) where
+instance (RealFrac'' s) => HasAgent (Differentiable s) where
   alg = genericAlg
   ($~) = genericAgentMap
-instance ∀ s . (RealFrac' s) => CartesianAgent (Differentiable s) where
+instance ∀ s . (RealFloat'' s, SimpleSpace s) => CartesianAgent (Differentiable s) where
   alg1to2 = genericAlg1to2
   alg2to1 = a2t1
-   where a2t1 :: ∀ α β γ . (LocallyScalable s α, LocallyScalable s β)
-           => (∀ q . LocallyScalable s q
+   where a2t1 :: ∀ α β γ . ( Manifold α, Manifold β
+                           , Atlas' α, Atlas' β
+                           , ProjectableBoundary α
+                           , LocallyScalable s α, LocallyScalable s β
+                           )
+           => (∀ q . ( LocallyScalable s q, Manifold q, Atlas q
+                     , Interior (Needle q) ~ Needle q
+                     , PseudoAffineWithBoundary (Needle q)
+                     , LinearManifold (Needle q)
+                     , SimpleSpace (Needle q)
+                     , HasTrie (ChartIndex q) )
                => DfblFuncValue s q α -> DfblFuncValue s q β -> DfblFuncValue s q γ )
            -> Differentiable s (α,β) γ
-         a2t1 = case ( dualSpaceWitness :: DualSpaceWitness (Needle α)
-                     , dualSpaceWitness :: DualSpaceWitness (Needle β) ) of
-            (DualSpaceWitness, DualSpaceWitness) -> genericAlg2to1
+         a2t1 f = case ( semimanifoldWitness @α, semimanifoldWitness @β
+                       , dualSpaceWitness @(Needle α), dualSpaceWitness @(Needle β) ) of
+            ( SemimanifoldWitness, SemimanifoldWitness
+             ,DualSpaceWitness, DualSpaceWitness )
+                -> needleIsOpenMfd @α
+                    (needleIsOpenMfd @β
+                      (boundaryHasSameScalar @α
+                        (boundaryHasSameScalar @β
+                          (boundaryHasSameScalar @(Needle α)
+                            (boundaryHasSameScalar @(Needle β)
+                              (undefined -- genericAlg2to1 f
+                                     ))))))
   alg2to2 = a2t1
-   where a2t1 :: ∀ α β γ δ . ( LocallyScalable s α, LocallyScalable s β
+   where a2t1 :: ∀ α β γ δ . ( Manifold α, Manifold β, Manifold γ, Manifold δ
+                             , Atlas' α, Atlas' β, Atlas' γ, Atlas' δ
+                             , LocallyScalable s α, LocallyScalable s β
                              , LocallyScalable s γ, LocallyScalable s δ )
-           => (∀ q . LocallyScalable s q
+           => (∀ q . ( LocallyScalable s q, Manifold q, Atlas q
+                     , Interior (Needle q) ~ Needle q
+                     , PseudoAffineWithBoundary (Needle q)
+                     , LinearManifold (Needle q)
+                     , SimpleSpace (Needle q)
+                     , HasTrie (ChartIndex q) )
                => DfblFuncValue s q α -> DfblFuncValue s q β
                      -> (DfblFuncValue s q γ, DfblFuncValue s q δ) )
            -> Differentiable s (α,β) (γ,δ)
-         a2t1 = case ( dualSpaceWitness :: DualSpaceWitness (Needle α)
-                     , dualSpaceWitness :: DualSpaceWitness (Needle β)
-                     , dualSpaceWitness :: DualSpaceWitness (Needle γ)
-                     , dualSpaceWitness :: DualSpaceWitness (Needle δ) ) of
-            (DualSpaceWitness, DualSpaceWitness, DualSpaceWitness, DualSpaceWitness)
-                  -> genericAlg2to2
-instance (RealFrac' s)
+         a2t1 f = case ( semimanifoldWitness @α, semimanifoldWitness @β
+                       , semimanifoldWitness @γ, semimanifoldWitness @δ
+                       , dualSpaceWitness @(Needle α), dualSpaceWitness @(Needle β)
+                       , dualSpaceWitness @(Needle γ), dualSpaceWitness @(Needle δ) ) of
+            ( SemimanifoldWitness, SemimanifoldWitness
+             ,SemimanifoldWitness, SemimanifoldWitness
+             ,DualSpaceWitness, DualSpaceWitness
+             ,DualSpaceWitness, DualSpaceWitness )
+                 -> needleIsOpenMfd @α
+                    (needleIsOpenMfd @β
+                     (needleIsOpenMfd @γ
+                      (needleIsOpenMfd @δ
+                       (boundaryHasSameScalar @α
+                        (boundaryHasSameScalar @β
+                         (boundaryHasSameScalar @γ
+                          (boundaryHasSameScalar @δ
+                           (boundaryHasSameScalar @(Needle α)
+                            (boundaryHasSameScalar @(Needle β)
+                             (boundaryHasSameScalar @(Needle γ)
+                              (boundaryHasSameScalar @(Needle δ)
+                               (undefined -- genericAlg2to2 f
+                                 ))))))))))))
+instance (RealFrac'' s, SimpleSpace s)
       => PointAgent (DfblFuncValue s) (Differentiable s) a x where
   point = genericPoint
 
@@ -438,18 +512,32 @@
 -- affinPoint p = GenericAgent (AffinDiffable (const p))
 
 
-dfblFnValsFunc :: ( LocallyScalable s c, LocallyScalable s c', LocallyScalable s d
-                  , v ~ Needle c, v' ~ Needle c'
-                  , ε ~ Norm v, ε ~ Norm v'
-                  , RealFrac' s )
+dfblFnValsFunc :: ∀ c c' d v v' ε s
+     . ( Manifold c, Manifold d, Manifold c'
+       , Atlas' c, Atlas' d, Atlas' c'
+       , ProjectableBoundary s, ProjectableBoundary v'
+       , ProjectableBoundary (Needle d)
+       , SimpleSpace (Needle d)
+       , LocallyScalable s c, LocallyScalable s c', LocallyScalable s d
+       , v ~ Needle c, v' ~ Needle c'
+       , ε ~ Norm v, ε ~ Norm v'
+       , SimpleSpace v'
+       , RealFrac'' s )
              => (c' -> (c, v'+>v, ε->ε)) -> DfblFuncValue s d c' -> DfblFuncValue s d c
-dfblFnValsFunc f = (Differentiable f $~)
+dfblFnValsFunc f = case ( scalarSpaceWitness @s
+                        , smfdWBoundWitness @s
+                        , semimanifoldWitness @d
+                        , semimanifoldWitness @c' ) of
+   ( ScalarSpaceWitness, OpenManifoldWitness
+    ,SemimanifoldWitness, SemimanifoldWitness )
+        -> needleIsOpenMfd @c (needleIsOpenMfd @d (Differentiable f $~))
 
 dfblFnValsCombine :: forall d c c' c'' v v' v'' ε ε' ε'' s. 
          ( LocallyScalable s c,  LocallyScalable s c',  LocallyScalable s c''
          ,  LocallyScalable s d
          , v ~ Needle c, v' ~ Needle c', v'' ~ Needle c''
          , ε ~ Norm v  , ε' ~ Norm v'  , ε'' ~ Norm v'', ε~ε', ε~ε'' 
+         , SimpleSpace (Needle d)
          , RealFrac' s )
        => (  c' -> c'' -> (c, (v',v'')+>v, ε -> (ε',ε''))  )
          -> DfblFuncValue s d c' -> DfblFuncValue s d c'' -> DfblFuncValue s d c
@@ -477,38 +565,59 @@
 
 
 
-instance ∀ v s a . (LinearSpace v, Scalar v ~ s, LocallyScalable s a, RealFloat' s)
+instance ∀ v s a . ( LinearManifold v, Scalar v ~ s
+                   , LocallyScalable s a, Manifold a, Atlas' a, Atlas' v
+                   , SimpleSpace v, SimpleSpace (Needle a)
+                   , RealFloat'' s )
     => AdditiveGroup (DfblFuncValue s a v) where
-  zeroV = case ( linearManifoldWitness :: LinearManifoldWitness v
-               , dualSpaceWitness :: DualSpaceWitness v ) of
-     (LinearManifoldWitness _, DualSpaceWitness) -> point zeroV
-  (^+^) = case ( linearManifoldWitness :: LinearManifoldWitness v
-               , dualSpaceWitness :: DualSpaceWitness v ) of
-     (LinearManifoldWitness _, DualSpaceWitness)
+  zeroV = case ( linearManifoldWitness @v, dualSpaceWitness @v
+               , semimanifoldWitness @a
+               ) of
+     (LinearManifoldWitness, DualSpaceWitness, SemimanifoldWitness)
+         -> needleIsOpenMfd @a (scalarIsOpenMfd @a
+               (needleBoundaryIsTriviallyProjectible @a (point zeroV)))
+  (^+^) = needleIsOpenMfd @a ( needleBoundaryIsTriviallyProjectible @a
+               (case ( linearManifoldWitness @v
+                     , linearManifoldWitness @(Needle a)
+                     , dualSpaceWitness @v
+                     , dualSpaceWitness @(Needle a) ) of
+     (LinearManifoldWitness, LinearManifoldWitness
+      ,DualSpaceWitness, DualSpaceWitness)
          -> curry $ \case
         (GenericAgent (AffinDiffable ef f), GenericAgent (AffinDiffable eg g))
               -> GenericAgent $ AffinDiffable (ef<>eg) (f^+^g)
         (α,β) -> dfblFnValsCombine (\a b -> (a^+^b, arr addV, const mempty)) α β
-  negateV = case ( linearManifoldWitness :: LinearManifoldWitness v
-                 , dualSpaceWitness :: DualSpaceWitness v ) of
-      (LinearManifoldWitness _, DualSpaceWitness) -> \case
+    ))
+  negateV = needleIsOpenMfd @a (case ( linearManifoldWitness @v, dualSpaceWitness @v
+                                     , semimanifoldWitness @a
+                                     ) of
+     (LinearManifoldWitness, DualSpaceWitness, SemimanifoldWitness)
+         -> needleBoundaryIsTriviallyProjectible @a (\case
          (GenericAgent (AffinDiffable ef f))
            -> GenericAgent $ AffinDiffable ef (negateV f)
          α -> dfblFnValsFunc (\a -> (negateV a, negateV id, const mempty)) α
+      )
+    )
   
-instance ∀ n a . (RealDimension n, LocallyScalable n a)
+instance ∀ n a . ( RealFloat'' n, Manifold a, LocallyScalable n a
+                 , SimpleSpace (Needle a)
+                 , Atlas' a, Atlas' n
+                 )
             => Num (DfblFuncValue n a n) where
-  fromInteger = case ( linearManifoldWitness :: LinearManifoldWitness n
-                     , closedScalarWitness :: ClosedScalarWitness n ) of
-      (LinearManifoldWitness _, ClosedScalarWitness) -> point . fromInteger
+  fromInteger = case ( linearManifoldWitness @n, dualSpaceWitness @n
+                     , semimanifoldWitness @a, closedScalarWitness @n
+                     ) of
+     (LinearManifoldWitness, DualSpaceWitness, SemimanifoldWitness, ClosedScalarWitness)
+         -> needleIsOpenMfd @a (scalarIsOpenMfd @a
+               (needleBoundaryIsTriviallyProjectible @a (point . fromInteger)))
   (+) = case closedScalarWitness :: ClosedScalarWitness n of
       ClosedScalarWitness -> (^+^)
   (*) = case ( linearManifoldWitness :: LinearManifoldWitness n
              , closedScalarWitness :: ClosedScalarWitness n ) of
-      (LinearManifoldWitness _, ClosedScalarWitness) -> dfblFnValsCombine $
+      (LinearManifoldWitness, ClosedScalarWitness) -> dfblFnValsCombine $
           \a b -> ( a*b
                   , arr $ addV <<< (scale $ a)***(scale $ b)
-                  , unsafe_dev_ε_δ(show a++"*"++show b) (sqrt :: n->n)
+                  , unsafe_dev_ε_δ(showℝ a++"*"++showℝ b) (sqrt :: n->n)
                        >>> \d¹₂ -> (d¹₂,d¹₂)
                            -- ε δa δb = (a+δa)·(b+δb) - (a·b + (a·δa + b·δb)) 
                            --         = δa·δb
@@ -516,22 +625,23 @@
                   )
   negate = case closedScalarWitness :: ClosedScalarWitness n of
      ClosedScalarWitness -> negateV
-  abs = mkabs linearManifoldWitness closedScalarWitness
-   where mkabs :: LinearManifoldWitness n -> ClosedScalarWitness n
-                     -> DfblFuncValue n a n -> DfblFuncValue n a n
-         mkabs (LinearManifoldWitness _) ClosedScalarWitness = dfblFnValsFunc dfblAbs
+  abs = needleBoundaryIsTriviallyProjectible @a (
+   case (linearManifoldWitness @n, closedScalarWitness @n) of
+         (LinearManifoldWitness, ClosedScalarWitness) -> dfblFnValsFunc dfblAbs
           where dfblAbs a
-                 | a>0        = (a, id, unsafe_dev_ε_δ("abs "++show a) $ \ε -> a + ε/2) 
-                 | a<0        = (-a, negateV id, unsafe_dev_ε_δ("abs "++show a) $ \ε -> ε/2 - a)
+                 | a>0        = (a, id, unsafe_dev_ε_δ("abs "++showℝ a) $ \ε -> a + ε/2) 
+                 | a<0        = (-a, negateV id, unsafe_dev_ε_δ("abs "++showℝ a)
+                                       $ \ε -> ε/2 - a)
                  | otherwise  = (0, zeroV, scaleNorm (sqrt 0.5))
-  signum = mksgn linearManifoldWitness closedScalarWitness
-   where mksgn :: LinearManifoldWitness n -> ClosedScalarWitness n
-                     -> DfblFuncValue n a n -> DfblFuncValue n a n
-         mksgn (LinearManifoldWitness _) ClosedScalarWitness = dfblFnValsFunc dfblSgn
+     )
+  signum = needleBoundaryIsTriviallyProjectible @a (
+   case (linearManifoldWitness @n, closedScalarWitness @n) of
+         (LinearManifoldWitness, ClosedScalarWitness) -> dfblFnValsFunc dfblSgn
           where dfblSgn a
-                 | a>0        = (1, zeroV, unsafe_dev_ε_δ("signum "++show a) $ const a)
-                 | a<0        = (-1, zeroV, unsafe_dev_ε_δ("signum "++show a) $ \_ -> -a)
+                 | a>0        = (1, zeroV, unsafe_dev_ε_δ("signum "++showℝ a) $ const a)
+                 | a<0        = (-1, zeroV, unsafe_dev_ε_δ("signum "++showℝ a) $ \_ -> -a)
                  | otherwise  = (0, zeroV, const $ spanNorm [1])
+     )
 
 
 
@@ -548,13 +658,13 @@
 
 
 -- | Important special operator needed to compute intersection of 'Region's.
-minDblfuncs :: ∀ s m . (LocallyScalable s m, RealDimension s)
+minDblfuncs :: ∀ m s . (LocallyScalable s m, RealFloat'' s)
      => Differentiable s m s -> Differentiable s m s -> Differentiable s m s
 minDblfuncs (Differentiable f) (Differentiable g)
              = Differentiable $ h linearManifoldWitness closedScalarWitness
  where h :: LinearManifoldWitness s -> ClosedScalarWitness s
              -> m -> (s, Needle m+>Needle s, LinDevPropag m s)
-       h (LinearManifoldWitness _) ClosedScalarWitness x
+       h (LinearManifoldWitness) ClosedScalarWitness x
          | fx < gx   = ( fx, jf
                        , \d -> devf d <> devg d
                                <> transformNorm δj
@@ -577,20 +687,31 @@
 
 
 
-genericisePreRegion :: ∀ s m . (RealDimension s, LocallyScalable s m)
+genericisePreRegion :: ∀ m s
+    . ( RealFloat'' s, LocallyScalable s m, Manifold m
+      , Atlas' m, Atlas' s, SimpleSpace (Needle m)
+      )
                           => PreRegion s m -> PreRegion s m
-genericisePreRegion GlobalRegion = case ( linearManifoldWitness :: LinearManifoldWitness s
-                                        , closedScalarWitness :: ClosedScalarWitness s ) of
-    (LinearManifoldWitness _, ClosedScalarWitness) -> PreRegion $ const 1
-genericisePreRegion (RealSubray PositiveHalfSphere xl) = preRegionToInfFrom' xl
-genericisePreRegion (RealSubray NegativeHalfSphere xr) = preRegionFromMinInfTo' xr
-genericisePreRegion r = r
+genericisePreRegion
+ = scalarIsOpenMfd @m (needleIsOpenMfd @m (needleBoundaryIsTriviallyProjectible @m 
+    (scalarBoundaryIsTriviallyProjectible @m (
+      case ( linearManifoldWitness @s, closedScalarWitness @s, semimanifoldWitness @m ) of
+    (LinearManifoldWitness, ClosedScalarWitness, SemimanifoldWitness)
+          -> \case
+          GlobalRegion -> PreRegion $ const 1
+          RealSubray PositiveHalfSphere xl -> preRegionToInfFrom' xl
+          RealSubray NegativeHalfSphere xr -> preRegionFromMinInfTo' xr
+          r -> r
+  ))))
 
 -- | Set-intersection of regions would not be guaranteed to yield a connected result
 --   or even have the reference point of one region contained in the other. This
 --   combinator assumes (unchecked) that the references are in a connected
 --   sub-intersection, which is used as the result.
-unsafePreRegionIntersect :: (RealDimension s, LocallyScalable s a)
+unsafePreRegionIntersect :: ∀ a s
+    . ( RealFloat'' s, LocallyScalable s a
+      , Manifold a, Atlas' a, Atlas' s
+      , SimpleSpace (Needle a) )
                   => PreRegion s a -> PreRegion s a -> PreRegion s a
 unsafePreRegionIntersect GlobalRegion r = r
 unsafePreRegionIntersect r GlobalRegion = r
@@ -598,29 +719,35 @@
                  = RealSubray PositiveHalfSphere $ max xl xl'
 unsafePreRegionIntersect (RealSubray NegativeHalfSphere xr) (RealSubray NegativeHalfSphere xr')
                  = RealSubray NegativeHalfSphere $ min xr xr'
-unsafePreRegionIntersect (PreRegion ra) (PreRegion rb) = PreRegion $ minDblfuncs ra rb
+unsafePreRegionIntersect (PreRegion ra) (PreRegion rb) = case scalarSpaceWitness @s of
+      ScalarSpaceWitness -> PreRegion $ minDblfuncs ra rb
 unsafePreRegionIntersect ra rb
    = unsafePreRegionIntersect (genericisePreRegion ra) (genericisePreRegion rb)
 
 -- | Cartesian product of two regions.
-regionProd :: (RealDimension s, LocallyScalable s a, LocallyScalable s b)
+regionProd :: ∀ a b s . ( RealDimension s, ObjectPair (Differentiable s) a b )
                   => Region s a -> Region s b -> Region s (a,b)
 regionProd (Region a₀ ra) (Region b₀ rb) = Region (a₀,b₀) (preRegionProd ra rb)
 
 -- | Cartesian product of two pre-regions.
-preRegionProd :: ∀ s a b . (RealDimension s, LocallyScalable s a, LocallyScalable s b)
+preRegionProd :: ∀ a b s . ( RealDimension s, ObjectPair (Differentiable s) a b )
                   => PreRegion s a -> PreRegion s b -> PreRegion s (a,b)
-preRegionProd = prp linearManifoldWitness closedScalarWitness
- where prp :: LinearManifoldWitness s -> ClosedScalarWitness s
-                 -> PreRegion s a -> PreRegion s b -> PreRegion s (a,b)
-       prp _ _ GlobalRegion GlobalRegion = GlobalRegion
-       prp (LinearManifoldWitness _) ClosedScalarWitness GlobalRegion (PreRegion rb)
-                    = PreRegion $ rb . snd
-       prp (LinearManifoldWitness _) ClosedScalarWitness (PreRegion ra) GlobalRegion
-                    = PreRegion $ ra . fst
-       prp (LinearManifoldWitness _) ClosedScalarWitness (PreRegion ra) (PreRegion rb)
-                    = PreRegion $ minDblfuncs (ra.fst) (rb.snd)
-       prp _ _ ra rb = preRegionProd (genericisePreRegion ra) (genericisePreRegion rb)
+preRegionProd = boundaryHasSameScalar @b
+              ( case ( semimanifoldWitness @a, semimanifoldWitness @b
+                     , linearManifoldWitness @s, closedScalarWitness @s
+                     , smfdWBoundWitness @b ) of
+     ( SemimanifoldWitness, SemimanifoldWitness
+      ,LinearManifoldWitness, ClosedScalarWitness
+      ,OpenManifoldWitness ) -> \case
+                      GlobalRegion -> \case
+                          GlobalRegion -> GlobalRegion
+                          (PreRegion rb) -> PreRegion $ rb . snd
+                      (PreRegion ra) -> \case
+                          GlobalRegion -> PreRegion $ ra . fst
+                          (PreRegion rb) -> PreRegion $ minDblfuncs (ra.fst) (rb.snd)
+                      ra -> \rb -> preRegionProd (genericisePreRegion ra)
+                                                 (genericisePreRegion rb)
+   )
 
 
 positivePreRegion, negativePreRegion :: (RealDimension s) => PreRegion s s
@@ -633,10 +760,10 @@
                        $ prr linearManifoldWitness closedScalarWitness
  where prr :: LinearManifoldWitness s -> ClosedScalarWitness s
            -> s -> (s, Needle s+>Needle s, LinDevPropag s s)
-       prr (LinearManifoldWitness _) ClosedScalarWitness
+       prr (LinearManifoldWitness) ClosedScalarWitness
            x = ( 1 - 1/xp1
                , (1/xp1²) *^ id
-               , unsafe_dev_ε_δ("positivePreRegion@"++show x) δ )
+               , unsafe_dev_ε_δ("positivePreRegion@"++showℝ x) δ )
                  -- ε = (1 − 1/(1+x)) + (-δ · 1/(x+1)²) − (1 − 1/(1+x−δ))
                  --   = 1/(1+x−δ) − 1/(1+x) − δ · 1/(x+1)²
                  --
@@ -673,7 +800,7 @@
               xp1² = xp1 ^ 2
 negativePreRegion' = npr (linearManifoldWitness :: LinearManifoldWitness s)
                          (closedScalarWitness :: ClosedScalarWitness s)
- where npr (LinearManifoldWitness BoundarylessWitness)
+ where npr (LinearManifoldWitness)
            (ClosedScalarWitness :: ClosedScalarWitness s)
                   = PreRegion $ ppr . ngt
         where PreRegion ppr = positivePreRegion' :: PreRegion s s
@@ -686,14 +813,14 @@
 preRegionToInfFrom', preRegionFromMinInfTo' :: ∀ s . RealDimension s => s -> PreRegion s s
 preRegionToInfFrom' = prif (linearManifoldWitness :: LinearManifoldWitness s)
                            (closedScalarWitness :: ClosedScalarWitness s)
- where prif (LinearManifoldWitness BoundarylessWitness)
+ where prif (LinearManifoldWitness)
             (ClosedScalarWitness :: ClosedScalarWitness s)
             xs = PreRegion $ ppr . trl
         where PreRegion ppr = positivePreRegion' :: PreRegion s s
               trl = actuallyAffineEndo (-xs) id
 preRegionFromMinInfTo' = prif (linearManifoldWitness :: LinearManifoldWitness s)
                            (closedScalarWitness :: ClosedScalarWitness s)
- where prif (LinearManifoldWitness BoundarylessWitness)
+ where prif (LinearManifoldWitness)
             (ClosedScalarWitness :: ClosedScalarWitness s)
             xe = PreRegion $ ppr . flp
         where PreRegion ppr = positivePreRegion' :: PreRegion s s
@@ -705,10 +832,10 @@
  where m = lb + radius; radius = (rb - lb)/2
        prr :: LinearManifoldWitness s -> ClosedScalarWitness s
                 -> s -> (s, Needle s+>Needle s, LinDevPropag s s)
-       prr (LinearManifoldWitness _) ClosedScalarWitness
+       prr (LinearManifoldWitness) ClosedScalarWitness
            x = ( 1 - ((x-m)/radius)^2
                , (2*(m-x)/radius^2) *^ id
-               , unsafe_dev_ε_δ("intervalPreRegion@"++show x) $ (*radius) . sqrt )
+               , unsafe_dev_ε_δ("intervalPreRegion@"++showℝ x) $ (*radius) . sqrt )
 
 
 
@@ -721,8 +848,10 @@
 
 
 instance (RealDimension s) => Category (RWDiffable s) where
-  type Object (RWDiffable s) o = (LocallyScalable s o, Manifold o, SimpleSpace (Needle o))
-  id = RWDiffable $ \x -> (GlobalRegion, pure id)
+  type Object (RWDiffable s) o = Object (Differentiable s) o
+  id = rwdid
+   where rwdid :: ∀ a . Object (RWDiffable s) a => RWDiffable s a a
+         rwdid = RWDiffable $ \x -> (GlobalRegion, pure id)
   RWDiffable f . RWDiffable g = RWDiffable h where
    h x₀ = case g x₀ of
            ( rg, Just gr'@(AffinDiffable IsDiffableEndo gr) )
@@ -838,10 +967,8 @@
   RWDFV_IdVar :: RWDfblFuncValue s c c
   GenericRWDFV :: RWDiffable s d c -> RWDfblFuncValue s d c
 
-genericiseRWDFV :: ( RealDimension s
-                   , LocallyScalable s c, SimpleSpace (Needle c)
-                   , LocallyScalable s d, SimpleSpace (Needle d)
-                   , Manifold d, Manifold c )
+genericiseRWDFV ::
+   ( RealDimension s, Object (Differentiable s) d, Object (Differentiable s) c )
                     => RWDfblFuncValue s d c -> RWDfblFuncValue s d c
 genericiseRWDFV (ConstRWDFV c) = GenericRWDFV $ const c
 genericiseRWDFV RWDFV_IdVar = GenericRWDFV id
@@ -867,20 +994,19 @@
 
 grwDfblFnValsFunc
      :: ( RealDimension s
-        , LocallyScalable s c, LocallyScalable s c', LocallyScalable s d
-        , Manifold d, Manifold c, Manifold c'
+        , Object (Differentiable s) d, Object (Differentiable s) c, Object (Differentiable s) c'
         , v ~ Needle c, v' ~ Needle c'
-        , SimpleSpace v, SimpleSpace (Needle d)
+        , SimpleSpace v
         , ε ~ Norm v, ε ~ Norm v' )
              => (c' -> (c, v'+>v, ε->ε)) -> RWDfblFuncValue s d c' -> RWDfblFuncValue s d c
 grwDfblFnValsFunc f = (RWDiffable (\_ -> (GlobalRegion, pure (Differentiable f))) $~)
 
 grwDfblFnValsCombine :: forall d c c' c'' v v' v'' ε ε' ε'' s. 
-         ( LocallyScalable s c,  LocallyScalable s c',  LocallyScalable s c''
-         , LocallyScalable s d, RealDimension s
-         , Manifold d, Manifold c', Manifold c''
+         ( RealDimension s
+         , Object (Differentiable s) d, Object (Differentiable s) c'
+         , Object (Differentiable s) c', Object (Differentiable s) c''
          , v ~ Needle c, v' ~ Needle c', v'' ~ Needle c''
-         , SimpleSpace v, SimpleSpace (Needle d)
+         , SimpleSpace v
          , ε ~ Norm v  , ε' ~ Norm v'  , ε'' ~ Norm v'', ε~ε', ε~ε''  )
        => (  c' -> c'' -> (c, (v',v'')+>v, ε -> (ε',ε''))  )
          -> RWDfblFuncValue s d c' -> RWDfblFuncValue s d c'' -> RWDfblFuncValue s d c
@@ -911,16 +1037,20 @@
         = grwDfblFnValsCombine cmb (genericiseRWDFV fv) (genericiseRWDFV gv)
 
           
-rwDfbl_plus :: ∀ s a v .
-        ( WithField s Manifold a
-        , LinearSpace v, Scalar v ~ s
-        , RealDimension s )
+rwDfbl_plus :: ∀ a v s .
+        ( RealDimension s
+        , Object (Differentiable s) a, Object (Differentiable s) v
+        , LinearSpace v )
       => RWDiffable s a v -> RWDiffable s a v -> RWDiffable s a v
 rwDfbl_plus (RWDiffable f) (RWDiffable g) = RWDiffable
-              $ h linearManifoldWitness dualSpaceWitness
-   where h :: LinearManifoldWitness v -> DualSpaceWitness v
+              $ needleIsOpenMfd @a (needleBoundaryIsTriviallyProjectible @a (
+                   h linearManifoldWitness linearManifoldWitness
+                        dualSpaceWitness dualSpaceWitness))
+   where h :: (OpenManifold (Needle a), ProjectableBoundary (Needle a))
+               => LinearManifoldWitness v -> LinearManifoldWitness (Needle a)
+               -> DualSpaceWitness v -> DualSpaceWitness (Needle a)
                 -> a -> (PreRegion s a, Maybe (Differentiable s a v))
-         h (LinearManifoldWitness _) DualSpaceWitness
+         h LinearManifoldWitness LinearManifoldWitness DualSpaceWitness DualSpaceWitness
            x₀ = (rh, liftA2 fgplus ff gf)
           where (rf, ff) = f x₀
                 (rg, gf) = g x₀
@@ -944,15 +1074,20 @@
                 fgplus (AffinDiffable fe fa) (AffinDiffable ge ga)
                            = AffinDiffable (fe<>ge) (fa^+^ga)
 
-rwDfbl_negateV :: ∀ s a v .
+rwDfbl_negateV :: ∀ a v s .
         ( WithField s Manifold a
         , LinearSpace v, Scalar v ~ s
         , RealDimension s )
       => RWDiffable s a v -> RWDiffable s a v
-rwDfbl_negateV (RWDiffable f) = RWDiffable $ h linearManifoldWitness dualSpaceWitness
-   where h :: LinearManifoldWitness v -> DualSpaceWitness v
+rwDfbl_negateV (RWDiffable f) = RWDiffable
+           $ needleIsOpenMfd @a (needleBoundaryIsTriviallyProjectible @a (
+                  h linearManifoldWitness dualSpaceWitness
+                    linearManifoldWitness dualSpaceWitness))
+   where h :: (OpenManifold (Needle a), ProjectableBoundary (Needle a))
+             => LinearManifoldWitness v -> DualSpaceWitness v
+              -> LinearManifoldWitness (Needle a) -> DualSpaceWitness (Needle a)
                 -> a -> (PreRegion s a, Maybe (Differentiable s a v))
-         h (LinearManifoldWitness _) DualSpaceWitness
+         h LinearManifoldWitness DualSpaceWitness LinearManifoldWitness DualSpaceWitness
            x₀ = (rf, fmap fneg ff)
           where (rf, ff) = f x₀
                 fneg :: Differentiable s a v -> Differentiable s a v
@@ -961,10 +1096,10 @@
                         where (fx, jf, δf) = fd x
                 fneg (AffinDiffable ef af) = AffinDiffable ef $ negateV af
 
-postCompRW :: ( RealDimension s
-              , LocallyScalable s a, LocallyScalable s b, LocallyScalable s c
-              , Manifold a, Manifold b, Manifold c
-              , SimpleSpace (Needle a), SimpleSpace (Needle b), SimpleSpace (Needle c) )
+postCompRW :: ∀ a b c s . ( RealDimension s
+                          , Object (Differentiable s) a
+                          , Object (Differentiable s) b
+                          , Object (Differentiable s) c )
               => RWDiffable s b c -> RWDfblFuncValue s a b -> RWDfblFuncValue s a c
 postCompRW (RWDiffable f) (ConstRWDFV x) = case f x of
      (_, Just fd) -> ConstRWDFV $ fd $ x
@@ -972,16 +1107,16 @@
 postCompRW f (GenericRWDFV g) = GenericRWDFV $ f . g
 
 
-instance ∀ s a v . ( WithField s Manifold a, SimpleSpace (Needle a)
-                   , Atlas v, HasTrie (ChartIndex v), SimpleSpace v, Scalar v ~ s
-                   , RealDimension s )
+instance ∀ s a v . ( RealDimension s
+                   , Object (Differentiable s) a, Object (Differentiable s) v
+                   , LinearSpace v )
     => AdditiveGroup (RWDfblFuncValue s a v) where
   zeroV = case ( linearManifoldWitness :: LinearManifoldWitness v
                , dualSpaceWitness :: DualSpaceWitness v ) of
-      (LinearManifoldWitness BoundarylessWitness, DualSpaceWitness) -> point zeroV
+      (LinearManifoldWitness, DualSpaceWitness) -> point zeroV
   (^+^) = case ( linearManifoldWitness :: LinearManifoldWitness v
                , dualSpaceWitness :: DualSpaceWitness v ) of
-      (LinearManifoldWitness BoundarylessWitness, DualSpaceWitness)
+      (LinearManifoldWitness, DualSpaceWitness)
          -> curry $ \case
               (ConstRWDFV c₁, ConstRWDFV c₂) -> ConstRWDFV (c₁^+^c₂)
               (ConstRWDFV c₁, RWDFV_IdVar) -> GenericRWDFV $
@@ -997,7 +1132,7 @@
                                 -> GenericRWDFV $ rwDfbl_plus f g
   negateV = case ( linearManifoldWitness :: LinearManifoldWitness v
                  , dualSpaceWitness :: DualSpaceWitness v ) of
-      (LinearManifoldWitness BoundarylessWitness, DualSpaceWitness) -> \case
+      (LinearManifoldWitness, DualSpaceWitness) -> \case
         (ConstRWDFV c) -> ConstRWDFV (negateV c)
         RWDFV_IdVar -> GenericRWDFV $ globalDiffable' (actuallyLinearEndo $ negateV id)
         (GenericRWDFV f) -> GenericRWDFV $ rwDfbl_negateV f
@@ -1012,12 +1147,11 @@
               s' = adjoint $ s :: LinearMap s v (DualVector w)
               tSpread = sum . map recip_t²PLUSs² $ snd (decomposeLinMap t') []
               sSpread = sum . map recip_t²PLUSs² $ snd (decomposeLinMap s') []
-              t²PLUSs²@(Norm t²Ps²M)
+              t²PLUSs²'@(Norm t²Ps²M)
                 = transformNorm t euclideanNorm <> transformNorm s euclideanNorm :: Norm w
-              recip_t²PLUSs² = normSq (dualNorm t²PLUSs²) :: DualVector w -> s
+              recip_t²PLUSs² = normSq (dualNorm t²PLUSs²') :: DualVector w -> s
 
-instance ( RealDimension n, WithField n Manifold a
-         , LocallyScalable n a, SimpleSpace (Needle a))
+instance ∀ n a . ( RealDimension n, Object (Differentiable n) a, SimpleSpace (Needle a) )
             => Num (RWDfblFuncValue n a n) where
   fromInteger i = point $ fromInteger i
   (+) = (^+^)
@@ -1031,8 +1165,7 @@
   GenericRWDFV f * ConstRWDFV c₂ = GenericRWDFV $
                                globalDiffable' (actuallyLinearEndo . arr $ scale $ c₂) . f
   f*g = genericiseRWDFV f ⋅ genericiseRWDFV g
-   where (⋅) :: ∀ n a . (RealDimension n, LocallyScalable n a, SimpleSpace (Needle a))
-           => RWDfblFuncValue n a n -> RWDfblFuncValue n a n -> RWDfblFuncValue n a n 
+   where (⋅) :: RWDfblFuncValue n a n -> RWDfblFuncValue n a n -> RWDfblFuncValue n a n 
          GenericRWDFV (RWDiffable fpcs) ⋅ GenericRWDFV (RWDiffable gpcs)
            = GenericRWDFV . RWDiffable $
                \d₀ -> let (rc₁, fmay) = fpcs d₀
@@ -1083,14 +1216,13 @@
           | a₀<0       = (negativePreRegion, pure (const $ -1))
           | otherwise  = (positivePreRegion, pure (const 1))
 
-instance ( RealDimension n, WithField n Manifold a
-         , LocallyScalable n a, SimpleSpace (Needle a))
+instance ∀ n a . ( RealDimension n, Object (Differentiable n) a, SimpleSpace (Needle a) )
             => Fractional (RWDfblFuncValue n a n) where
   fromRational i = point $ fromRational i
   recip = postCompRW . RWDiffable $ \a₀ -> if a₀<0
                                     then (negativePreRegion, pure (Differentiable negp))
                                     else (positivePreRegion, pure (Differentiable posp))
-   where negp x = (x'¹, (- x'¹^2) *^ id, unsafe_dev_ε_δ("1/"++show x) δ)
+   where negp x = (x'¹, (- x'¹^2) *^ id, unsafe_dev_ε_δ("1/"++showℝ x) δ)
                  -- ε = 1/x − δ/x² − 1/(x+δ)
                  -- ε·x + ε·δ = 1 + δ/x − δ/x − δ²/x² − 1
                  --           = -δ²/x²
@@ -1103,7 +1235,7 @@
                            else - x -- numerical underflow of εx³ vs mph
                                     --  ≡ ε*x^3 / (2*mph) (Taylor-expansion of the root)
                 x'¹ = recip x
-         posp x = (x'¹, (- x'¹^2) *^ id, unsafe_dev_ε_δ("1/"++show x) δ)
+         posp x = (x'¹, (- x'¹^2) *^ id, unsafe_dev_ε_δ("1/"++showℝ x) δ)
           where δ ε = let mph = ε*x^2/2
                           δ₀ = sqrt (mph^2 + ε*x^3) - mph
                       in if δ₀>0 then δ₀ else x
@@ -1112,18 +1244,17 @@
 
 
 
-instance ∀ n a . ( RealDimension n, WithField n Manifold a
-                 , LocallyScalable n a, SimpleSpace (Needle a) )
+instance ∀ n a . ( RealDimension n, Object (Differentiable n) a, SimpleSpace (Needle a) )
             => Floating (RWDfblFuncValue n a n) where
   pi = point pi
   
   exp = grwDfblFnValsFunc
     $ \x -> let ex = exp x
             in if ex*2 == ex  -- numerical trouble...
-                then if x<0 then ( 0, zeroV, unsafe_dev_ε_δ("exp "++show x) $ \ε -> log ε - x )
+                then if x<0 then ( 0, zeroV, unsafe_dev_ε_δ("exp "++showℝ x) $ \ε -> log ε - x )
                             else ( ex, ex*^id
-                                 , unsafe_dev_ε_δ("exp "++show x) $ \_ -> 1e-300 :: n )
-                else ( ex, ex *^ id, unsafe_dev_ε_δ("exp "++show x)
+                                 , unsafe_dev_ε_δ("exp "++showℝ x) $ \_ -> 1e-300 :: n )
+                else ( ex, ex *^ id, unsafe_dev_ε_δ("exp "++showℝ x)
                           $ \ε -> case acosh(ε/(2*ex) + 1) of
                                     δ | δ==δ      -> δ
                                       | otherwise -> log ε - x )
@@ -1136,7 +1267,7 @@
   log = postCompRW . RWDiffable $ \x -> if x>0
                                   then (positivePreRegion, pure (Differentiable lnPosR))
                                   else (negativePreRegion, notDefinedHere)
-   where lnPosR x = ( log x, recip x *^ id, unsafe_dev_ε_δ("log "++show x) $ \ε -> x * sqrt(1 - exp(-ε)) )
+   where lnPosR x = ( log x, recip x *^ id, unsafe_dev_ε_δ("log "++showℝ x) $ \ε -> x * sqrt(1 - exp(-ε)) )
                  -- ε = ln x + (-δ)/x − ln(x−δ)
                  --   = ln (x / ((x−δ) · exp(δ/x)))
                  -- x/e^ε = (x−δ) · exp(δ/x)
@@ -1150,13 +1281,13 @@
   sqrt = postCompRW . RWDiffable $ \x -> if x>0
                                    then (positivePreRegion, pure (Differentiable sqrtPosR))
                                    else (negativePreRegion, notDefinedHere)
-   where sqrtPosR x = ( sx, id ^/ (2*sx), unsafe_dev_ε_δ("sqrt "++show x) $
+   where sqrtPosR x = ( sx, id ^/ (2*sx), unsafe_dev_ε_δ("sqrt "++showℝ x) $
                           \ε -> 2 * (s2 * sqrt sx^3 * sqrt ε + signum (ε*2-sx) * sx * ε) )
           where sx = sqrt x; s2 = sqrt 2
                  -- Exact inverse of O(δ²) remainder.
   
   sin = grwDfblFnValsFunc sinDfb
-   where sinDfb x = ( sx, cx *^ id, unsafe_dev_ε_δ("sin "++show x) δ )
+   where sinDfb x = ( sx, cx *^ id, unsafe_dev_ε_δ("sin "++showℝ x) δ )
           where sx = sin x; cx = cos x
                 sx² = sx^2; cx² = cx^2
                 sx' = abs sx; cx' = abs cx
@@ -1185,7 +1316,7 @@
   cosh x = (exp x + exp (-x))/2
   
   tanh = grwDfblFnValsFunc tanhDfb
-   where tanhDfb x = ( tnhx, id ^/ (cosh x^2), unsafe_dev_ε_δ("tan "++show x) δ )
+   where tanhDfb x = ( tnhx, id ^/ (cosh x^2), unsafe_dev_ε_δ("tan "++showℝ x) δ )
           where tnhx = tanh x
                 c = (tnhx*2/pi)^2
                 p = 1 + abs x/(2*pi)
@@ -1194,7 +1325,7 @@
                   -- with quite a big margin. TODO: find a tighter definition.
 
   atan = grwDfblFnValsFunc atanDfb
-   where atanDfb x = ( atnx, id ^/ (1+x^2), unsafe_dev_ε_δ("atan "++show x) δ )
+   where atanDfb x = ( atnx, id ^/ (1+x^2), unsafe_dev_ε_δ("atan "++showℝ x) δ )
           where atnx = atan x
                 c = (atnx*2/pi)^2
                 p = 1 + abs x/(2*pi)
@@ -1210,7 +1341,7 @@
                   | x < (-1)   -> (preRegionFromMinInfTo (-1), notDefinedHere)  
                   | x > 1      -> (preRegionToInfFrom 1, notDefinedHere)
                   | otherwise  -> (intervalPreRegion (-1,1), pure (Differentiable asinDefdR))
-   where asinDefdR x = ( asinx, asin'x *^ id, unsafe_dev_ε_δ("asin "++show x) δ )
+   where asinDefdR x = ( asinx, asin'x *^ id, unsafe_dev_ε_δ("asin "++showℝ x) δ )
           where asinx = asin x; asin'x = recip (sqrt $ 1 - x^2)
                 c = 1 - x^2 
                 δ ε = sqrt ε * c
@@ -1220,13 +1351,13 @@
                   | x < (-1)   -> (preRegionFromMinInfTo (-1), notDefinedHere)  
                   | x > 1      -> (preRegionToInfFrom 1, notDefinedHere)
                   | otherwise  -> (intervalPreRegion (-1,1), pure (Differentiable acosDefdR))
-   where acosDefdR x = ( acosx, acos'x *^ id, unsafe_dev_ε_δ("acos "++show x) δ )
+   where acosDefdR x = ( acosx, acos'x *^ id, unsafe_dev_ε_δ("acos "++showℝ x) δ )
           where acosx = acos x; acos'x = - recip (sqrt $ 1 - x^2)
                 c = 1 - x^2
                 δ ε = sqrt ε * c -- Like for asin – it's just a translation/reflection.
 
   asinh = grwDfblFnValsFunc asinhDfb
-   where asinhDfb x = ( asinhx, id ^/ sqrt(1+x^2), unsafe_dev_ε_δ("asinh "++show x) δ )
+   where asinhDfb x = ( asinhx, id ^/ sqrt(1+x^2), unsafe_dev_ε_δ("asinh "++showℝ x) δ )
           where asinhx = asinh x
                 δ ε = abs x * sqrt((1 - exp(-ε))*0.8 + ε^2/(3*abs x + 1)) + sqrt(ε/(abs x+0.5))
                  -- Empirical, modified from log function (the area hyperbolic sine
@@ -1235,7 +1366,7 @@
   acosh = postCompRW . RWDiffable $ \x -> if x>1
                                    then (preRegionToInfFrom 1, pure (Differentiable acoshDfb))
                                    else (preRegionFromMinInfTo 1, notDefinedHere)
-   where acoshDfb x = ( acosh x, id ^/ sqrt(x^2 - 1), unsafe_dev_ε_δ("acosh "++show x) δ )
+   where acoshDfb x = ( acosh x, id ^/ sqrt(x^2 - 1), unsafe_dev_ε_δ("acosh "++showℝ x) δ )
           where δ ε = (2 - 1/sqrt x) * (s2 * sqrt sx^3 * sqrt(ε/s2) + signum (ε*s2-sx) * sx * ε/s2) 
                 sx = sqrt(x-1)
                 s2 = sqrt 2
@@ -1246,7 +1377,7 @@
                   | x < (-1)   -> (preRegionFromMinInfTo (-1), notDefinedHere)  
                   | x > 1      -> (preRegionToInfFrom 1, notDefinedHere)
                   | otherwise  -> (intervalPreRegion (-1,1), pure (Differentiable atnhDefdR))
-   where atnhDefdR x = ( atanh x, recip(1-x^2) *^ id, unsafe_dev_ε_δ("atanh "++show x) $ \ε -> sqrt(tanh ε)*(1-abs x) )
+   where atnhDefdR x = ( atanh x, recip(1-x^2) *^ id, unsafe_dev_ε_δ("atanh "++showℝ x) $ \ε -> sqrt(tanh ε)*(1-abs x) )
                  -- Empirical, with epsEst upper bound.
   
 
@@ -1290,9 +1421,8 @@
 --   Just _ 'Control.Applicative.*>' a = a
 --   _      'Control.Applicative.*>' a = Nothing
 --   @
-(?->) :: ( RealDimension n, LocallyScalable n a, LocallyScalable n b, LocallyScalable n c
-         , Manifold b, Manifold c
-         , SimpleSpace (Needle b), SimpleSpace (Needle c) )
+(?->) :: ( RealDimension n, Object (Differentiable n) a, Object (Differentiable n) b
+         , Object (Differentiable n) c )
       => RWDfblFuncValue n c a -> RWDfblFuncValue n c b -> RWDfblFuncValue n c b
 ConstRWDFV _ ?-> f = f
 RWDFV_IdVar ?-> f = f
@@ -1318,12 +1448,12 @@
 --   allows chaining of comparison operators like in Python.)
 --   Note that less-than comparison is <http://www.paultaylor.eu/ASD/ equivalent>
 --   to less-or-equal comparison, because there is no such thing as equality.
-(?>) :: (RealDimension n, LocallyScalable n a, Manifold a, SimpleSpace (Needle a))
+(?>) :: ( RealDimension n, Object (Differentiable n) a, SimpleSpace (Needle a) )
            => RWDfblFuncValue n a n -> RWDfblFuncValue n a n -> RWDfblFuncValue n a n
 a ?> b = (positiveRegionalId $~ a-b) ?-> b
 
 -- | Return the RHS, if it is greater than the LHS.
-(?<) :: (RealDimension n, LocallyScalable n a, Manifold a, SimpleSpace (Needle a))
+(?<) :: ( RealDimension n, Object (Differentiable n) a, SimpleSpace (Needle a) )
            => RWDfblFuncValue n a n -> RWDfblFuncValue n a n -> RWDfblFuncValue n a n
 ConstRWDFV a ?< RWDFV_IdVar = GenericRWDFV . RWDiffable $
        \x₀ -> if a < x₀ then ( preRegionToInfFrom a
@@ -1346,9 +1476,7 @@
 --   @
 -- 
 --  Basically a weaker and agent-ised version of 'backupRegions'.
-(?|:) :: ( RealDimension n, LocallyScalable n a, LocallyScalable n b
-         , Manifold a, Manifold b
-         , SimpleSpace (Needle a), SimpleSpace (Needle b) )
+(?|:) :: ( RealDimension n, Object (Differentiable n) a, Object (Differentiable n) b )
       => RWDfblFuncValue n a b -> RWDfblFuncValue n a b -> RWDfblFuncValue n a b
 ConstRWDFV c ?|: _ = ConstRWDFV c
 RWDFV_IdVar ?|: _ = RWDFV_IdVar
@@ -1365,7 +1493,7 @@
 
 -- | Replace the regions in which the first function is undefined with values
 --   from the second function.
-backupRegions :: (RealDimension n, LocallyScalable n a, LocallyScalable n b)
+backupRegions :: (RealDimension n, Object (Differentiable n) a, Object (Differentiable n) b)
       => RWDiffable n a b -> RWDiffable n a b -> RWDiffable n a b
 backupRegions (RWDiffable f) (RWDiffable g) = RWDiffable h
  where h x₀ = case f x₀ of
@@ -1379,12 +1507,12 @@
 
 -- | Like 'Data.VectorSpace.lerp', but gives a differentiable function
 --   instead of a Hask one.
-lerp_diffable :: ∀ m s . ( LinearSpace m, Scalar m ~ s, Atlas m
-                         , HasTrie (ChartIndex m), RealDimension s )
+lerp_diffable :: ∀ m s . ( LinearSpace m, RealDimension s, Object (Differentiable s) m )
       => m -> m -> Differentiable s s m
-lerp_diffable = case ( linearManifoldWitness :: LinearManifoldWitness m
-                     , dualSpaceWitness :: DualSpaceWitness m ) of
-     (LinearManifoldWitness BoundarylessWitness, DualSpaceWitness)
+lerp_diffable = case ( linearManifoldWitness @m
+                     , dualSpaceWitness @m
+                     , smfdWBoundWitness @m) of
+     (LinearManifoldWitness, DualSpaceWitness, OpenManifoldWitness)
          -> \a b -> actuallyAffine a . arr $ flipBilin scale $ b.-.a
 
 
diff --git a/Data/Manifold/Atlas.hs b/Data/Manifold/Atlas.hs
--- a/Data/Manifold/Atlas.hs
+++ b/Data/Manifold/Atlas.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE ConstraintKinds           #-}
 {-# LANGUAGE FlexibleContexts          #-}
 {-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE UndecidableInstances      #-}
 {-# LANGUAGE EmptyDataDecls, EmptyCase #-}
 {-# LANGUAGE CPP                       #-}
 {-# LANGUAGE ScopedTypeVariables       #-}
@@ -23,6 +24,8 @@
 import Data.VectorSpace
 import Data.Manifold.PseudoAffine
 import Data.Manifold.Types.Primitive
+import Data.Manifold.WithBoundary
+import Data.Manifold.WithBoundary.Class
 
 import Data.Void
 
@@ -35,70 +38,63 @@
 
 import qualified Linear.Affine as LinAff
 
-class Semimanifold m => Atlas m where
+class SemimanifoldWithBoundary m => Atlas m where
   type ChartIndex m :: *
   chartReferencePoint :: ChartIndex m -> m
-  chartReferencePoint = fromInterior . interiorChartReferencePoint ([]::[m])
-  interiorChartReferencePoint :: Hask.Functor p => p m -> ChartIndex m -> Interior m
   lookupAtlas :: m -> ChartIndex m
 
 #define VectorSpaceAtlas(c,v)              \
 instance (c) => Atlas (v) where {           \
   type ChartIndex (v) = ();                  \
-  interiorChartReferencePoint _ () = zeroV;   \
   chartReferencePoint () = zeroV;              \
   lookupAtlas _ = () }
 
-VectorSpaceAtlas((), ZeroDim s)
+type NumPrime s = (Num' s, Eq s, OpenManifold s, ProjectableBoundary s)
+
+VectorSpaceAtlas(NumPrime s, ZeroDim s)
 VectorSpaceAtlas((), ℝ)
-VectorSpaceAtlas(Num s, V0 s)
-VectorSpaceAtlas(Num s, V1 s)
-VectorSpaceAtlas(Num s, V2 s)
-VectorSpaceAtlas(Num s, V3 s)
-VectorSpaceAtlas(Num s, V4 s)
-VectorSpaceAtlas((LinearSpace v, Scalar v ~ s, TensorSpace w, Scalar w ~ s), LinearMap s v w)
-VectorSpaceAtlas((TensorSpace v, Scalar v ~ s, TensorSpace w, Scalar w ~ s), Tensor s v w)
+VectorSpaceAtlas(NumPrime s, V0 s)
+VectorSpaceAtlas(NumPrime s, V1 s)
+VectorSpaceAtlas(NumPrime s, V2 s)
+VectorSpaceAtlas(NumPrime s, V3 s)
+VectorSpaceAtlas(NumPrime s, V4 s)
+VectorSpaceAtlas((NumPrime s, LinearSpace v, Scalar v ~ s, LinearSpace w, Scalar w ~ s), LinearMap s v w)
+VectorSpaceAtlas((NumPrime s, LinearSpace v, Scalar v ~ s, LinearSpace w, Scalar w ~ s), Tensor s v w)
 
-instance (Atlas x, Atlas y) => Atlas (x,y) where
+instance (Atlas x, Atlas y, SemimanifoldWithBoundary (x,y)) => Atlas (x,y) where
   type ChartIndex (x,y) = (ChartIndex x, ChartIndex y)
   chartReferencePoint = chartReferencePoint *** chartReferencePoint
-  interiorChartReferencePoint p
-         = interiorChartReferencePoint (fst<$>p) *** interiorChartReferencePoint (snd<$>p)
   lookupAtlas = lookupAtlas *** lookupAtlas
 
 instance Atlas S⁰ where
   type ChartIndex S⁰ = S⁰
   chartReferencePoint = id
-  interiorChartReferencePoint _ = id
   lookupAtlas = id
 instance Atlas S¹ where
   type ChartIndex S¹ = S⁰
   chartReferencePoint NegativeHalfSphere = S¹Polar $ -pi/2
   chartReferencePoint PositiveHalfSphere = S¹Polar $ pi/2
-  interiorChartReferencePoint _ NegativeHalfSphere = S¹Polar $ -pi/2
-  interiorChartReferencePoint _ PositiveHalfSphere = S¹Polar $ pi/2
   lookupAtlas (S¹Polar φ) | φ<0        = NegativeHalfSphere
                      | otherwise  = PositiveHalfSphere
 instance Atlas S² where
   type ChartIndex S² = S⁰
   chartReferencePoint PositiveHalfSphere = S²Polar 0 0
   chartReferencePoint NegativeHalfSphere = S²Polar pi 0
-  interiorChartReferencePoint _ PositiveHalfSphere = S²Polar 0 0
-  interiorChartReferencePoint _ NegativeHalfSphere = S²Polar pi 0
   lookupAtlas (S²Polar ϑ _) | ϑ<pi/2     = PositiveHalfSphere
                             | otherwise  = NegativeHalfSphere
 
-instance (LinearSpace (a n), Needle (a n) ~ a n, Interior (a n) ~ a n)
+instance (Num'' n, LinearManifold (a n), Scalar (a n) ~ n, Needle (a n) ~ a n)
               => Atlas (LinAff.Point a n) where
   type ChartIndex (LinAff.Point a n) = ()
-  interiorChartReferencePoint _ () = LinAff.P zeroV
+  chartReferencePoint () = LinAff.P zeroV
   lookupAtlas _ = ()
 
+type Atlas' m = (Atlas m, HasTrie (ChartIndex m))
 
 
 -- | The 'AffineSpace' class plus manifold constraints.
-type AffineManifold m = ( Atlas m, Manifold m, AffineSpace m
-                        , Needle m ~ Diff m, HasTrie (ChartIndex m) )
+type AffineManifold m = ( Atlas' m, Manifold m, AffineSpace m
+                        , Needle m ~ Diff m )
 
 -- | An euclidean space is a real affine space whose tangent space is a Hilbert space.
 type EuclidSpace x = ( AffineManifold x, InnerSpace (Diff x)
diff --git a/Data/Manifold/Cone.hs b/Data/Manifold/Cone.hs
--- a/Data/Manifold/Cone.hs
+++ b/Data/Manifold/Cone.hs
@@ -19,6 +19,7 @@
 {-# LANGUAGE TupleSections            #-}
 {-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE PatternGuards            #-}
+{-# LANGUAGE EmptyCase                #-}
 {-# LANGUAGE TypeOperators            #-}
 {-# LANGUAGE UnicodeSyntax            #-}
 {-# LANGUAGE MultiWayIf               #-}
@@ -37,6 +38,8 @@
 import Data.VectorSpace
 import Data.Tagged
 import Data.Manifold.Types.Primitive
+import Math.Manifold.Core.Types
+import Data.Manifold.WithBoundary
 import Data.Manifold.Types.Stiefel
 import Math.LinearMap.Category
 
@@ -50,60 +53,53 @@
 
 import Data.Manifold.PseudoAffine
 
+import Data.Kind (Type)
 
 
-newtype ConeVecArr m = ConeVecArr {getConeVecArr :: CℝayInterior m}
-type ConeNeedle m = Needle (ConeVecArr m)
-data SConn'dConeVecArr m = SConn'dConeVecArr ℝ (Interior m)
 
-
-class ( Semimanifold m, Semimanifold (Interior (Interior m))
-      , Semimanifold (ConeVecArr m)
-      , Interior (ConeVecArr m) ~ ConeVecArr m )
-           => ConeSemimfd m where
-  {-# MINIMAL (fromCℝayInterior | fromCD¹Interior)
-            , (toCℝayInterior | toCD¹Interior) #-}
-  type CℝayInterior m :: *
-  
-  fromCℝayInterior :: ConeVecArr m -> Cℝay m
-  fromCℝayInterior = projCD¹ToCℝay . fromCD¹Interior
-  fromCD¹Interior :: ConeVecArr m -> CD¹ m
-  fromCD¹Interior = embCℝayToCD¹ . fromCℝayInterior
-  
-  toCℝayInterior :: Cℝay m -> Maybe (ConeVecArr m)
-  toCℝayInterior = toCD¹Interior . embCℝayToCD¹
-  toCD¹Interior :: CD¹ m -> Maybe (ConeVecArr m)
-  toCD¹Interior = toCℝayInterior . projCD¹ToCℝay
-
-  
-
+instance SemimanifoldWithBoundary (CD¹ ℝ⁰) where
+  type Interior (CD¹ ℝ⁰) = ℝ
+  type Boundary (CD¹ ℝ⁰) = S⁰
+  type HalfNeedle (CD¹ ℝ⁰) = ℝay
+  smfdWBoundWitness = SmfdWBoundWitness
+  fromInterior l = CD¹ (bijectℝtoIntvplus l) Origin
+  separateInterior (CD¹ 0 Origin) = Left NegativeHalfSphere
+  separateInterior (CD¹ 1 Origin) = Left PositiveHalfSphere
+  separateInterior (CD¹ ρ Origin) = Right $ bijectIntvplustoℝ ρ
+  NegativeHalfSphere |+^ Cℝay a Origin = CD¹ (bijectℝplustoIntv a) Origin
+  extendToBoundary l a
+   | a<0        = Just NegativeHalfSphere
+   | a>0        = Just PositiveHalfSphere
+   | otherwise  = Nothing
 
+instance SemimanifoldWithBoundary ℝay where
+  type Interior ℝay = ℝ
+  type Boundary ℝay = ℝ⁰
+  type HalfNeedle ℝay = ℝay
+  Cℝay ρ Origin .+^| w
+   | ρ >= -w    = Right $ ρ+w
+   | otherwise  = Left (Origin, (ρ+w)/w)
+  fromInterior l = Cℝay (bijectℝtoℝplus l) Origin
+  fromBoundary Origin = Cℝay 0 Origin
+  separateInterior (Cℝay ρ Origin)
+   | ρ>0        = Right $ bijectℝplustoℝ ρ
+   | otherwise  = Left Origin
+  Origin |+^ a = a
+  extendToBoundary l a
+   | a<0        = Just Origin
+   | otherwise  = Nothing
 
-instance ∀ m . (ConeSemimfd m) => Semimanifold (Cℝay m) where
-  type Needle (Cℝay m) = ConeNeedle m
-  type Interior (Cℝay m) = ConeVecArr m
-  fromInterior = fromCℝayInterior
-  toInterior = toCℝayInterior
-  translateP = ctp
-   where ctp :: Tagged (Cℝay m) (ConeVecArr m -> ConeNeedle m -> ConeVecArr m)
-         ctp = Tagged ctp'
-          where Tagged ctp' = translateP
-                  :: Tagged (ConeVecArr m) (ConeVecArr m -> ConeNeedle m -> ConeVecArr m)
-  semimanifoldWitness = case semimanifoldWitness :: SemimanifoldWitness (ConeVecArr m) of
-       SemimanifoldWitness BoundarylessWitness -> SemimanifoldWitness BoundarylessWitness
-  
-instance (ConeSemimfd m) => Semimanifold (CD¹ m) where
-  type Needle (CD¹ m) = ConeNeedle m
-  type Interior (CD¹ m) = ConeVecArr m
-  fromInterior = fromCD¹Interior
-  toInterior = toCD¹Interior
-  translateP = ctp
-   where ctp :: Tagged (CD¹ m) (ConeVecArr m -> ConeNeedle m -> ConeVecArr m)
-         ctp = Tagged ctp'
-          where Tagged ctp' = translateP
-                  :: Tagged (ConeVecArr m) (ConeVecArr m -> ConeNeedle m -> ConeVecArr m)
-  semimanifoldWitness = case semimanifoldWitness :: SemimanifoldWitness (ConeVecArr m) of
-       SemimanifoldWitness BoundarylessWitness -> SemimanifoldWitness BoundarylessWitness
+instance SemimanifoldWithBoundary (Cℝay S⁰) where
+  type Interior (Cℝay S⁰) = ℝ
+  type Boundary (Cℝay S⁰) = EmptyMfd ℝ⁰
+  type HalfNeedle (Cℝay S⁰) = ℝay
+  fromInterior l
+   | l<0        = Cℝay l PositiveHalfSphere
+   | otherwise  = Cℝay (-l) NegativeHalfSphere
+  separateInterior (Cℝay ρ PositiveHalfSphere) = Right ρ
+  separateInterior (Cℝay ρ NegativeHalfSphere) = Right $ -ρ
+  b |+^ _ = case b of {}
+  extendToBoundary _ _ = Nothing 
 
 
 
@@ -117,7 +113,8 @@
 bijectℝtoℝplus      , bijectℝplustoℝ
  , bijectIntvtoℝplus, bijectℝplustoIntv
  ,     bijectIntvtoℝ, bijectℝtoIntv
-               :: ℝ -> ℝ
+ , bijectIntvplustoℝ, bijectℝtoIntvplus
+               :: RealFloat r => r -> r
 
 bijectℝplustoℝ x = x - 1/x
 bijectℝtoℝplus y = y/2 + sqrt(y^2/4 + 1)
@@ -134,10 +131,14 @@
                  -- x = -1/2y ± sqrt(1/4y² + 1)
 bijectIntvtoℝ x = x / (1-x^2)
 
-embCℝayToCD¹ :: Cℝay m -> CD¹ m
+-- ]0, 1[ ↔ ℝ
+bijectℝtoIntvplus y = (bijectℝtoIntv y + 1)/2
+bijectIntvplustoℝ x = bijectIntvtoℝ $ x*2 - 1
+
+embCℝayToCD¹ :: RealFloat (Scalar (Needle m)) => Cℝay m -> CD¹ m
 embCℝayToCD¹ (Cℝay h m) = CD¹ (bijectℝplustoIntv h) m
 
-projCD¹ToCℝay :: CD¹ m -> Cℝay m
+projCD¹ToCℝay :: RealFloat (Scalar (Needle m)) => CD¹ m -> Cℝay m
 projCD¹ToCℝay (CD¹ h m) = Cℝay (bijectIntvtoℝplus h) m
 
 
diff --git a/Data/Manifold/DifferentialEquation.hs b/Data/Manifold/DifferentialEquation.hs
--- a/Data/Manifold/DifferentialEquation.hs
+++ b/Data/Manifold/DifferentialEquation.hs
@@ -102,8 +102,8 @@
                        , dualSpaceWitness :: DualSpaceWitness x
                        , linearManifoldWitness :: LinearManifoldWitness y
                        , dualSpaceWitness :: DualSpaceWitness y ) of
-   ( LinearManifoldWitness BoundarylessWitness, DualSpaceWitness
-    ,LinearManifoldWitness BoundarylessWitness, DualSpaceWitness ) -> \bwt'inv bwt' ->
+   ( LinearManifoldWitness, DualSpaceWitness
+    ,LinearManifoldWitness, DualSpaceWitness ) -> \bwt'inv bwt' ->
         \(Shade (_x,y) δxy) -> LocalDifferentialEqn
          { _rescanDifferentialEqn
             = \(QuadraticModel shy' shj'Apriori _) ->
@@ -128,8 +128,8 @@
                       , dualSpaceWitness :: DualSpaceWitness x
                       , linearManifoldWitness :: LinearManifoldWitness y
                       , dualSpaceWitness :: DualSpaceWitness y ) of
-   ( LinearManifoldWitness BoundarylessWitness, DualSpaceWitness
-    ,LinearManifoldWitness BoundarylessWitness, DualSpaceWitness ) -> \bwt' ->
+   ( LinearManifoldWitness, DualSpaceWitness
+    ,LinearManifoldWitness, DualSpaceWitness ) -> \bwt' ->
     let bwt'inv = pseudoInverse bwt'
     in \(Shade (_x,y) δxy) -> LocalDifferentialEqn
             (\(QuadraticModel shy' _ _) ->
diff --git a/Data/Manifold/FibreBundle.hs b/Data/Manifold/FibreBundle.hs
--- a/Data/Manifold/FibreBundle.hs
+++ b/Data/Manifold/FibreBundle.hs
@@ -14,6 +14,7 @@
 {-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE UndecidableInstances       #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE UnicodeSyntax              #-}
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE DefaultSignatures          #-}
@@ -42,8 +43,7 @@
 import Control.Category.Discrete
 import Control.Arrow.Constrained
 
-import Linear.V2 (V2(V2))
-import Linear.V3 (V3(V3))
+import Linear (V2(V2), V3(V3), V4(V4))
 
 import Data.Tagged
 
@@ -59,7 +59,7 @@
 
 -- | A zero vector in the fibre bundle at the given position. Intended to be used
 --   with tangent-modifying lenses such as 'Math.Manifold.Real.Coordinates.delta'.
-tangentAt :: (AdditiveGroup (Needle m), m ~ Interior m) => m -> TangentBundle m
+tangentAt :: (AdditiveGroup (Needle m)) => m -> TangentBundle m
 tangentAt p = zeroV :@. p
 
 data TransportOnNeedleWitness k m f where
@@ -71,7 +71,7 @@
   ForgetTransportProperties :: ParallelTransporting (->) m f
                      => ForgetTransportProperties k m f
 
-class (PseudoAffine m, m ~ Interior m, Category k, Object k f)
+class (PseudoAffine m, Category k, Object k f)
            => ParallelTransporting k m f where
   transportOnNeedleWitness :: TransportOnNeedleWitness k m f
   default transportOnNeedleWitness
@@ -91,28 +91,28 @@
                     , parallelTransport q $ p.-~!q ))
    where q = p.+~^v
 
-instance ∀ m s . (PseudoAffine m, m ~ Interior m, s ~ (Scalar (Needle m)), Num' s)
+instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
       => ParallelTransporting Discrete m (ZeroDim s) where
   transportOnNeedleWitness = case (pseudoAffineWitness :: PseudoAffineWitness m) of
-    (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)) -> TransportOnNeedle
+    (PseudoAffineWitness (SemimanifoldWitness)) -> TransportOnNeedle
   forgetTransportProperties = case (pseudoAffineWitness :: PseudoAffineWitness m) of
-    (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness))
+    (PseudoAffineWitness (SemimanifoldWitness))
         -> ForgetTransportProperties
   parallelTransport _ _ = id
-instance ∀ m s . (PseudoAffine m, m ~ Interior m, s ~ (Scalar (Needle m)), Num' s)
+instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
       => ParallelTransporting (LinearFunction s) m (ZeroDim s) where
   transportOnNeedleWitness = case (pseudoAffineWitness :: PseudoAffineWitness m) of
-    (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)) -> TransportOnNeedle
+    (PseudoAffineWitness (SemimanifoldWitness)) -> TransportOnNeedle
   forgetTransportProperties = case (pseudoAffineWitness :: PseudoAffineWitness m) of
-    (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness))
+    (PseudoAffineWitness (SemimanifoldWitness))
         -> ForgetTransportProperties
   parallelTransport _ _ = id
-instance ∀ m s . (PseudoAffine m, m ~ Interior m, s ~ (Scalar (Needle m)), Num' s)
+instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
       => ParallelTransporting (->) m (ZeroDim s) where
   transportOnNeedleWitness = case (pseudoAffineWitness :: PseudoAffineWitness m) of
-    (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)) -> TransportOnNeedle
+    (PseudoAffineWitness (SemimanifoldWitness)) -> TransportOnNeedle
   forgetTransportProperties = case (pseudoAffineWitness :: PseudoAffineWitness m) of
-    (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness))
+    (PseudoAffineWitness (SemimanifoldWitness))
         -> ForgetTransportProperties
   parallelTransport _ _ = id
 
@@ -215,10 +215,10 @@
          , pseudoAffineWitness :: PseudoAffineWitness fb
          , transportOnNeedleWitness :: TransportOnNeedleWitness k a fa
          , transportOnNeedleWitness :: TransportOnNeedleWitness k b fb ) of
-     ( PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-      ,PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-      ,PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-      ,PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
+     ( PseudoAffineWitness (SemimanifoldWitness)
+      ,PseudoAffineWitness (SemimanifoldWitness)
+      ,PseudoAffineWitness (SemimanifoldWitness)
+      ,PseudoAffineWitness (SemimanifoldWitness)
       ,TransportOnNeedle, TransportOnNeedle)
          -> TransportOnNeedle
   forgetTransportProperties = case
@@ -240,9 +240,9 @@
          , pseudoAffineWitness :: PseudoAffineWitness g
          , transportOnNeedleWitness :: TransportOnNeedleWitness k a f
          , transportOnNeedleWitness :: TransportOnNeedleWitness k a g ) of
-     ( PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-      ,PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-      ,PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
+     ( PseudoAffineWitness (SemimanifoldWitness)
+      ,PseudoAffineWitness (SemimanifoldWitness)
+      ,PseudoAffineWitness (SemimanifoldWitness)
       ,TransportOnNeedle, TransportOnNeedle)
          -> TransportOnNeedle
   forgetTransportProperties = case
@@ -261,31 +261,24 @@
   negateV (FibreBundle p v) = FibreBundle (negateV p) (negateV v)
 
 instance ∀ m f s .
-         ( ParallelTransporting (->) m (Interior f), Semimanifold f
+         ( ParallelTransporting (->) m f, Semimanifold f
          , ParallelTransporting (LinearFunction s) (Needle m) (Needle f)
          , s ~ Scalar (Needle m) )
                 => Semimanifold (FibreBundle m f) where
-  type Interior (FibreBundle m f) = FibreBundle m (Interior f)
   type Needle (FibreBundle m f) = FibreBundle (Needle m) (Needle f)
-  toInterior (FibreBundle p f) = FibreBundle p <$> toInterior f
-  translateP = Tagged $ case ( translateP :: Tagged m (Interior m -> Needle m -> Interior m)
-                             , semimanifoldWitness :: SemimanifoldWitness f) of
-      (Tagged tpm, SemimanifoldWitness BoundarylessWitness)
-           -> \(FibreBundle p f) (FibreBundle v δf)
-                   -> FibreBundle (tpm p v) (parallelTransport p v f.+~^δf)
   semimanifoldWitness = case ( semimanifoldWitness :: SemimanifoldWitness m
                              , semimanifoldWitness :: SemimanifoldWitness f
                              , forgetTransportProperties
                                :: ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
                              ) of
-         (SemimanifoldWitness BoundarylessWitness, SemimanifoldWitness BoundarylessWitness
+         (SemimanifoldWitness, SemimanifoldWitness
           ,ForgetTransportProperties)
-           -> SemimanifoldWitness BoundarylessWitness
+           -> SemimanifoldWitness
   FibreBundle p f .+~^ FibreBundle v δf
       = FibreBundle (p.+~^v) (parallelTransport p v f.+~^δf)
 
 instance ∀ m f s .
-         ( ParallelTransporting (->) m f, ParallelTransporting (->) m (Interior f)
+         ( ParallelTransporting (->) m f
          , PseudoAffine f
          , ParallelTransporting (LinearFunction s) (Needle m) (Needle f)
          , s ~ Scalar (Needle m) )
@@ -295,21 +288,23 @@
                              , forgetTransportProperties
                                :: ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
                              ) of
-     ( PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-      ,PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
+     ( PseudoAffineWitness (SemimanifoldWitness)
+      ,PseudoAffineWitness (SemimanifoldWitness)
       ,ForgetTransportProperties)
-         -> PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
+         -> PseudoAffineWitness (SemimanifoldWitness)
+  FibreBundle p f .-~! FibreBundle q g = case p.-~!q of
+      v  -> FibreBundle v $ f .-~! parallelTransport p v g
   FibreBundle p f .-~. FibreBundle q g = case p.-~.q of
       Nothing -> Nothing
       Just v  -> FibreBundle v <$> f .-~. parallelTransport p v g
 
 
-instance (AdditiveGroup f, x ~ Interior x) => NaturallyEmbedded x (FibreBundle x f) where
+instance (AdditiveGroup f) => NaturallyEmbedded x (FibreBundle x f) where
   embed x = FibreBundle x zeroV
   coEmbed (FibreBundle x _) = x
 
 instance (NaturallyEmbedded m v, VectorSpace f)
-    => NaturallyEmbedded (FibreBundle m ℝ⁰) (FibreBundle v f) where
+    => NaturallyEmbedded (FibreBundle m (ZeroDim s)) (FibreBundle v f) where
   embed (FibreBundle x Origin) = FibreBundle (embed x) zeroV
   coEmbed (FibreBundle u _) = FibreBundle (coEmbed u) Origin
 
@@ -322,20 +317,21 @@
       => NaturallyEmbedded (FibreBundle ℝ v) (FibreBundle ℝ w) where
   embed (FibreBundle p v) = FibreBundle p $ embed v
   coEmbed (FibreBundle p w) = FibreBundle p $ coEmbed w
-instance NaturallyEmbedded v w
-      => NaturallyEmbedded (FibreBundle ℝ² v) (FibreBundle ℝ² w) where
+instance (NaturallyEmbedded v w, s'~s)
+      => NaturallyEmbedded (FibreBundle (V2 s) v) (FibreBundle (V2 s') w) where
   embed (FibreBundle p v) = FibreBundle p $ embed v
   coEmbed (FibreBundle p w) = FibreBundle p $ coEmbed w
-instance NaturallyEmbedded v w
-      => NaturallyEmbedded (FibreBundle ℝ³ v) (FibreBundle ℝ³ w) where
+instance (NaturallyEmbedded v w, s'~s)
+      => NaturallyEmbedded (FibreBundle (V3 s) v) (FibreBundle (V3 s') w) where
   embed (FibreBundle p v) = FibreBundle p $ embed v
   coEmbed (FibreBundle p w) = FibreBundle p $ coEmbed w
-instance NaturallyEmbedded v w
-      => NaturallyEmbedded (FibreBundle ℝ⁴ v) (FibreBundle ℝ⁴ w) where
+instance (NaturallyEmbedded v w, s'~s)
+      => NaturallyEmbedded (FibreBundle (V4 s) v) (FibreBundle (V4 s') w) where
   embed (FibreBundle p v) = FibreBundle p $ embed v
   coEmbed (FibreBundle p w) = FibreBundle p $ coEmbed w
 
-instance NaturallyEmbedded (FibreBundle S¹ ℝ) (FibreBundle ℝ² ℝ²) where
+instance (RealFloat s, InnerSpace s, s~s', s~s'', s~s''')
+      => NaturallyEmbedded (FibreBundle (S¹_ s) s') (FibreBundle (V2 s'') (V2 s''')) where
   embed (FibreBundle (S¹Polar φ) l) = FibreBundle (V2 cφ sφ) $ l*^(V2 (-sφ) cφ)
    where (cφ, sφ) = (cos &&& sin) φ
   coEmbed (FibreBundle (V2 0 0) (V2 _ δy)) = FibreBundle (S¹Polar 0) δy
@@ -343,14 +339,15 @@
    where V2 cφ sφ = p^/r
          r = magnitude p
 
-instance NaturallyEmbedded (FibreBundle S² ℝ²) (FibreBundle ℝ³ ℝ³) where
-  embed (FibreBundle (S²Polar θ φ) 𝐯@(V2 δξ δυ))
+instance ∀ s s' s'' s''' . (RealFloat' s, InnerSpace s, s~s', s~s'', s~s''')
+   => NaturallyEmbedded (FibreBundle (S²_ s) (V2 s')) (FibreBundle (V3 s'') (V3 s''')) where
+  embed (FibreBundle (S²Polar θ φ) v@(V2 δξ δυ))
        = FibreBundle (V3 (sθ*cφ) (sθ*sφ) cθ) 𝐯r
    where [V2 cθ sθ, V2 cφ sφ] = embed . S¹Polar <$> [θ,φ]
-         S¹Polar γc = coEmbed 𝐯
+         S¹Polar γc = coEmbed v
          γ | θ < pi/2   = γc - φ
            | otherwise  = γc + φ
-         d = magnitude 𝐯
+         d = magnitude v
 
          V2 δθ δφ = d *^ embed (S¹Polar γ)
          
@@ -358,35 +355,35 @@
          𝐞θ = V3 (cθ*cφ) (cθ*sφ) (-sθ)
          𝐯r = δθ*^𝐞θ ^+^ δφ*^𝐞φ
   
-  coEmbed (FibreBundle (V3 x y z) 𝐯r)
-           = FibreBundle (S²Polar θ φ) (magnitude (δθ,δφ) *^ embed (S¹Polar γc))
-   where r = sqrt $ x^2 + y^2 + z^2
-         rxy = sqrt $ x^2 + y^2
-         θ = atan2 rxy z
-         φ = atan2 y x
-         cθ = z / r
-         sθ = rxy / r
-         (cφ,sφ) | rxy>0      = (x,y)^/rxy
-                 | otherwise  = (1,0)
-         𝐞φ = V3 (-sφ) cφ 0
-         𝐞θ = V3 (cθ*cφ) (cθ*sφ) (-sθ)
-         δθ = 𝐞θ <.> 𝐯r
-         δφ = 𝐞φ <.> 𝐯r
-         γ = atan2 δφ δθ
-         γc | θ < pi/2   = γ + φ
-            | otherwise  = γ - φ
+  coEmbed (FibreBundle (V3 x y z) 𝐯r) = case closedScalarWitness @s of
+   ClosedScalarWitness -> FibreBundle (S²Polar θ φ) (magnitude (δθ,δφ) *^ embed (S¹Polar γc))
+     where r = sqrt $ x^2 + y^2 + z^2
+           rxy = sqrt $ x^2 + y^2
+           θ = atan2 rxy z
+           φ = atan2 y x
+           cθ = z / r
+           sθ = rxy / r
+           (cφ,sφ) | rxy>0      = (x,y)^/rxy
+                   | otherwise  = (1,0)
+           𝐞φ = V3 (-sφ) cφ 0
+           𝐞θ = V3 (cθ*cφ) (cθ*sφ) (-sθ)
+           δθ = 𝐞θ <.> 𝐯r
+           δφ = 𝐞φ <.> 𝐯r
+           γ = atan2 δφ δθ
+           γc | θ < pi/2   = γ + φ
+              | otherwise  = γ - φ
 
 
 -- | @ex -> ey@, @ey -> ez@, @ez -> ex@
 transformEmbeddedTangents
-    :: ∀ x f v . ( NaturallyEmbedded (FibreBundle x f) (FibreBundle v v)
-                               , v ~ Interior v )
+    :: ∀ x f v . ( NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) )
            => (v -> v) -> FibreBundle x f -> FibreBundle x f
 transformEmbeddedTangents f p = case embed p :: FibreBundle v v of
     FibreBundle v δv -> coEmbed (FibreBundle (f v) (f δv) :: FibreBundle v v)
 
 
-instance Rotatable (FibreBundle S² ℝ²) where
-  type AxisSpace (FibreBundle S² ℝ²) = ℝP²
-  rotateAbout axis angle = transformEmbeddedTangents $ rotateℝ³AboutCenteredAxis axis angle
+instance (s~ℝ, s'~ℝ) => Rotatable (FibreBundle (S²_ s) (V2 s')) where
+  type AxisSpace (FibreBundle (S²_ s) (V2 s')) = ℝP²_ s
+  rotateAbout axis angle = transformEmbeddedTangents
+        $ rotateℝ³AboutCenteredAxis axis angle
 
diff --git a/Data/Manifold/Function/Interpolation.hs b/Data/Manifold/Function/Interpolation.hs
--- a/Data/Manifold/Function/Interpolation.hs
+++ b/Data/Manifold/Function/Interpolation.hs
@@ -76,7 +76,7 @@
         where localModel = nd^.dataAtNode.thisNodeData
               newNorm = spanNorm
                   [ dx ^/ ((0.1 + occlusion (ngb^.thisNodeData.tweakLocalOffset)
-                                            (fromInterior ySynth))
+                                            ySynth)
                            * (dx<.>^δx))
                   | (δx,ngb) <- concat . take 2 $ localOnion (nd^.dataAtNode) []
                   , let dx = nd^.localScalarProduct<$|δx
@@ -88,14 +88,14 @@
         => ℝ -> (x -> ㄇ x y -> Needle x -> Shade' y)
             -> InterpolationFunction ㄇ x y -> PointsWeb x (Shade' y)
 upsampleAtLargeDist dmax gapFillFunc (InterpolationFunction web)
-     = fromWebNodes (\(Shade x _) -> case nearestNeighbour webI (fromInterior x) of
+     = fromWebNodes (\(Shade x _) -> case nearestNeighbour webI x of
                          Just (_,nearest) -> nearest ^. nodeLocalScalarProduct) $ do
           local <- toList webI
           (local^.thisNodeCoord, evalLocalModel (local^.thisNodeData) zeroV) : do 
              (ngId, (δx, ngb)) <- local^.nodeNeighbours
              guard (ngId > local^.thisNodeId
                    && (local^.nodeLocalScalarProduct|$|δx) > dmax)
-             return ( local^.thisNodeCoord !+~^ δx^/2
+             return ( local^.thisNodeCoord .+~^ δx^/2
                     , gapFillFunc (local^.thisNodeCoord)
                                   (local^.thisNodeData)
                                   (δx^/2) )
diff --git a/Data/Manifold/Function/LocalModel.hs b/Data/Manifold/Function/LocalModel.hs
--- a/Data/Manifold/Function/LocalModel.hs
+++ b/Data/Manifold/Function/LocalModel.hs
@@ -31,13 +31,12 @@
     -- ** Differential equations
     , DifferentialEqn, LocalDifferentialEqn(..)
     , propagateDEqnSolution_loc, LocalDataPropPlan(..)
-    -- ** Range interpolation
-    , rangeWithinVertices
     ) where
 
 
 import Data.Manifold.Types
 import Data.Manifold.PseudoAffine
+import Data.Manifold.WithBoundary
 import Data.Manifold.Types.Primitive ((^))
 import Data.Manifold.Shade
 import Data.Manifold.Riemannian
@@ -66,12 +65,12 @@
 type DifferentialEqn ㄇ x y = Shade (x,y) -> LocalDifferentialEqn ㄇ x y
 
 data LocalDataPropPlan x y = LocalDataPropPlan
-       { _sourcePosition :: !(Interior x)
+       { _sourcePosition :: !x
        , _targetPosOffset :: !(Needle x)
        , _sourceData, _targetAPrioriData :: !y
        , _relatedData :: [(Needle x, y)]
        }
-deriving instance (Show (Interior x), Show y, Show (Needle x))
+deriving instance (Show x, Show y, Show (Needle x))
              => Show (LocalDataPropPlan x y)
 
 makeLenses ''LocalDataPropPlan
@@ -84,8 +83,8 @@
                              -> Maybe (Shade' (LocalLinear x y))
 estimateLocalJacobian = elj ( pseudoAffineWitness :: PseudoAffineWitness x
                             , pseudoAffineWitness :: PseudoAffineWitness y )
- where elj ( PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-           , PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness) )
+ where elj ( PseudoAffineWitness SemimanifoldWitness
+           , PseudoAffineWitness SemimanifoldWitness )
         mex [(Local x₁, Shade' y₁ ey₁),(Local x₀, Shade' y₀ ey₀)]
          = return $ Shade' (dx-+|>δy)
                           (Norm . LinearFunction $ \δj -> δx ⊗ (σey<$|δj $ δx))
@@ -127,7 +126,7 @@
 
 
 
-quadratic_linearRegression :: ∀ s x y .
+quadratic_linearRegression :: ∀ x y s .
                       ( WithField s PseudoAffine x
                       , WithField s PseudoAffine y, Geodesic y
                       , SimpleSpace (Needle x), SimpleSpace (Needle y) )
@@ -138,22 +137,22 @@
          (\δx -> lfun $ \(c,(b,a)) -> (a $ squareV δx) ^+^ (b $ δx) ^+^ c )
          (\cmy (cBest, (bBest, aBest)) σ
             -> let (σc, (σb, σa)) = second summandSpaceNorms $ summandSpaceNorms σ
-               in QuadraticModel (Shade (cmy⊙+^cBest $ ([]::[y])) σc)
+               in QuadraticModel (Shade (cmy.+~^cBest) σc)
                               (Shade bBest σb)
                               (Shade aBest σa) )
 
-gLinearRegression :: ∀ s x y ㄇ ψ.
+gLinearRegression :: ∀ x y ㄇ ψ s .
                       ( WithField s PseudoAffine x
                       , WithField s PseudoAffine y, Geodesic y
                       , SimpleSpace (Needle x), SimpleSpace (Needle y)
                       , SimpleSpace ψ, Scalar ψ ~ s )
             => (Needle x -> ψ -+> Needle y)
-               -> (Interior y -> ψ -> Variance ψ -> ㄇ x y)
+               -> (y -> ψ -> Variance ψ -> ㄇ x y)
                -> NE.NonEmpty (Needle x, Shade' y) -> ㄇ x y
-gLinearRegression fwdCalc analyse = qlr (pseudoAffineWitness, geodesicWitness)
- where qlr :: (PseudoAffineWitness y, GeodesicWitness y)
+gLinearRegression fwdCalc analyse = qlr (pseudoAffineWitness)
+ where qlr :: (PseudoAffineWitness y)
                    -> NE.NonEmpty (Needle x, Shade' y) -> ㄇ x y
-       qlr (PseudoAffineWitness (SemimanifoldWitness _), GeodesicWitness _) ps
+       qlr (PseudoAffineWitness SemimanifoldWitness) ps
                  = analyse cmy ψ σψ
         where Just cmy = pointsBarycenter $ _shade'Ctr.snd<$>ps
               Just vsxy = Hask.mapM (\(x, Shade' y ey) -> (x,).(,ey)<$>y.-~.cmy) ps
@@ -177,7 +176,7 @@
           , Scalar (Needle y) ~ Scalar (Needle x) ) =>
      QuadraticModel x y -> (Shade' y, (Shade' (LocalLinear x y), Shade' (LocalBilinear x y))) 
 quadraticModel_derivatives (QuadraticModel sh shð shð²)
-    | (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness))
+    | (PseudoAffineWitness SemimanifoldWitness)
                                      :: PseudoAffineWitness y <- pseudoAffineWitness
     , DualSpaceWitness :: DualSpaceWitness (Needle x) <- dualSpaceWitness
     , DualSpaceWitness :: DualSpaceWitness (Needle y) <- dualSpaceWitness
@@ -218,12 +217,9 @@
 propagateDEqnSolution_loc f propPlan
                   = pdesl (dualSpaceWitness :: DualNeedleWitness x)
                           (dualSpaceWitness :: DualNeedleWitness y)
-                          (boundarylessWitness :: BoundarylessWitness x)
                           (pseudoAffineWitness :: PseudoAffineWitness y)
-                          (geodesicWitness :: GeodesicWitness y)
- where pdesl DualSpaceWitness DualSpaceWitness BoundarylessWitness
-             (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness))
-             (GeodesicWitness _)
+ where pdesl DualSpaceWitness DualSpaceWitness
+             (PseudoAffineWitness SemimanifoldWitness)
           | Nothing <- jacobian  = Nothing
           | otherwise            = pure result
          where (_,jacobian) = f shxy ^. rescanDifferentialEqn
@@ -288,7 +284,7 @@
                             (\δx -> lfun $ \(b,a) -> (a $ δx) ^+^ b )
                             (\cmy (bBest, aBest) σ
                                -> let (σb, σa) = summandSpaceNorms σ
-                                  in AffineModel (Shade (cmy⊙+^bBest $ ([]::[y]))
+                                  in AffineModel (Shade (cmy.+~^bBest)
                                                         $ scaleNorm 2 σb)
                                -- The magic factor 2 seems dubious ↗, but testing indicates
                                -- that this is necessary to not overrate the accuracy.
@@ -300,7 +296,7 @@
   evalLocalModel = aEvL pseudoAffineWitness
    where aEvL :: ∀ x y . ModellableRelation x y
                 => PseudoAffineWitness y -> AffineModel x y -> Needle x -> Shade' y
-         aEvL (PseudoAffineWitness (SemimanifoldWitness _)) (AffineModel shy₀ shj) δx
+         aEvL (PseudoAffineWitness SemimanifoldWitness) (AffineModel shy₀ shj) δx
           = convolveShade' (dualShade shy₀)
                            (dualShade . linearProjectShade (lfun ($ δx)) $ shj)
 
@@ -318,7 +314,7 @@
   evalLocalModel = aEvL pseudoAffineWitness
    where aEvL :: ∀ x y . ModellableRelation x y
                 => PseudoAffineWitness y -> QuadraticModel x y -> Needle x -> Shade' y
-         aEvL (PseudoAffineWitness (SemimanifoldWitness _))
+         aEvL (PseudoAffineWitness SemimanifoldWitness)
               (QuadraticModel shy₀ shj shjj) δx
           = (dualShade shy₀)
            `convolveShade'`
diff --git a/Data/Manifold/Function/Quadratic.hs b/Data/Manifold/Function/Quadratic.hs
--- a/Data/Manifold/Function/Quadratic.hs
+++ b/Data/Manifold/Function/Quadratic.hs
@@ -55,66 +55,70 @@
 affineQuadratic (Affine f) = Quadratic . trie
                   $ untrie f >>> second (id &&& const zeroV)
 
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , Manifold y, Scalar (Needle y) ~ s )
-              => Semimanifold (Quadratic s x y) where
+instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold (Needle y), Scalar (Needle y) ~ s
+         , Needle (Needle y) ~ Needle y
+         ) => Semimanifold (Quadratic s x y) where
   type Needle (Quadratic s x y) = Quadratic s x (Needle y)
-  toInterior = pure
-  fromInterior = id
-  (.+~^) = case ( semimanifoldWitness :: SemimanifoldWitness y
-                , boundarylessWitness :: BoundarylessWitness y ) of
-    (SemimanifoldWitness _, BoundarylessWitness) -> \(Quadratic f) (Quadratic g)
+  (.+~^) = case ( semimanifoldWitness :: SemimanifoldWitness y ) of
+    (SemimanifoldWitness) -> \(Quadratic f) (Quadratic g)
       -> Quadratic . trie $ \ix -> case (untrie f ix, untrie g ix) of
           ((fx₀,f'), (gx₀,g')) -> (fx₀.+~^gx₀, f'^+^g')
-  translateP = Tagged (.+~^)
   semimanifoldWitness = case semimanifoldWitness :: SemimanifoldWitness y of
-    SemimanifoldWitness _ -> SemimanifoldWitness BoundarylessWitness
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , Manifold y, Scalar (Needle y) ~ s )
-              => PseudoAffine (Quadratic s x y) where
-  (.-~!) = case ( semimanifoldWitness :: SemimanifoldWitness y
-                , boundarylessWitness :: BoundarylessWitness y ) of
-    (SemimanifoldWitness _, BoundarylessWitness) -> \(Quadratic f) (Quadratic g)
+    SemimanifoldWitness -> SemimanifoldWitness
+instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold (Needle y), Scalar (Needle y) ~ s
+         , Needle (Needle y) ~ Needle y
+         ) => PseudoAffine (Quadratic s x y) where
+  p.-~.q = pure (p.-~!q)
+  (.-~!) = case ( semimanifoldWitness :: SemimanifoldWitness y ) of
+    (SemimanifoldWitness) -> \(Quadratic f) (Quadratic g)
       -> Quadratic . trie $ \ix -> case (untrie f ix, untrie g ix) of
           ((fx₀,f'), (gx₀,g')) -> (fx₀.-~!gx₀, f'^-^g')
   pseudoAffineWitness = case semimanifoldWitness :: SemimanifoldWitness y of
-    SemimanifoldWitness _ -> PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , Manifold y, Scalar (Needle y) ~ s )
-              => AffineSpace (Quadratic s x y) where
+    SemimanifoldWitness -> PseudoAffineWitness (SemimanifoldWitness)
+instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold (Needle y), Scalar (Needle y) ~ s
+         , Needle (Needle y) ~ Needle y
+         ) => AffineSpace (Quadratic s x y) where
   type Diff (Quadratic s x y) = Quadratic s x (Needle y)
   (.+^) = (.+~^); (.-.) = (.-~!)
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , LinearSpace y, Scalar y ~ s, Num' s )
-            => AdditiveGroup (Quadratic s x y) where
+instance ( Atlas x, HasTrie (ChartIndex x)
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold y, Scalar y ~ s
+         , Needle y ~ y
+         ) => AdditiveGroup (Quadratic s x y) where
   zeroV = case linearManifoldWitness :: LinearManifoldWitness y of
-       LinearManifoldWitness _ -> Quadratic . trie $ const (zeroV, zeroV)
+       LinearManifoldWitness -> Quadratic . trie $ const (zeroV, zeroV)
   (^+^) = case ( linearManifoldWitness :: LinearManifoldWitness y
                , dualSpaceWitness :: DualSpaceWitness y ) of
-      (LinearManifoldWitness BoundarylessWitness, DualSpaceWitness) -> (.+~^)
+      (LinearManifoldWitness, DualSpaceWitness) -> (.+~^)
   negateV = case linearManifoldWitness :: LinearManifoldWitness y of
-       LinearManifoldWitness _ -> \(Quadratic f) -> Quadratic . trie $
+       LinearManifoldWitness -> \(Quadratic f) -> Quadratic . trie $
              untrie f >>> negateV***negateV
-instance ( Atlas x, HasTrie (ChartIndex x), LinearSpace (Needle x), Scalar (Needle x) ~ s
-         , LinearSpace y, Scalar y ~ s, Num' s )
-            => VectorSpace (Quadratic s x y) where
+instance ( Atlas x, HasTrie (ChartIndex x)
+         , LinearManifold (Needle x), Scalar (Needle x) ~ s
+         , LinearManifold y, Scalar y ~ s
+         , Needle y ~ y
+         ) => VectorSpace (Quadratic s x y) where
   type Scalar (Quadratic s x y) = s
   (*^) = case linearManifoldWitness :: LinearManifoldWitness y of
-       LinearManifoldWitness _ -> \μ (Quadratic f) -> Quadratic . trie $
+       LinearManifoldWitness -> \μ (Quadratic f) -> Quadratic . trie $
              untrie f >>> (μ*^)***(μ*^)
 
-evalQuadratic :: ∀ s x y . ( Manifold x, Atlas x, HasTrie (ChartIndex x)
+evalQuadratic :: ∀ x y s . ( Manifold x, Atlas x, HasTrie (ChartIndex x)
                            , Manifold y
                            , s ~ Scalar (Needle x), s ~ Scalar (Needle y) )
                => Quadratic s x y -> x
                     -> (y, ( LinearMap s (Needle x) (Needle y)
                            , LinearMap s (SymmetricTensor s (Needle x)) (Needle y) ))
-evalQuadratic = ea (boundarylessWitness, boundarylessWitness)
- where ea :: (BoundarylessWitness x, BoundarylessWitness y)
-             -> Quadratic s x y -> x -> (y, ( LinearMap s (Needle x) (Needle y)
+evalQuadratic = ea
+ where ea :: Quadratic s x y -> x -> (y, ( LinearMap s (Needle x) (Needle y)
                                             , LinearMap s (SymmetricTensor s (Needle x)) (Needle y) ))
-       ea (BoundarylessWitness, BoundarylessWitness)
-          (Quadratic f) x = ( fx₀.+~^(ðx'f₀ $ v).+~^(ð²x'f $ squareV v)
+       ea (Quadratic f) x = ( fx₀.+~^(ðx'f₀ $ v).+~^(ð²x'f $ squareV v)
                             , ( ðx'f₀ ^+^ 2*^((currySymBilin $ ð²x'f) $ v)
                               , ð²x'f
                               ) )
diff --git a/Data/Manifold/Griddable.hs b/Data/Manifold/Griddable.hs
--- a/Data/Manifold/Griddable.hs
+++ b/Data/Manifold/Griddable.hs
@@ -43,6 +43,8 @@
 import Data.Manifold.Types
 import Data.Manifold.Types.Primitive ((^), (^.))
 import Data.Manifold.PseudoAffine
+import Data.Manifold.WithBoundary
+import Data.Manifold.WithBoundary.Class
 import Data.Manifold.TreeCover (Shade(..), fullShade, shadeCtr, shadeExpanse)
     
 import Data.Embedding
@@ -86,7 +88,7 @@
 axisGrLength (GridAxCons _ _ ax) = 1 + axisGrLength ax
 axisGrLength (GridAxisClosed _ ax) = axisGrLength ax
 
-class (WithField ℝ Manifold m) => Griddable m g where
+class (WithField ℝ PseudoAffine m) => Griddable m g where
   data GriddingParameters m g :: *
   mkGridding :: GriddingParameters m g -> Int -> Shade m -> [GridAxis m g]
 
@@ -112,7 +114,10 @@
 
 instance ∀ m n a
     . ( SimpleSpace (Needle m), SimpleSpace (Needle n), SimpleSpace (Needle a)
-      , Griddable m a, Griddable n a, m ~ Interior m, n ~ Interior n )
+      , Griddable m a, Griddable n a
+      , PseudoAffineWithBoundary (m,n)
+      , ProjectableBoundary (m,n)
+      )
              => Griddable (m,n) a where
   data GriddingParameters (m,n) a = PairGriddingParameters {
                fstGriddingParams :: GriddingParameters m a
diff --git a/Data/Manifold/PseudoAffine.hs b/Data/Manifold/PseudoAffine.hs
--- a/Data/Manifold/PseudoAffine.hs
+++ b/Data/Manifold/PseudoAffine.hs
@@ -44,26 +44,30 @@
 {-# LANGUAGE UnicodeSyntax            #-}
 {-# LANGUAGE MultiWayIf               #-}
 {-# LANGUAGE ScopedTypeVariables      #-}
+{-# LANGUAGE TypeApplications         #-}
 {-# LANGUAGE RecordWildCards          #-}
 {-# LANGUAGE CPP                      #-}
 
 
 module Data.Manifold.PseudoAffine (
             -- * Manifold class
-              Manifold(inInterior)
+              Manifold
             , Semimanifold(..), Needle'
             , PseudoAffine(..)
+            , LinearManifold, ScalarManifold
+            , Num'', RealFrac'', RealFloat''
             -- * Type definitions
             -- ** Needles
-            , Local(..), (⊙+^), (!+~^)
+            , Local(..)
+#if !MIN_VERSION_manifolds_core(0,6,0)
+            , (!+~^)
+#endif
             -- ** Metrics
             , Metric, Metric'
             , RieMetric, RieMetric'
             -- ** Constraints
             , SemimanifoldWitness(..)
             , PseudoAffineWitness(..)
-            , BoundarylessWitness(..)
-            , boundarylessWitness
             , DualNeedleWitness 
             , WithField
             , LocallyScalable
@@ -77,6 +81,7 @@
     
 
 import Math.Manifold.Core.PseudoAffine
+import Data.Manifold.WithBoundary.Class
 
 import Data.Maybe
 import Data.Fixed
@@ -114,14 +119,15 @@
   
 
 -- | See 'Semimanifold' and 'PseudoAffine' for the methods.
-class (PseudoAffine m, LSpace (Needle m)) => Manifold m where
-  boundarylessWitness :: BoundarylessWitness m
-  default boundarylessWitness :: (m ~ Interior m) => BoundarylessWitness m
-  boundarylessWitness = BoundarylessWitness
-  inInterior :: m -> Interior m
-  default inInterior :: (m ~ Interior m) => m -> Interior m
-  inInterior = id
-instance (PseudoAffine m, LSpace (Needle m), Interior m ~ m) => Manifold m
+--   As a 'Manifold' we understand a pseudo-affine space whose 'Needle'
+--   space is a well-behaved vector space that is isomorphic to
+--   all of the manifold's tangent spaces.
+--   It must also be an instance of the 'SemimanifoldWithBoundary' class
+--   with explicitly empty boundary (in other words, with /no/ boundary).
+class (OpenManifold m, ProjectableBoundary m, LSpace (Needle m))
+            => Manifold m where
+instance (OpenManifold m, ProjectableBoundary m, LSpace (Needle m))
+            => Manifold m
 
 
 
@@ -157,11 +163,6 @@
   oppositeLocalCoercion :: CanonicalDiffeomorphism ξ x
   default oppositeLocalCoercion :: LocallyCoercible ξ x => CanonicalDiffeomorphism ξ x
   oppositeLocalCoercion = CanonicalDiffeomorphism
-  interiorLocalCoercion :: Functor p (->) (->) 
-                  => p (x,ξ) -> CanonicalDiffeomorphism (Interior x) (Interior ξ)
-  default interiorLocalCoercion :: LocallyCoercible (Interior x) (Interior ξ)
-                  => p (x,ξ) -> CanonicalDiffeomorphism (Interior x) (Interior ξ)
-  interiorLocalCoercion _ = CanonicalDiffeomorphism
 
 type NumPrime n = (Num' n, Eq n)
 
@@ -170,8 +171,7 @@
   locallyTrivialDiffeomorphism = id;              \
   coerceNeedle _ = id;                             \
   coerceNeedle' _ = id;                             \
-  oppositeLocalCoercion = CanonicalDiffeomorphism;   \
-  interiorLocalCoercion _ = CanonicalDiffeomorphism }
+  oppositeLocalCoercion = CanonicalDiffeomorphism }
 identityCoercion(NumPrime s, ZeroDim s)
 identityCoercion(NumPrime s, V0 s)
 identityCoercion((), ℝ)
@@ -337,13 +337,6 @@
   coerceNeedle _ = regroup
   coerceNeedle' _ = regroup
   oppositeLocalCoercion = CanonicalDiffeomorphism
-  interiorLocalCoercion _ = case ( semimanifoldWitness :: SemimanifoldWitness a
-                                 , semimanifoldWitness :: SemimanifoldWitness b
-                                 , semimanifoldWitness :: SemimanifoldWitness c ) of
-       ( SemimanifoldWitness BoundarylessWitness
-        ,SemimanifoldWitness BoundarylessWitness
-        ,SemimanifoldWitness BoundarylessWitness )
-              -> CanonicalDiffeomorphism
 instance ∀ a b c .
          ( Semimanifold a, Semimanifold b, Semimanifold c
          , LSpace (Needle a), LSpace (Needle b), LSpace (Needle c)
@@ -355,56 +348,74 @@
   coerceNeedle _ = regroup'
   coerceNeedle' _ = regroup'
   oppositeLocalCoercion = CanonicalDiffeomorphism
-  interiorLocalCoercion _ = case ( semimanifoldWitness :: SemimanifoldWitness a
-                                 , semimanifoldWitness :: SemimanifoldWitness b
-                                 , semimanifoldWitness :: SemimanifoldWitness c ) of
-       ( SemimanifoldWitness BoundarylessWitness
-        ,SemimanifoldWitness BoundarylessWitness
-        ,SemimanifoldWitness BoundarylessWitness )
-            -> CanonicalDiffeomorphism
 
 
-instance (LinearSpace (a n), Needle (a n) ~ a n, Interior (a n) ~ a n)
+instance (LinearSpace (a n), Needle (a n) ~ a n)
             => Semimanifold (LinAff.Point a n) where
   type Needle (LinAff.Point a n) = a n
-  fromInterior = id
-  toInterior = pure
   LinAff.P v .+~^ w = LinAff.P $ v ^+^ w
-  translateP = Tagged $ \(LinAff.P v) w -> LinAff.P $ v ^+^ w
-instance (LinearSpace (a n), Needle (a n) ~ a n, Interior (a n) ~ a n)
+instance (LinearSpace (a n), Needle (a n) ~ a n)
             => PseudoAffine (LinAff.Point a n) where
   LinAff.P v .-~. LinAff.P w = return $ v ^-^ w
+  LinAff.P v .-~! LinAff.P w = v ^-^ w
 
 
+instance RealFloat' r => Semimanifold (S⁰_ r) where
+  type Needle (S⁰_ r) = ZeroDim r
+  p .+~^ Origin = p
+  p .-~^ Origin = p
+instance RealFloat' r => PseudoAffine (S⁰_ r) where
+  PositiveHalfSphere .-~. PositiveHalfSphere = pure Origin
+  NegativeHalfSphere .-~. NegativeHalfSphere = pure Origin
+  _ .-~. _ = Nothing
+  PositiveHalfSphere .-~! PositiveHalfSphere = Origin
+  NegativeHalfSphere .-~! NegativeHalfSphere = Origin
+  _ .-~! _ = error "There is no path between the two 0-dimensional half spheres."
 
+instance RealFloat' r => Semimanifold (S¹_ r) where
+  type Needle (S¹_ r) = r
+  S¹Polar φ₀ .+~^ δφ  = S¹Polar $ φ'
+   where φ' = toS¹range $ φ₀ + δφ
+  semimanifoldWitness = case linearManifoldWitness @r of
+    LinearManifoldWitness -> SemimanifoldWitness
+instance RealFloat' r => PseudoAffine (S¹_ r) where
+  p .-~. q = pure (p.-~!q)
+  S¹Polar φ₁ .-~! S¹Polar φ₀
+     | δφ > pi     = δφ - tau
+     | δφ < (-pi)  = δφ + tau
+     | otherwise   = δφ
+   where δφ = φ₁ - φ₀
 
-instance Semimanifold S² where
-  type Needle S² = ℝ²
-  fromInterior = id
-  toInterior = pure
-  translateP = Tagged (.+~^)
-  S²Polar θ₀ φ₀ .+~^ 𝐯 = S²Polar θ₁ φ₁
-   where -- See images/constructions/sphericoords-needles.svg.
-         S¹Polar γc = coEmbed 𝐯
-         γ | θ₀ < pi/2   = γc - φ₀
-           | otherwise   = γc + φ₀
-         d = magnitude 𝐯
-         S¹Polar φ₁ = S¹Polar φ₀ .+~^ δφ
-         
-         -- Cartesian coordinates of p₁ in the system whose north pole is p₀
-         -- with φ₀ as the zero meridian
-         V3 bx by bz = embed $ S²Polar d γ
-         
-         sθ₀ = sin θ₀; cθ₀ = cos θ₀
-         -- Cartesian coordinates of p₁ in the system with the standard north pole,
-         -- but still φ₀ as the zero meridian
-         (qx,qz) = ( cθ₀ * bx + sθ₀ * bz
-                   ,-sθ₀ * bx + cθ₀ * bz )
-         qy      = by
-         
-         S²Polar θ₁ δφ = coEmbed $ V3 qx qy qz
 
-instance PseudoAffine S² where
+
+instance RealFloat' s => Semimanifold (S²_ s) where
+  type Needle (S²_ s) = V2 s
+  (.+~^) = case linearManifoldWitness @s of
+   LinearManifoldWitness ->
+      let addS² (S²Polar θ₀ φ₀) 𝐯 = S²Polar θ₁ φ₁
+           where -- See images/constructions/sphericoords-needles.svg.
+                 S¹Polar γc = coEmbed 𝐯
+                 γ | θ₀ < pi/2   = γc - φ₀
+                   | otherwise   = γc + φ₀
+                 d = magnitude 𝐯
+                 S¹Polar φ₁ = S¹Polar φ₀ .+~^ δφ
+                 
+                 -- Cartesian coordinates of p₁ in the system whose north pole is p₀
+                 -- with φ₀ as the zero meridian
+                 V3 bx by bz = embed $ S²Polar d γ
+                 
+                 sθ₀ = sin θ₀; cθ₀ = cos θ₀
+                 -- Cartesian coordinates of p₁ in the system with the standard north pole,
+                 -- but still φ₀ as the zero meridian
+                 (qx,qz) = ( cθ₀ * bx + sθ₀ * bz
+                           ,-sθ₀ * bx + cθ₀ * bz )
+                 qy      = by
+                 
+                 S²Polar θ₁ δφ = coEmbed $ V3 qx qy qz
+      in addS²
+
+instance RealFloat' s => PseudoAffine (S²_ s) where
+  p.-~.q = pure (p.-~!q)
   S²Polar θ₁ φ₁ .-~! S²Polar θ₀ φ₀ = d *^ embed(S¹Polar γc)
    where -- See images/constructions/sphericoords-needles.svg.
          V3 qx qy qz = embed $ S²Polar θ₁ (φ₁-φ₀)
@@ -424,15 +435,13 @@
 
 instance Semimanifold ℝP² where
   type Needle ℝP² = ℝ²
-  fromInterior = id
-  toInterior = pure
-  translateP = Tagged (.+~^)
   HemisphereℝP²Polar θ₀ φ₀ .+~^ v
       = case S²Polar θ₀ φ₀ .+~^ v of
           S²Polar θ₁ φ₁
            | θ₁ > pi/2   -> HemisphereℝP²Polar (pi-θ₁) (-φ₁)
            | otherwise   -> HemisphereℝP²Polar θ₁        φ₁
 instance PseudoAffine ℝP² where
+  p.-~.q = pure (p.-~!q)
   HemisphereℝP²Polar θ₁ φ₁ .-~! HemisphereℝP²Polar θ₀ φ₀
       = case S²Polar θ₁ φ₁ .-~! S²Polar θ₀ φ₀ of
           v -> let r² = magnitudeSq v
@@ -476,21 +485,17 @@
 
 
 
+#if !MIN_VERSION_manifolds_core(0,6,0)
 infixl 6 !+~^
 -- | Boundary-unsafe version of `.+~^`.
 (!+~^) :: ∀ x . (Semimanifold x, HasCallStack) => x -> Needle x -> x
 p!+~^v = case toInterior p of
            Just p' -> p'.+~^v
+#endif
 
 
-infix 6 ⊙+^
--- | Proxy-version of `translateP`.
-(⊙+^) :: ∀ x proxy . Semimanifold x => Interior x -> Needle x -> proxy x -> Interior x
-(⊙+^) x v _ = tp x v
- where Tagged tp = translateP :: Tagged x (Interior x -> Needle x -> Interior x)
 
 
-
 infix 6 .−.
 -- | A connected manifold is one where any point can be reached by translation from
 --   any other point.
@@ -515,3 +520,11 @@
 instance (Connected x, Connected y, PseudoAffine (FibreBundle x y))
                => Connected (FibreBundle x y)
 
+
+
+type LinearManifold m = (LinearSpace m, Manifold m)
+
+type ScalarManifold s = (Num' s, Manifold s, Manifold (ZeroDim s))
+type Num'' s = ScalarManifold s
+type RealFrac'' s = (RealFrac' s, ScalarManifold s)
+type RealFloat'' s = (RealFloat' s, SimpleSpace s, ScalarManifold s)
diff --git a/Data/Manifold/Riemannian.hs b/Data/Manifold/Riemannian.hs
--- a/Data/Manifold/Riemannian.hs
+++ b/Data/Manifold/Riemannian.hs
@@ -41,6 +41,7 @@
 {-# LANGUAGE LiberalTypeSynonyms        #-}
 {-# LANGUAGE CPP                        #-}
 {-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE DefaultSignatures          #-}
 
 
@@ -59,8 +60,10 @@
 import Linear (V0(..), V1(..), V2(..), V3(..), V4(..))
 
 import Data.Manifold.Types
-import Data.Manifold.Types.Primitive ((^), empty, embed, coEmbed)
+import Data.Manifold.Types.Primitive ( (^), empty, embed, coEmbed )
 import Data.Manifold.Types.Stiefel
+import Data.Manifold.WithBoundary
+import Data.Manifold.WithBoundary.Class
 import Data.Manifold.PseudoAffine
 import Data.Manifold.Atlas (AffineManifold)
     
@@ -78,11 +81,7 @@
 import Data.Foldable.Constrained
 
 
-data GeodesicWitness x where
-  GeodesicWitness :: Geodesic (Interior x)
-       => SemimanifoldWitness x -> GeodesicWitness x
-
-class Semimanifold x => Geodesic x where
+class SemimanifoldWithBoundary x => Geodesic x where
   geodesicBetween ::
           x -- ^ Starting point; the interpolation will yield this at -1.
        -> x -- ^ End point, for +1.
@@ -90,9 +89,6 @@
             --   If the two points are actually connected by a path...
        -> Maybe (D¹ -> x) -- ^ ...then this is the interpolation function. Attention: 
                           --   the type will change to 'Differentiable' in the future.
-  geodesicWitness :: GeodesicWitness x
-  default geodesicWitness :: Geodesic (Interior x) => GeodesicWitness x
-  geodesicWitness = GeodesicWitness semimanifoldWitness
   middleBetween :: x -> x -> Maybe x
   middleBetween p₀ p₁ = ($ D¹ 0) <$> geodesicBetween p₀ p₁
 
@@ -111,49 +107,45 @@
 
 deriveAffineGD (ℝ)
 
-instance Geodesic (ZeroDim s) where
+instance (Num' s, OpenManifold s) => Geodesic (ZeroDim s) where
   geodesicBetween Origin Origin = return $ \_ -> Origin
   middleBetween Origin Origin = return Origin
 
-instance ∀ a b . (Geodesic a, Geodesic b) => Geodesic (a,b) where
+instance ∀ a b . ( Geodesic a, Geodesic b
+                 , Scalar (Needle (Interior a)) ~ Scalar (Needle (Interior b))
+                 , SemimanifoldWithBoundary (a,b)
+                 )
+      => Geodesic (a,b) where
   geodesicBetween (a,b) (α,β) = liftA2 (&&&) (geodesicBetween a α) (geodesicBetween b β)
-  geodesicWitness = case ( geodesicWitness :: GeodesicWitness a
-                         , geodesicWitness :: GeodesicWitness b ) of
-     (GeodesicWitness _, GeodesicWitness _) -> GeodesicWitness semimanifoldWitness
   middleBetween (a,b) (α,β) = fzip (middleBetween a α, middleBetween b β)
 
-instance ∀ a b c . (Geodesic a, Geodesic b, Geodesic c) => Geodesic (a,b,c) where
-  geodesicBetween (a,b,c) (α,β,γ)
-      = liftA3 (\ia ib ic t -> (ia t, ib t, ic t))
-           (geodesicBetween a α) (geodesicBetween b β) (geodesicBetween c γ)
-  geodesicWitness = case ( geodesicWitness :: GeodesicWitness a
-                         , geodesicWitness :: GeodesicWitness b
-                         , geodesicWitness :: GeodesicWitness c ) of
-     (GeodesicWitness _, GeodesicWitness _, GeodesicWitness _)
-         -> GeodesicWitness semimanifoldWitness
+-- instance ∀ a b c . (Geodesic a, Geodesic b, Geodesic c) => Geodesic (a,b,c) where
+--   geodesicBetween (a,b,c) (α,β,γ)
+--       = liftA3 (\ia ib ic t -> (ia t, ib t, ic t))
+--            (geodesicBetween a α) (geodesicBetween b β) (geodesicBetween c γ)
 
 -- instance (KnownNat n) => Geodesic (FreeVect n ℝ) where
 --   geodesicBetween (FreeVect v) (FreeVect w)
 --       = return $ \(D¹ t) -> let μv = (1-t)/2; μw = (t+1)/2
 --                             in FreeVect $ Arr.zipWith (\vi wi -> μv*vi + μw*wi) v w
 
-instance ∀ v . ( Geodesic v, FiniteFreeSpace v, FiniteFreeSpace (DualVector v)
-               , LinearSpace v, Scalar v ~ ℝ, Geodesic (DualVector v)
-               , InnerSpace (DualVector v) )
-             => Geodesic (Stiefel1 v) where
-  geodesicBetween = gb dualSpaceWitness
-   where gb :: DualSpaceWitness v -> Stiefel1 v -> Stiefel1 v -> Maybe (D¹ -> Stiefel1 v)
-         gb DualSpaceWitness (Stiefel1 p') (Stiefel1 q')
-           = (\f -> \(D¹ t) -> Stiefel1 . f . D¹ $ g * tan (ϑ*t))
-            <$> geodesicBetween p q
-          where p = normalized p'; q = normalized q'
-                l = magnitude $ p^-^q
-                ϑ = asin $ l/2
-                g = sqrt $ 4/l^2 - 1
-  middleBetween = gb dualSpaceWitness
-   where gb :: DualSpaceWitness v -> Stiefel1 v -> Stiefel1 v -> Maybe (Stiefel1 v)
-         gb DualSpaceWitness  (Stiefel1 p) (Stiefel1 q)
-             = Stiefel1 <$> middleBetween (normalized p) (normalized q)
+-- instance ∀ v . ( Geodesic v, FiniteFreeSpace v, FiniteFreeSpace (DualVector v)
+--                , LinearSpace v, Scalar v ~ ℝ, Geodesic (DualVector v)
+--                , InnerSpace (DualVector v) )
+--              => Geodesic (Stiefel1 v) where
+--   geodesicBetween = gb dualSpaceWitness
+--    where gb :: DualSpaceWitness v -> Stiefel1 v -> Stiefel1 v -> Maybe (D¹ -> Stiefel1 v)
+--          gb DualSpaceWitness (Stiefel1 p') (Stiefel1 q')
+--            = (\f -> \(D¹ t) -> Stiefel1 . f . D¹ $ g * tan (ϑ*t))
+--             <$> geodesicBetween p q
+--           where p = normalized p'; q = normalized q'
+--                 l = magnitude $ p^-^q
+--                 ϑ = asin $ l/2
+--                 g = sqrt $ 4/l^2 - 1
+--   middleBetween = gb dualSpaceWitness
+--    where gb :: DualSpaceWitness v -> Stiefel1 v -> Stiefel1 v -> Maybe (Stiefel1 v)
+--          gb DualSpaceWitness  (Stiefel1 p) (Stiefel1 q)
+--              = Stiefel1 <$> middleBetween (normalized p) (normalized q)
 
 
 instance Geodesic S⁰ where
@@ -232,19 +224,19 @@
 deriveAffineGD (ℝ³)
 deriveAffineGD (ℝ⁴)
 
-instance (TensorSpace v, Scalar v ~ ℝ, TensorSpace w, Scalar w ~ ℝ)
+instance (LinearSpace v, Scalar v ~ ℝ, LinearSpace w, Scalar w ~ ℝ)
              => Geodesic (Tensor ℝ v w) where
   geodesicBetween a b = return $ alerp a b . (/2) . (+1) . xParamD¹
-instance (LinearSpace v, Scalar v ~ ℝ, TensorSpace w, Scalar w ~ ℝ)
+instance (LinearSpace v, Scalar v ~ ℝ, LinearSpace w, Scalar w ~ ℝ)
              => Geodesic (LinearMap ℝ v w) where
   geodesicBetween a b = return $ alerp a b . (/2) . (+1) . xParamD¹
-instance (TensorSpace v, Scalar v ~ ℝ, TensorSpace w, Scalar w ~ ℝ)
+instance (LinearSpace v, Scalar v ~ ℝ, LinearSpace w, Scalar w ~ ℝ)
              => Geodesic (LinearFunction ℝ v w) where
   geodesicBetween a b = return $ alerp a b . (/2) . (+1) . xParamD¹
 
 
 -- | One-dimensional manifolds, whose closure is homeomorpic to the unit interval.
-class WithField ℝ PseudoAffine i => IntervalLike i where
+class WithField ℝ PseudoAffine (Interior i) => IntervalLike i where
   toClosedInterval :: i -> D¹ -- Differentiable ℝ i D¹
 
 instance IntervalLike D¹ where
diff --git a/Data/Manifold/Shade.hs b/Data/Manifold/Shade.hs
--- a/Data/Manifold/Shade.hs
+++ b/Data/Manifold/Shade.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE StandaloneDeriving         #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies               #-}
 {-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE GADTs                      #-}
@@ -22,6 +23,7 @@
 {-# LANGUAGE ViewPatterns               #-}
 {-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE CPP                        #-}
 {-# LANGUAGE TupleSections              #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
@@ -48,7 +50,7 @@
        , shadesMerge, pointsShades', pseudoECM, convolveMetric
        , WithAny(..), shadeWithAny, shadeWithoutAnything
        -- * Misc
-       , rangeOnGeodesic, rangeWithinVertices
+       , rangeWithinVertices
     ) where
 
 
@@ -70,6 +72,7 @@
 import Data.Manifold.Types.Primitive ((^))
 import Data.Manifold.PseudoAffine
 import Data.Manifold.Riemannian
+import Data.Manifold.WithBoundary
 import Data.Manifold.Atlas
 import Data.Function.Affine
 import Data.Manifold.Function.Quadratic
@@ -104,22 +107,22 @@
 --   there is 'Region', whose implementation is vastly more complex.
 data Shade x where
    Shade :: (Semimanifold x, SimpleSpace (Needle x))
-           =>  { _shadeCtr :: !(Interior x)
+           =>  { _shadeCtr :: !x
                , _shadeExpanse :: !(Metric' x) } -> Shade x
-deriving instance (Show (Interior x), Show (Metric' x), WithField ℝ PseudoAffine x)
+deriving instance (Show x, Show (Metric' x), WithField ℝ PseudoAffine x)
                 => Show (Shade x)
 
 -- | A &#x201c;co-shade&#x201d; can describe ellipsoid regions as well, but unlike
 --   'Shade' it can be unlimited / infinitely wide in some directions.
 --   It does OTOH need to have nonzero thickness, which 'Shade' needs not.
-data Shade' x = Shade' { _shade'Ctr :: !(Interior x)
+data Shade' x = Shade' { _shade'Ctr :: !x
                        , _shade'Narrowness :: !(Metric x) }
 
 
 class IsShade shade where
 --  type (*) shade :: *->*
   -- | Access the center of a 'Shade' or a 'Shade''.
-  shadeCtr :: Lens' (shade x) (Interior x)
+  shadeCtr :: Lens' (shade x) x
 --  -- | Convert between 'Shade' and 'Shade' (which must be neither singular nor infinite).
 --  unsafeDualShade :: WithField ℝ Manifold x => shade x -> shade* x
   -- | Check the statistical likelihood-density of a point being within a shade.
@@ -143,30 +146,30 @@
                           => (x+>y) -> shade x -> shade y
   -- | Squash a shade down into a lower dimensional space.
   projectShade :: ( Semimanifold x, Semimanifold y
-                  , Object (Affine s) (Interior x), Object (Affine s) (Interior y)
+                  , Object (Affine s) x, Object (Affine s) y
                   , SimpleSpace (Needle x), SemiInner (Needle y) )
-                        => Embedding (Affine s) (Interior x) (Interior y)
+                        => Embedding (Affine s) x y
                               -> shade y -> shade x
   -- | Include a shade in a higher-dimensional space. Notice that this behaves
   --   fundamentally different for 'Shade' and 'Shade''. For 'Shade', it gives
   --   a “flat image” of the region, whereas for 'Shade'' it gives an “extrusion
   --   pillar” pointing in the projection's orthogonal complement.
   embedShade :: ( Semimanifold x, Semimanifold y
-                , Object (Affine s) (Interior x), Object (Affine s) (Interior y)
+                , Object (Affine s) x, Object (Affine s) y
                 , SemiInner (Needle x), SimpleSpace (Needle y) )
-                        => Embedding (Affine s) (Interior x) (Interior y)
+                        => Embedding (Affine s) x y
                               -> shade x -> shade y
   
 
-linearProjectShade :: ∀ s x y
+linearProjectShade :: ∀ x y s
           . (Num' s, LinearSpace x, SimpleSpace y, Scalar x ~ s, Scalar y ~ s)
                   => (x+>y) -> Shade x -> Shade y
 linearProjectShade = case ( linearManifoldWitness :: LinearManifoldWitness x
                           , linearManifoldWitness :: LinearManifoldWitness y
                           , dualSpaceWitness :: DualSpaceWitness x
                           , dualSpaceWitness :: DualSpaceWitness y ) of
-   ( LinearManifoldWitness BoundarylessWitness
-    ,LinearManifoldWitness BoundarylessWitness
+   ( LinearManifoldWitness
+    ,LinearManifoldWitness
     ,DualSpaceWitness, DualSpaceWitness )
        -> \f (Shade x ex) -> Shade (f $ x) (transformVariance f ex)
 
@@ -186,8 +189,8 @@
    where occ :: ∀ x s . ( PseudoAffine x, SimpleSpace (Needle x)
                         , Scalar (Needle x) ~ s, RealFloat' s )
                     => PseudoAffineWitness x -> DualNeedleWitness x -> Shade x -> x -> s
-         occ (PseudoAffineWitness (SemimanifoldWitness _)) DualSpaceWitness (Shade p₀ δ)
-                 = \p -> case toInterior p >>= (.-~.p₀) of
+         occ (PseudoAffineWitness SemimanifoldWitness) DualSpaceWitness (Shade p₀ δ)
+                 = \p -> case p.-~.p₀ of
            (Just vd) | mSq <- normSq δinv vd
                      , mSq == mSq  -- avoid NaN
                      -> exp (negate mSq)
@@ -214,12 +217,11 @@
    where cS :: ∀ x y . (LocallyCoercible x y, SimpleSpace (Needle y))
                 => DualNeedleWitness x -> DualNeedleWitness y -> Shade x -> Shade y
          cS DualSpaceWitness DualSpaceWitness
-                    = \(Shade x δxym) -> Shade (internCoerce x) (tN δxym)
+                    = \(Shade x δxym)
+                         -> Shade (locallyTrivialDiffeomorphism x) (tN δxym)
           where tN = case oppositeLocalCoercion :: CanonicalDiffeomorphism y x of
                       CanonicalDiffeomorphism ->
                        transformNorm . arr $ coerceNeedle' ([]::[(y,x)])
-                internCoerce = case interiorLocalCoercion ([]::[(x,y)]) of
-                      CanonicalDiffeomorphism -> locallyTrivialDiffeomorphism
   linIsoTransformShade = lits linearManifoldWitness linearManifoldWitness
                               dualSpaceWitness dualSpaceWitness
    where lits :: ∀ x y . ( LinearSpace x, SimpleSpace y
@@ -227,30 +229,30 @@
                => LinearManifoldWitness x -> LinearManifoldWitness y
                    -> DualSpaceWitness x -> DualSpaceWitness y
                        -> (x+>y) -> Shade x -> Shade y
-         lits (LinearManifoldWitness BoundarylessWitness)
-              (LinearManifoldWitness BoundarylessWitness)
+         lits (LinearManifoldWitness)
+              (LinearManifoldWitness)
               DualSpaceWitness DualSpaceWitness
               f (Shade x δx)
                   = Shade (f $ x) (transformNorm (adjoint $ f) δx)
   embedShade = ps' (semimanifoldWitness, semimanifoldWitness)
    where ps' :: ∀ s x y . ( Semimanifold y
-                          , Object (Affine s) (Interior x), Object (Affine s) (Interior y)
+                          , Object (Affine s) x, Object (Affine s) y
                           , SemiInner (Needle x), SimpleSpace (Needle y) )
                         => (SemimanifoldWitness x, SemimanifoldWitness y)
-               -> Embedding (Affine s) (Interior x) (Interior y)
+               -> Embedding (Affine s) x y
                               -> Shade x -> Shade y
-         ps' (SemimanifoldWitness _, SemimanifoldWitness _)
+         ps' (SemimanifoldWitness, SemimanifoldWitness)
               (Embedding q _) (Shade x e) = Shade y (transformVariance j e)
           where y = q $ x
                 (_,j) = evalAffine q x
   projectShade = ps' (semimanifoldWitness, semimanifoldWitness)
    where ps' :: ∀ s x y . ( Semimanifold x
-                          , Object (Affine s) (Interior x), Object (Affine s) (Interior y)
+                          , Object (Affine s) x, Object (Affine s) y
                           , SimpleSpace (Needle x), SemiInner (Needle y) )
                         => (SemimanifoldWitness x, SemimanifoldWitness y)
-               -> Embedding (Affine s) (Interior x) (Interior y)
+               -> Embedding (Affine s) x y
                               -> Shade y -> Shade x
-         ps' (SemimanifoldWitness _, SemimanifoldWitness _)
+         ps' (SemimanifoldWitness, SemimanifoldWitness)
               (Embedding _ q) (Shade x e) = Shade y (transformVariance j e)
           where y = q $ x
                 (_,j) = evalAffine q x
@@ -288,8 +290,8 @@
    where occ :: ∀ x s . ( PseudoAffine x, SimpleSpace (Needle x)
                         , Scalar (Needle x) ~ s, RealFloat' s )
                     => PseudoAffineWitness x -> Shade' x -> x -> s
-         occ (PseudoAffineWitness (SemimanifoldWitness _)) (Shade' p₀ δinv) p
-               = case toInterior p >>= (.-~.p₀) of
+         occ (PseudoAffineWitness (SemimanifoldWitness)) (Shade' p₀ δinv) p
+               = case p.-~.p₀ of
            (Just vd) | mSq <- normSq δinv vd
                      , mSq == mSq  -- avoid NaN
                      -> exp (negate mSq)
@@ -299,12 +301,10 @@
   orthoShades (Shade' x δx) (Shade' y δy) = Shade' (x,y) $ sumSubspaceNorms δx δy
   coerceShade = cS
    where cS :: ∀ x y . (LocallyCoercible x y) => Shade' x -> Shade' y
-         cS = \(Shade' x δxym) -> Shade' (internCoerce x) (tN δxym)
+         cS = \(Shade' x δxym) -> Shade' (locallyTrivialDiffeomorphism x) (tN δxym)
           where tN = case oppositeLocalCoercion :: CanonicalDiffeomorphism y x of
                       CanonicalDiffeomorphism ->
                        transformNorm . arr $ coerceNeedle ([]::[(y,x)])
-                internCoerce = case interiorLocalCoercion ([]::[(x,y)]) of
-                      CanonicalDiffeomorphism -> locallyTrivialDiffeomorphism
   linIsoTransformShade = lits linearManifoldWitness linearManifoldWitness
                               dualSpaceWitness dualSpaceWitness
    where lits :: ∀ x y . ( SimpleSpace x, SimpleSpace y
@@ -312,28 +312,28 @@
                => LinearManifoldWitness x -> LinearManifoldWitness y
                    -> DualSpaceWitness x -> DualSpaceWitness y
                        -> (x+>y) -> Shade' x -> Shade' y
-         lits (LinearManifoldWitness BoundarylessWitness)
-              (LinearManifoldWitness BoundarylessWitness)
+         lits (LinearManifoldWitness)
+              (LinearManifoldWitness)
               DualSpaceWitness DualSpaceWitness
                f (Shade' x δx)
           = Shade' (f $ x) (transformNorm (pseudoInverse f) δx)
   embedShade = ps (semimanifoldWitness, semimanifoldWitness)
-   where ps :: ∀ s x y . ( Object (Affine s) (Interior x), Object (Affine s) (Interior y)
+   where ps :: ∀ s x y . ( Object (Affine s) x, Object (Affine s) y
                          , SemiInner (Needle x), SemiInner (Needle y) )
                         => (SemimanifoldWitness x, SemimanifoldWitness y)
-               -> Embedding (Affine s) (Interior x) (Interior y)
+               -> Embedding (Affine s) x y
                               -> Shade' x -> Shade' y
-         ps (SemimanifoldWitness _, SemimanifoldWitness _)
+         ps (SemimanifoldWitness, SemimanifoldWitness)
              (Embedding q p) (Shade' x e) = Shade' y (transformNorm j e)
           where y = q $ x
                 (_,j) = evalAffine p y
   projectShade = ps (semimanifoldWitness, semimanifoldWitness)
-   where ps :: ∀ s x y . ( Object (Affine s) (Interior x), Object (Affine s) (Interior y)
+   where ps :: ∀ s x y . ( Object (Affine s) x, Object (Affine s) y
                          , SemiInner (Needle x), SemiInner (Needle y) )
                         => (SemimanifoldWitness x, SemimanifoldWitness y)
-               -> Embedding (Affine s) (Interior x) (Interior y)
+               -> Embedding (Affine s) x y
                               -> Shade' y -> Shade' x
-         ps (SemimanifoldWitness _, SemimanifoldWitness _)
+         ps (SemimanifoldWitness, SemimanifoldWitness)
              (Embedding p q) (Shade' x e) = Shade' y (transformNorm j e)
           where y = q $ x
                 (_,j) = evalAffine p y
@@ -342,23 +342,67 @@
 shadeNarrowness :: Lens' (Shade' x) (Metric x)
 shadeNarrowness f (Shade' c e) = fmap (Shade' c) $ f e
 
-instance ∀ x . (PseudoAffine x) => Semimanifold (Shade x) where
-  type Needle (Shade x) = Needle x
-  fromInterior = id
-  toInterior = pure
-  translateP = Tagged (.+~^)
+newtype ShadeNeedle x = ShadeNeedle { shadeCtrDiff :: Needle x
+                                       -- TODO add shade-spread information
+                                   }
+deriving instance (AdditiveGroup (Needle x)) => AdditiveGroup (ShadeNeedle x)
+deriving instance (VectorSpace (Needle x)) => VectorSpace (ShadeNeedle x)
+
+instance (VectorSpace (Needle x)) => Semimanifold (ShadeNeedle x) where
+  type Needle (ShadeNeedle x) = ShadeNeedle x
+  (.+~^) = (^+^)
+
+instance ∀ x . (PseudoAffine x, VectorSpace (Needle x)) => Semimanifold (Shade x) where
+  type Needle (Shade x) = ShadeNeedle x
   (.+~^) = case semimanifoldWitness :: SemimanifoldWitness x of
-             SemimanifoldWitness BoundarylessWitness
-                   -> \(Shade c e) v -> Shade (c.+~^v) e
+             SemimanifoldWitness
+                   -> \(Shade c e) (ShadeNeedle v) -> Shade (c.+~^v) e
   (.-~^) = case semimanifoldWitness :: SemimanifoldWitness x of
-             SemimanifoldWitness BoundarylessWitness
-                   -> \(Shade c e) v -> Shade (c.-~^v) e
+             SemimanifoldWitness
+                   -> \(Shade c e) (ShadeNeedle v) -> Shade (c.-~^v) e
   semimanifoldWitness = case semimanifoldWitness :: SemimanifoldWitness x of
-                         (SemimanifoldWitness BoundarylessWitness)
-                          -> SemimanifoldWitness BoundarylessWitness
+                         (SemimanifoldWitness)
+                          -> SemimanifoldWitness
 
-instance (WithField ℝ PseudoAffine x, Geodesic (Interior x), SimpleSpace (Needle x))
-             => Geodesic (Shade x) where
+data ShadeHalfNeedle x = ShadeHalfNeedle -- TODO add shade-spread information
+
+instance AdditiveMonoid (ShadeHalfNeedle x) where
+  zeroHV = undefined
+  addHVs = undefined
+
+instance ( VectorSpace (Needle x)
+         ) => HalfSpace (ShadeHalfNeedle x) where
+  type FullSubspace (ShadeHalfNeedle x) = Needle x
+  type Ray (ShadeHalfNeedle x) = Ray x
+  type MirrorJoin (ShadeHalfNeedle x) = Needle x
+  scaleNonNeg = undefined
+  fromFullSubspace = undefined
+  projectToFullSubspace = undefined
+  fullSubspaceIsVectorSpace _ = undefined
+  rayIsHalfSpace _ = undefined
+  mirrorJoinIsVectorSpace _ = undefined
+  fromPositiveHalf = undefined
+  fromNegativeHalf = undefined
+
+instance ( AffineSpace x, Manifold x, Diff x ~ Needle x
+         , Atlas x, HasTrie (ChartIndex x)   -- ??
+         , LinearSpace (Needle x), LinearSpace (Needle' x)
+         , Num' (Scalar (Needle x))
+         ) => SemimanifoldWithBoundary (Shade x) where
+  type Interior (Shade x) = Shade' x
+  type Boundary (Shade x) = x
+  type HalfNeedle (Shade x) = ShadeHalfNeedle x
+  extendToBoundary = undefined
+  smfdWBoundWitness = undefined
+  needleIsOpenMfd _ = undefined
+  scalarIsOpenMfd _ = undefined
+
+instance ( AffineSpace x, Manifold x, Diff x ~ Needle x
+         , Atlas x, HasTrie (ChartIndex x)   -- ??
+         , Geodesic x
+         , LinearSpace (Needle x), LinearSpace (Needle' x)
+         , Scalar (Needle x) ~ ℝ
+         ) => Geodesic (Shade x) where
   geodesicBetween = gb dualSpaceWitness
    where gb :: DualNeedleWitness x -> Shade x -> Shade x -> Maybe (D¹ -> Shade x)
          gb DualSpaceWitness (Shade c (Norm e)) (Shade ζ (Norm η)) = pure interp
@@ -368,18 +412,56 @@
                 ηd@(LinearMap _) = arr η
                 Just pinterp = geodesicBetween c ζ
 
+newtype Shade'Needle x = Shade'Needle { shade'CtrDiff :: Needle x
+                                       -- TODO add shade-spread information
+                                   }
+deriving instance (AdditiveGroup (Needle x)) => AdditiveGroup (Shade'Needle x)
+deriving instance (VectorSpace (Needle x)) => VectorSpace (Shade'Needle x)
+
+instance (VectorSpace (Needle x)) => Semimanifold (Shade'Needle x) where
+  type Needle (Shade'Needle x) = Shade'Needle x
+  (.+~^) = (^+^)
+
+
 instance (AffineManifold x) => Semimanifold (Shade' x) where
-  type Needle (Shade' x) = Needle x
-  fromInterior = id
-  toInterior = pure
-  translateP = Tagged (.+~^)
-  (.+~^) = case boundarylessWitness :: BoundarylessWitness x of
-      BoundarylessWitness -> \(Shade' c e) v -> Shade' (c.+~^v) e
-  (.-~^) = case boundarylessWitness :: BoundarylessWitness x of
-      BoundarylessWitness -> \(Shade' c e) v -> Shade' (c.-~^v) e
+  type Needle (Shade' x) = Shade'Needle x
+  Shade' c e .+~^ Shade'Needle v = Shade' (c.+~^v) e
+  Shade' c e .-~^ Shade'Needle v = Shade' (c.-~^v) e
   semimanifoldWitness = case semimanifoldWitness :: SemimanifoldWitness x of
-     SemimanifoldWitness BoundarylessWitness -> SemimanifoldWitness BoundarylessWitness
+     SemimanifoldWitness -> SemimanifoldWitness
 
+data Shade'HalfNeedle x = Shade'HalfNeedle -- TODO add shade-spread information
+
+instance AdditiveMonoid (Shade'HalfNeedle x) where
+  zeroHV = undefined
+  addHVs = undefined
+
+instance ( VectorSpace (Needle x)
+         ) => HalfSpace (Shade'HalfNeedle x) where
+  type FullSubspace (Shade'HalfNeedle x) = Needle x
+  type Ray (Shade'HalfNeedle x) = Ray x
+  type MirrorJoin (Shade'HalfNeedle x) = Needle x
+  scaleNonNeg = undefined
+  fromFullSubspace = undefined
+  projectToFullSubspace = undefined
+  fullSubspaceIsVectorSpace _ = undefined
+  rayIsHalfSpace _ = undefined
+  mirrorJoinIsVectorSpace _ = undefined
+  fromPositiveHalf = undefined
+  fromNegativeHalf = undefined
+
+instance ( AffineSpace x, Manifold x, Diff x ~ Needle x
+         , Atlas' x
+         , LinearSpace (Needle x), LinearSpace (Needle' x)
+         ) => SemimanifoldWithBoundary (Shade' x) where
+  type Interior (Shade' x) = Shade x
+  type Boundary (Shade' x) = x
+  type HalfNeedle (Shade' x) = Shade'HalfNeedle x
+  extendToBoundary = undefined
+  smfdWBoundWitness = undefined
+  needleIsOpenMfd _ = undefined
+  scalarIsOpenMfd _ = undefined
+
 instance ∀ x . (WithField ℝ AffineManifold x, Geodesic x, SimpleSpace (Needle x))
             => Geodesic (Shade' x) where
   geodesicBetween (Shade' c e) (Shade' ζ η) = pure interp
@@ -387,14 +469,13 @@
          interp t = Shade' (pinterp t)
                            (spanNorm [ v ^/ (alerpB 1 (recip qη) t)
                                      | (v,qη) <- sharedSpan ])
-         Just pinterp = case geodesicWitness :: GeodesicWitness x of
-            GeodesicWitness _ -> geodesicBetween c ζ
+         Just pinterp = geodesicBetween c ζ
 
 fullShade :: (Semimanifold x, SimpleSpace (Needle x))
-                      => Interior x -> Metric' x -> Shade x
+                      => x -> Metric' x -> Shade x
 fullShade ctr expa = Shade ctr expa
 
-fullShade' :: WithField ℝ SimpleSpace x => Interior x -> Metric x -> Shade' x
+fullShade' :: WithField ℝ SimpleSpace x => x -> Metric x -> Shade' x
 fullShade' ctr expa = Shade' ctr expa
 
 
@@ -407,7 +488,7 @@
 pattern (:±) :: (Semimanifold x, SimpleSpace (Needle x))
 #endif
              => (Semimanifold x, SimpleSpace (Needle x))
-                         => Interior x -> [Needle x] -> Shade x
+                         => x -> [Needle x] -> Shade x
 pattern x :± shs <- (Shade x (varianceSpanningSystem -> shs))
  where x :± shs = fullShade x $ spanVariance shs
 
@@ -418,8 +499,7 @@
 --   Note that '|±|' is only possible, as such, in an inner-product space; in
 --   general you need reciprocal vectors ('Needle'') to define a 'Shade''.
 (|±|) :: ∀ x . WithField ℝ EuclidSpace x => x -> [Needle x] -> Shade' x
-(|±|) = case boundarylessWitness :: BoundarylessWitness x of
-   BoundarylessWitness -> \x shs -> Shade' x $ spanNorm [v^/(v<.>v) | v<-shs]
+x|±|shs = Shade' x $ spanNorm [v^/(v<.>v) | v<-shs]
 
 
 
@@ -437,12 +517,12 @@
 --   for each connected component. And for an empty input list, there is no shade!
 --   Hence the result type is a list.
 pointsShades :: (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
-                                 => [Interior x] -> [Shade x]
-pointsShades = map snd . pointsShades' mempty . map ((,()) . fromInterior)
+                                 => [x] -> [Shade x]
+pointsShades = map snd . pointsShades' mempty . map ((,()))
 
 coverAllAround :: ∀ x s . ( Fractional' s, WithField s PseudoAffine x
                           , SimpleSpace (Needle x) )
-                  => Interior x -> [Needle x] -> Shade x
+                  => x -> [Needle x] -> Shade x
 coverAllAround x₀ offs = Shade x₀
          $ guaranteeIn dualSpaceWitness offs
                (scaleNorm (1/fromIntegral (length offs)) $ spanVariance offs)
@@ -463,33 +543,33 @@
 --   the shade, i.e. if @['Shade' x₀ ex]@ is the result then
 --   @'metric' (recipMetric ex) (p-x₀) ≤ 1@ for all @p@ in the list.
 pointsCovers :: ∀ x . (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
-                          => [Interior x] -> [Shade x]
+                          => [x] -> [Shade x]
 pointsCovers = case pseudoAffineWitness :: PseudoAffineWitness x of
-                 (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)) ->
+                 (PseudoAffineWitness (SemimanifoldWitness)) ->
                   \ps -> map (\(ps', Shade x₀ _)
                                 -> coverAllAround x₀ [v | (p,())<-ps'
                                                         , let Just v
-                                                                 = p.-~.fromInterior x₀])
-                             (pointsShades' mempty ((,()).fromInterior<$>ps)
+                                                                 = p.-~.x₀])
+                             (pointsShades' mempty ((,())<$>ps)
                                   :: [([(x,())], Shade x)])
 
 pointsShade's :: ∀ x . (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
-                     => [Interior x] -> [Shade' x]
+                     => [x] -> [Shade' x]
 pointsShade's = case dualSpaceWitness :: DualNeedleWitness x of
  DualSpaceWitness -> map (\(Shade c e :: Shade x) -> Shade' c $ dualNorm e) . pointsShades
 
 pointsCover's :: ∀ x . (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
-                     => [Interior x] -> [Shade' x]
+                     => [x] -> [Shade' x]
 pointsCover's = case dualSpaceWitness :: DualNeedleWitness x of
  DualSpaceWitness -> map (\(Shade c e :: Shade x) -> Shade' c $ dualNorm e) . pointsCovers
 
 pseudoECM :: ∀ x y p . (WithField ℝ PseudoAffine x, SimpleSpace (Needle x), Hask.Functor p)
                 => p x -> NonEmpty (x,y) -> (x, ([(x,y)],[(x,y)]))
 pseudoECM = case semimanifoldWitness :: SemimanifoldWitness x of
- SemimanifoldWitness _ ->
+ SemimanifoldWitness ->
    \_ ((p₀,y₀) NE.:| psr) -> foldl' ( \(acc, (rb,nr)) (i,(p,y))
-                                -> case (p.-~.acc, toInterior acc) of 
-                                      (Just δ, Just acci)
+                                -> case (p.-~.acc, acc) of 
+                                      (Just δ, acci)
                                         -> (acci .+~^ δ^/i, ((p,y):rb, nr))
                                       _ -> (acc, (rb, (p,y):nr)) )
                              (p₀, mempty)
@@ -498,8 +578,8 @@
 pointsShades' :: ∀ x y . (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
                                 => Metric' x -> [(x,y)] -> [([(x,y)], Shade x)]
 pointsShades' _ [] = []
-pointsShades' minExt ps = case (expa, toInterior ctr) of 
-                           (Just e, Just c)
+pointsShades' minExt ps = case (expa, ctr) of 
+                           (Just e, c)
                              -> (ps, fullShade c e) : pointsShades' minExt unreachable
                            _ -> pointsShades' minExt inc'd
                                   ++ pointsShades' minExt unreachable
@@ -517,16 +597,16 @@
                       --   in the same connected region of a manifold are merged.
                  -> [Shade x] -- ^ A list of /n/ shades.
                  -> [Shade x] -- ^ /m/ &#x2264; /n/ shades which cover at least the same area.
-shadesMerge fuzz (sh₁@(Shade c₁ e₁) : shs)
+shadesMerge fuzz (sh@(Shade c₁ e₁) : shs)
     = case extractJust (tryMerge pseudoAffineWitness dualSpaceWitness)
                  shs of
           (Just mg₁, shs') -> shadesMerge fuzz
                                 $ shs'++[mg₁] -- Append to end to prevent undue weighting
                                               -- of first shade and its mergers.
-          (_, shs') -> sh₁ : shadesMerge fuzz shs' 
+          (_, shs') -> sh : shadesMerge fuzz shs' 
  where tryMerge :: PseudoAffineWitness x -> DualNeedleWitness x
                          -> Shade x -> Maybe (Shade x)
-       tryMerge (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)) DualSpaceWitness
+       tryMerge (PseudoAffineWitness (SemimanifoldWitness)) DualSpaceWitness
                     (Shade c₂ e₂)
            | Just v <- c₁.-~.c₂
            , [e₁',e₂'] <- dualNorm<$>[e₁, e₂] 
@@ -550,7 +630,7 @@
 mixShade's = ms pseudoAffineWitness dualSpaceWitness
  where ms :: PseudoAffineWitness y -> DualNeedleWitness y
                   -> NonEmpty (Shade' y) -> Maybe (Shade' y)
-       ms (PseudoAffineWitness (SemimanifoldWitness _)) DualSpaceWitness
+       ms (PseudoAffineWitness (SemimanifoldWitness)) DualSpaceWitness
                  (Shade' c₀ (Norm e₁):|shs) = sequenceA ciso >> pure mixed
         where ciso = [ci.-~.c₀ | Shade' ci shi <- shs]
               cis = [v | Just v <- ciso]
@@ -562,7 +642,7 @@
                              | ni@(Norm ei) <- Norm e₁ : (_shade'Narrowness<$>shs)
                              | ci <- zeroV : cis
                              ] )
-              Tagged (+^) = translateP :: Tagged y (Interior y->Needle y->Interior y)
+              (+^) = (.+~^)
   -- cc should minimise the quadratic form
   -- β(cc) = ∑ᵢ ⟨cc−cᵢ|eᵢ|cc−cᵢ⟩
   -- = ⟨cc|e₁|cc⟩ + ∑ᵢ₌₁… ⟨cc−c₂|e₂|cc−c₂⟩
@@ -595,8 +675,8 @@
 minusLogOcclusion' (Shade' p₀ δinv)
         = occ (pseudoAffineWitness :: PseudoAffineWitness x)
               (dualSpaceWitness :: DualNeedleWitness x)
- where occ (PseudoAffineWitness (SemimanifoldWitness _)) DualSpaceWitness
-           p = case toInterior p >>= (.-~.p₀) of
+ where occ (PseudoAffineWitness (SemimanifoldWitness)) DualSpaceWitness
+           p = case p.-~.p₀ of
          (Just vd) | mSq <- normSq δinv vd
                    , mSq == mSq  -- avoid NaN
                    -> mSq
@@ -607,8 +687,8 @@
 minusLogOcclusion (Shade p₀ δ)
         = occ (pseudoAffineWitness :: PseudoAffineWitness x)
               (dualSpaceWitness :: DualNeedleWitness x)
- where occ (PseudoAffineWitness (SemimanifoldWitness _)) DualSpaceWitness
-            = \p -> case toInterior p >>= (.-~.p₀) of
+ where occ (PseudoAffineWitness (SemimanifoldWitness)) DualSpaceWitness
+            = \p -> case p.-~.p₀ of
          (Just vd) | mSq <- normSq δinv vd
                    , mSq == mSq  -- avoid NaN
                    -> mSq
@@ -617,61 +697,33 @@
 
 
 
-
-{-# WARNING rangeOnGeodesic "This function never worked properly. Use 'rangeWithinVertices'." #-}
-rangeOnGeodesic :: ∀ i m . 
-      ( WithField ℝ PseudoAffine m, Geodesic m, SimpleSpace (Needle m)
-      , WithField ℝ IntervalLike i, SimpleSpace (Needle i) )
-                     => m -> m -> Maybe (Shade i -> Shade m)
-rangeOnGeodesic = case ( semimanifoldWitness :: SemimanifoldWitness i
-                       , dualSpaceWitness :: DualNeedleWitness i
-                       , dualSpaceWitness :: DualNeedleWitness m ) of
- (SemimanifoldWitness _, DualSpaceWitness, DualSpaceWitness) ->
-  \p₀ p₁ -> geodesicBetween p₀ p₁ >>=
-      \interp -> case pointsShades =<<
-                       [ mapMaybe (toInterior . interp . D¹) [-(1-ε), 1-ε]
-                       | ε <- [0.0001, 0.001, 0.01, 0.1] ] of
-                      defaultSh:_ -> Just $
-                       \(Shade t₀ et) -> case pointsShades
-                         . mapMaybe (toInterior
-                               . interp . (toClosedInterval :: i -> D¹))
-                         $ fromInterior <$> t₀ : [ t₀+^v
-                                                 | v<-normSpanningSystem et ] of
-                       [sh] -> sh
-                       _ -> defaultSh
-                      _ -> Nothing
- where Tagged (+^) = translateP :: Tagged i (Interior i->Needle i->Interior i)
-
-
-rangeWithinVertices :: ∀ s i m t
-        . ( RealFrac' s
-          , WithField s PseudoAffine i, WithField s PseudoAffine m
-          , Geodesic i, Geodesic m
-          , SimpleSpace (Needle i), SimpleSpace (Needle m)
-          , AffineManifold (Interior i), AffineManifold (Interior m)
-          , Object (Affine s) (Interior i), Object (Affine s) (Interior m)
+rangeWithinVertices :: ∀ i m t s
+        . ( Geodesic i
+          , Geodesic m
+          , WithField s AffineManifold (Interior i)
+          , WithField s AffineManifold (Interior m)
+          , SimpleSpace (Needle (Interior i))
+          , SimpleSpace (Needle (Interior m))
+          , SimpleSpace (Needle' (Interior i))
+          , SimpleSpace (Needle' (Interior m))
+          , RealFrac' s
           , Hask.Traversable t )
-          => (Interior i,Interior m) -> t (i,m) -> Maybe (Shade i -> Shade m)
-rangeWithinVertices
-      = case ( semimanifoldWitness :: SemimanifoldWitness i
-             , semimanifoldWitness :: SemimanifoldWitness m ) of
-  (SemimanifoldWitness BoundarylessWitness, SemimanifoldWitness BoundarylessWitness)
-      -> \(cii,cmi) verts ->
-       let ci = fromInterior cii
-           cm = fromInterior cmi
-       in do
-           vs <- sequenceA [ fzip ( middleBetween pi ci >>= (.-~.ci)
-                                  , middleBetween pm cm >>= (.-~.cm) )
+          => (Interior i,Interior m) -> t (i,m)
+               -> Maybe (Shade (Interior i) -> Shade (Interior m))
+rangeWithinVertices (cii,cmi) verts = do
+           vs <- sequenceA [ fzip ( middleBetween pi ci >>= (toInterior>=>(.-~.cii))
+                                  , middleBetween pm cm >>= (toInterior>=>(.-~.cmi)) )
                            | (pi, pm) <- Hask.toList verts ]
-           affinSys <- (correspondingDirections (cii,cmi) vs
-                                 :: Maybe (Embedding (Affine (Scalar (Needle i)))
-                                                     (Interior i) (Interior m)))
+           affinSys <- correspondingDirections @(Interior m) @(Interior i)
+                         (cii,cmi) vs
            return $ embedShade affinSys
-          
+ where ci = fromInterior cii
+       cm = fromInterior cmi
 
 
 
 
+
 data DebugView x where
   DebugView :: ( Show x, Show (Needle x+>Needle' x), LinearShowable (Needle x)
                , Needle' x ~ Needle x ) => DebugView x
@@ -690,7 +742,7 @@
   subShade' :: Shade' y -> Shade' y -> Bool
   subShade' (Shade' ac ae) (Shade' tc te)
         = case pseudoAffineWitness :: PseudoAffineWitness y of
-   PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
+   PseudoAffineWitness (SemimanifoldWitness)
     | Just v <- tc.-~.ac
     , v² <- normSq te v
     , v² <= 1
@@ -709,7 +761,7 @@
   refineShade' (Shade' c₀ (Norm e₁)) (Shade' c₀₂ (Norm e₂))
       = case ( dualSpaceWitness :: DualNeedleWitness y
              , pseudoAffineWitness :: PseudoAffineWitness y ) of
-          (DualSpaceWitness, PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness))
+          (DualSpaceWitness, PseudoAffineWitness (SemimanifoldWitness))
                -> do
            c₂ <- c₀₂.-~.c₀
            let σe = arr $ e₁^+^e₂
@@ -857,7 +909,7 @@
   
 defaultConvolveShade' :: ∀ y . Refinable y => Shade' y -> Shade' (Needle y) -> Shade' y
 defaultConvolveShade' = case (pseudoAffineWitness :: PseudoAffineWitness y) of
-  PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
+  PseudoAffineWitness (SemimanifoldWitness)
     -> \(Shade' y₀ ey) (Shade' δ₀ eδ) -> Shade' (y₀.+~^δ₀)
                                           $ convolveMetric ([]::[y]) ey eδ
 
@@ -930,23 +982,16 @@
 
 instance ∀ x y . (Semimanifold x) => Semimanifold (x`WithAny`y) where
   type Needle (WithAny x y) = Needle x
-  type Interior (WithAny x y) = Interior x `WithAny` y
   WithAny y x .+~^ δx = WithAny y $ x.+~^δx
-  fromInterior (WithAny y x) = WithAny y $ fromInterior x
-  toInterior (WithAny y x) = fmap (WithAny y) $ toInterior x
-  translateP = tpWD
-   where tpWD :: ∀ x y . Semimanifold x => Tagged (WithAny x y)
-                            (Interior x`WithAny`y -> Needle x -> Interior x`WithAny`y)
-         tpWD = Tagged `id` \(WithAny y x) δx -> WithAny y $ tpx x δx
-          where Tagged tpx = translateP :: Tagged x (Interior x -> Needle x -> Interior x)
   semimanifoldWitness = case semimanifoldWitness :: SemimanifoldWitness x of
-      SemimanifoldWitness BoundarylessWitness -> SemimanifoldWitness BoundarylessWitness
+      SemimanifoldWitness -> SemimanifoldWitness
             
 instance (PseudoAffine x) => PseudoAffine (x`WithAny`y) where
+  WithAny _ x .-~! WithAny _ ξ = x.-~!ξ
   WithAny _ x .-~. WithAny _ ξ = x.-~.ξ
   pseudoAffineWitness = case pseudoAffineWitness :: PseudoAffineWitness x of
-      PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
-       -> PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)
+      PseudoAffineWitness (SemimanifoldWitness)
+       -> PseudoAffineWitness (SemimanifoldWitness)
 
 instance (AffineSpace x) => AffineSpace (x`WithAny`y) where
   type Diff (WithAny x y) = Diff x
@@ -1003,12 +1048,12 @@
 
 
 data LtdErrorShowWitness m where
-   LtdErrorShowWitness :: (LtdErrorShow (Interior m), LtdErrorShow (Needle m))
+   LtdErrorShowWitness :: (LtdErrorShow m, LtdErrorShow (Needle m))
                   => PseudoAffineWitness m -> LtdErrorShowWitness m
 
 class Refinable m => LtdErrorShow m where
   ltdErrorShowWitness :: LtdErrorShowWitness m
-  default ltdErrorShowWitness :: (LtdErrorShow (Interior m), LtdErrorShow (Needle m))
+  default ltdErrorShowWitness :: (LtdErrorShow m, LtdErrorShow (Needle m))
                          => LtdErrorShowWitness m
   ltdErrorShowWitness = LtdErrorShowWitness pseudoAffineWitness
   showsPrecShade'_errorLtdC :: Int -> Shade' m -> ShowS
@@ -1018,7 +1063,7 @@
                    . (":±["++) . flip (foldr id) (intersperse (',':) u) . (']':)
    where v = showsPrecShade'_errorLtdC 6 (Shade' c e :: Shade' m)
          u :: [ShowS] = case ltdErrorShowWitness :: LtdErrorShowWitness m of
-           LtdErrorShowWitness (PseudoAffineWitness (SemimanifoldWitness _)) ->
+           LtdErrorShowWitness (PseudoAffineWitness SemimanifoldWitness) ->
              [ showsPrecShade'_errorLtdC 6 (Shade' δ e :: Shade' (Needle m))
              | δ <- varianceSpanningSystem e']
          e = dualNorm' e'
@@ -1028,7 +1073,7 @@
                    . ("|±|["++) . flip (foldr id) (intersperse (',':) u) . (']':)
    where v = showsPrecShade'_errorLtdC 6 sh
          u :: [ShowS] = case ltdErrorShowWitness :: LtdErrorShowWitness m of
-           LtdErrorShowWitness (PseudoAffineWitness (SemimanifoldWitness _)) ->
+           LtdErrorShowWitness (PseudoAffineWitness SemimanifoldWitness) ->
              [ showsPrecShade'_errorLtdC 6 (Shade' δ e :: Shade' (Needle m))
              | δ <- varianceSpanningSystem e']
          e' = dualNorm e
@@ -1071,9 +1116,9 @@
               => LtdErrorShow (x,y) where
   ltdErrorShowWitness = case ( ltdErrorShowWitness :: LtdErrorShowWitness x
                              , ltdErrorShowWitness :: LtdErrorShowWitness y ) of
-   (  LtdErrorShowWitness(PseudoAffineWitness(SemimanifoldWitness BoundarylessWitness))
-    , LtdErrorShowWitness(PseudoAffineWitness(SemimanifoldWitness BoundarylessWitness)) )
-    ->LtdErrorShowWitness(PseudoAffineWitness(SemimanifoldWitness BoundarylessWitness))
+   (  LtdErrorShowWitness(PseudoAffineWitness(SemimanifoldWitness))
+    , LtdErrorShowWitness(PseudoAffineWitness(SemimanifoldWitness)) )
+    ->LtdErrorShowWitness(PseudoAffineWitness(SemimanifoldWitness))
   showsPrecShade'_errorLtdC _ sh = ('(':) . shshx . (',':) . shshy . (')':)
    where (shx,shy) = factoriseShade sh
          shshx = showsPrecShade'_errorLtdC 0 shx 
diff --git a/Data/Manifold/TreeCover.hs b/Data/Manifold/TreeCover.hs
--- a/Data/Manifold/TreeCover.hs
+++ b/Data/Manifold/TreeCover.hs
@@ -24,6 +24,7 @@
 {-# LANGUAGE PatternSynonyms            #-}
 {-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE TemplateHaskell            #-}
@@ -123,7 +124,7 @@
 
 type Depth = Int
 data Wall x = Wall { _wallID :: (Depth,(Int,Int))
-                   , _wallAnchor :: Interior x
+                   , _wallAnchor :: x
                    , _wallNormal :: Needle' x
                    , _wallDistance :: Scalar (Needle x)
                    }
@@ -143,7 +144,7 @@
 subshadeId :: ( WithField ℝ PseudoAffine x, LinearSpace (Needle x)
               , FiniteDimensional (Needle' x) )
                     => Shade x -> x -> (Int, HourglassBulb)
-subshadeId (Shade c expa) = subshadeId' (fromInterior c)
+subshadeId (Shade c expa) = subshadeId' c
                               . NE.fromList $ normSpanningSystem' expa
                  
 
@@ -190,7 +191,7 @@
                 | OverlappingBranches !LeafCount !(Shade x) (NonEmpty (DBranch x y))
   deriving (Generic, Hask.Functor, Hask.Foldable, Hask.Traversable)
 deriving instance ( WithField ℝ PseudoAffine x, Show x
-                  , Show (Interior x), Show (Needle' x), Show (Metric' x) )
+                  , Show x, Show (Needle' x), Show (Metric' x) )
              => Show (ShadeTree x)
            
 data DBranch' x c = DBranch { boughDirection :: !(Needle' x)
@@ -412,9 +413,9 @@
                        (empty, 0)
               $        brs
 positionIndex _ sh@(OverlappingBranches n (Shade c ce) brs) x
-   | PseudoAffineWitness (SemimanifoldWitness _)
+   | PseudoAffineWitness SemimanifoldWitness
                <- pseudoAffineWitness :: PseudoAffineWitness x
-   , Just vx <- toInterior x>>=(.-~.c)
+   , Just vx <- x.-~.c
         = let (_,(i₀,t')) = maximumBy (comparing fst)
                        [ (σ*ω, t')
                        | DBranch d (Hourglass t'u t'd) <- NE.toList $ indexDBranches brs
@@ -429,9 +430,9 @@
 
 fromLeafPoints' :: ∀ x y. (WithField ℝ Manifold x, SimpleSpace (Needle x)) =>
     (Shade x -> [(x,y)] -> NonEmpty (DBranch' x [(x,y)])) -> [(x,y)] -> x`Shaded`y
-fromLeafPoints' sShIdPart = go boundarylessWitness mempty
- where go :: BoundarylessWitness x -> Metric' x -> [(x,y)] -> x`Shaded`y
-       go bw@BoundarylessWitness preShExpa
+fromLeafPoints' sShIdPart = go mempty
+ where go :: Metric' x -> [(x,y)] -> x`Shaded`y
+       go preShExpa
             = \xs -> case pointsShades' (scaleNorm (1/3) preShExpa) xs of
                      [] -> PlainLeaves []
                      [(_,rShade)] -> let trials = sShIdPart rShade xs
@@ -443,9 +444,9 @@
                                          _ -> PlainLeaves xs
                      partitions -> DisjointBranches (length xs)
                                    . NE.fromList
-                                    $ map (\(xs',pShade) -> go bw mempty xs') partitions
+                                    $ map (\(xs',pShade) -> go mempty xs') partitions
         where 
-              branchProc redSh = fmap (fmap $ go bw redSh)
+              branchProc redSh = fmap (fmap $ go redSh)
                                  
               reduce :: Shade x -> NonEmpty (DBranch' x [(x,y)])
                                       -> Maybe (NonEmpty (DBranch' x [(x,y)]))
@@ -464,7 +465,7 @@
 
 
 sShIdPartition' :: (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
-        => Interior x -> [(x,y)] -> NonEmpty (DBranch' x [(x,y)])
+        => x -> [(x,y)] -> NonEmpty (DBranch' x [(x,y)])
                                  -> NonEmpty (DBranch' x [(x,y)])
 sShIdPartition' c xs st
            = foldr (\(p,y) -> let (i,h) = ssi p
@@ -472,7 +473,7 @@
                                                     -> DBranch d (oneBulb h ((p,y):) c))
                                       i )
                    st xs
- where ssi = subshadeId' (fromInterior c) (boughDirection<$>st)
+ where ssi = subshadeId' c (boughDirection<$>st)
 sShIdPartition :: (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
                     => Shade x -> [(x,y)] -> NonEmpty (DBranch' x [(x,y)])
 sShIdPartition (Shade c expa) xs
@@ -516,8 +517,8 @@
 trunks :: ∀ x y . (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
                   => x`Shaded`y -> [Shade x]
 trunks t = case (pseudoAffineWitness :: PseudoAffineWitness x, t) of
-  (PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness), PlainLeaves lvs)
-                                    -> pointsCovers . catMaybes $ toInterior.fst<$>lvs
+  (PseudoAffineWitness SemimanifoldWitness, PlainLeaves lvs)
+                                    -> pointsCovers $ fst<$>lvs
   (_, DisjointBranches _ brs)       -> Hask.foldMap trunks brs
   (_, OverlappingBranches _ sh _)   -> [sh]
 
@@ -604,7 +605,7 @@
                                                    $ NE.zip ioffs djbs
                                                , False )
         where ioffs = NE.scanl (\i -> (+i) . nLeaves) i₀ djbs
-       go sw@(PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness)) envi
+       go sw@(PseudoAffineWitness SemimanifoldWitness) envi
            ct@(i₀, (OverlappingBranches nlvs rob@(Shade robc _) brs))
                 = ( case descentResult of
                      OuterNothing -> f
@@ -632,15 +633,15 @@
                        ++ [(nLeaves bdc₁, bdc₂) | overlap < 1]
                       where overlap = bdir<.>^δxenv
               approach q = [q]
-       go (PseudoAffineWitness (SemimanifoldWitness _)) envi plvs@(i₀, (PlainLeaves _))
+       go (PseudoAffineWitness SemimanifoldWitness) envi plvs@(i₀, (PlainLeaves _))
                          = (f $ purgeRemotes (plvs, envi), True)
        
-       twigProximæ :: PseudoAffineWitness x -> Interior x -> x`Shaded`y -> TwigEnviron x y
+       twigProximæ :: PseudoAffineWitness x -> x -> x`Shaded`y -> TwigEnviron x y
        twigProximæ sw x₀ (DisjointBranches _ djbs)
                = Hask.foldMap (\(i₀,st) -> first (+i₀) <$> twigProximæ sw x₀ st)
                     $ NE.zip ioffs djbs
         where ioffs = NE.scanl (\i -> (+i) . nLeaves) 0 djbs
-       twigProximæ sw@(PseudoAffineWitness (SemimanifoldWitness _))
+       twigProximæ sw@(PseudoAffineWitness SemimanifoldWitness)
                           x₀ ct@(OverlappingBranches _ (Shade xb qb) brs)
                    = twigsaveTrim hither ct
         where Just δxb = x₀ .-~. xb
@@ -669,15 +670,13 @@
 completeTopShading (PlainLeaves plvs) = case ( dualSpaceWitness :: DualNeedleWitness x
                                              , dualSpaceWitness :: DualNeedleWitness y ) of
        (DualSpaceWitness, DualSpaceWitness)
-          -> pointsShade's . catMaybes
-               $ toInterior <$> plvs
+          -> pointsShade's plvs
 completeTopShading (DisjointBranches _ bqs)
                      = take 1 . completeTopShading =<< NE.toList bqs
 completeTopShading t = case ( dualSpaceWitness :: DualNeedleWitness x
                             , dualSpaceWitness :: DualNeedleWitness y ) of
        (DualSpaceWitness, DualSpaceWitness)
-          -> pointsCover's . catMaybes
-                . map toInterior $ onlyLeaves t
+          -> pointsCover's $ onlyLeaves t
 
 
 transferAsNormsDo :: ∀ v . LSpace v => Norm v -> Variance v -> v-+>v
@@ -696,7 +695,7 @@
                             (completeTopShading tr) tr
  where recst _ qsh@(_:_) (DisjointBranches n bqs)
           = undefined -- DisjointBranches n $ NE.zipWith (recst . (:[])) (NE.fromList qsh) bqs
-       recst (DualSpaceWitness,DualSpaceWitness,PseudoAffineWitness (SemimanifoldWitness _))
+       recst (DualSpaceWitness,DualSpaceWitness,PseudoAffineWitness SemimanifoldWitness)
                [sha@(Shade' (_,yc₀) expa₀)] t = fmap fts $ f sha
         where expa'₀ = dualNorm expa₀
               j₀ :: LocalLinear x y
@@ -740,10 +739,10 @@
 leavesWithPotentialNeighbours = map (second snd) . go pseudoAffineWitness 0 0 []
  where go :: PseudoAffineWitness x -> Depth -> Int -> [Wall x] -> x`Shaded`y
                 -> [((x,y), ([Wall x], [Int]))]
-       go (PseudoAffineWitness (SemimanifoldWitness _)) depth n₀ walls (PlainLeaves lvs)
+       go (PseudoAffineWitness SemimanifoldWitness) depth n₀ walls (PlainLeaves lvs)
                = [ ((x,y), ( [ wall & wallDistance .~ d
                          | wall <- walls
-                         , Just vw <- [toInterior x>>=(.-~.wall^.wallAnchor)]
+                         , Just vw <- [x.-~.wall^.wallAnchor]
                          , let d = (wall^.wallNormal)<.>^vw
                          , d < wall^.wallDistance ]
                        , [] ))
@@ -752,7 +751,7 @@
          = snd (foldl' (\(n₀',prev) br -> ( n₀'+nLeaves br
                                           , prev . (go pw depth n₀' walls br++)))
                         (n₀,id) dp) []
-       go pw@(PseudoAffineWitness (SemimanifoldWitness _))
+       go pw@(PseudoAffineWitness SemimanifoldWitness)
                depth n₀ walls (OverlappingBranches _ (Shade brCtr _) dp)
          = reassemble $ snd
              (foldl' assignWalls (n₀,id) . directionIChoices 0 $ NE.toList dp) []
@@ -839,7 +838,7 @@
                              in GenericTree [ (ctr, GenericTree $ (,mempty).fst <$> ps) ]
 onlyNodes (DisjointBranches _ brs) = Hask.foldMap onlyNodes brs
 onlyNodes (OverlappingBranches _ (Shade ctr _) brs)
-              = GenericTree [ ( fromInterior ctr
+              = GenericTree [ ( ctr
                               , Hask.foldMap (Hask.foldMap onlyNodes) brs ) ]
 
 entireTree :: ∀ x y . (WithField ℝ PseudoAffine x, SimpleSpace (Needle x))
@@ -855,7 +854,7 @@
                   | GenericTree sub <- NE.toList $ fmap entireTree brs
                   , (x, GenericTree subt) <- sub ]
 entireTree (OverlappingBranches _ (Shade ctr _) brs)
-    = GenericTree [ ( fromInterior ctr
+    = GenericTree [ ( ctr
                     , GenericTree . ListT . Right
                        $ Hask.foldMap (Hask.foldMap $ treeBranches . entireTree) brs ) ]
 
@@ -936,24 +935,26 @@
                           , SimpleSpace (Needle x) )
          => x`Shaded`y -> x -> Cℝay y
 stiWithDensity (PlainLeaves lvs)
-  | [Shade baryc expa :: Shade x] <- pointsShades . catMaybes 
-                                       $ toInterior . fst <$> lvs
+  | LinearManifoldWitness <- linearManifoldWitness @y
+  , [Shade baryc expa :: Shade x] <- pointsShades $ fst <$> lvs
        = let nlvs = fromIntegral $ length lvs :: ℝ
-             indiShapes = [(Shade pi expa, y) | (p,y) <- lvs
-                                              , Just pi <- [toInterior p]]
+             indiShapes = [(Shade p expa, y) | (p,y) <- lvs]
          in \x -> let lcCoeffs = [ occlusion psh x | (psh, _) <- indiShapes ]
                       dens = sum lcCoeffs
                   in mkCone dens . linearCombo . zip (snd<$>indiShapes)
                        $ (/dens)<$>lcCoeffs
 stiWithDensity (DisjointBranches _ lvs)
-           = \x -> foldr1 qGather $ (`stiWithDensity`x)<$>lvs
+           = case linearManifoldWitness @y of
+          LinearManifoldWitness -> \x -> foldr1 qGather $ (`stiWithDensity`x)<$>lvs
  where qGather (Cℝay 0 _) o = o
        qGather o _ = o
 stiWithDensity (OverlappingBranches n (Shade bc extend) brs)
-           = ovbSWD (dualSpaceWitness, pseudoAffineWitness)
- where ovbSWD :: (DualNeedleWitness x, PseudoAffineWitness x) -> x -> Cℝay y
-       ovbSWD (DualSpaceWitness, PseudoAffineWitness (SemimanifoldWitness _)) x
-                     = case toInterior x>>=(.-~.bc) of
+           = ovbSWD (dualSpaceWitness, pseudoAffineWitness, linearManifoldWitness)
+ where ovbSWD :: (DualNeedleWitness x, PseudoAffineWitness x, LinearManifoldWitness y)
+                     -> x -> Cℝay y
+       ovbSWD (DualSpaceWitness
+          , PseudoAffineWitness SemimanifoldWitness, LinearManifoldWitness) x
+                     = case x.-~.bc of
            Just v
              | dist² <- normSq ε v
              , dist² < 9
@@ -981,20 +982,20 @@
           => (Shade x -> Shade y) -> ShadeTree x -> x`Shaded`y
 spanShading f = unsafeFmapTree (addYs . fmap fst) id id
  where addYs :: NonEmpty x -> NonEmpty (x,y)
-       addYs l = foldr (NE.<|) (fmap (,fromInterior ymid) l     )
-                               (fmap (fromInterior xmid,) yexamp)
-          where [xsh@(Shade xmid _)] = pointsCovers . catMaybes . toList
-                                           $ toInterior<$>l
+       addYs l = foldr (NE.<|) (fmap (,ymid) l     )
+                               (fmap (xmid,) yexamp)
+          where [xsh@(Shade xmid _)] = pointsCovers . toList
+                                           $ l
                 Shade ymid yexpa = f xsh
                 yexamp = [ ymid .+~^ σ*^δy
                          | δy <- varianceSpanningSystem yexpa, σ <- [-1,1] ]
                       
 
 
-coneTip :: (AdditiveGroup v) => Cℝay v
+coneTip :: (AdditiveGroup v, Num (Scalar (Needle v))) => Cℝay v
 coneTip = Cℝay 0 zeroV
 
-mkCone :: AdditiveGroup v => ℝ -> v -> Cℝay v
+mkCone :: (AdditiveGroup v, Real (Scalar (Needle v))) => Scalar (Needle v) -> v -> Cℝay v
 mkCone 0 _ = coneTip
 mkCone h v = Cℝay h v
 
diff --git a/Data/Manifold/Types.hs b/Data/Manifold/Types.hs
--- a/Data/Manifold/Types.hs
+++ b/Data/Manifold/Types.hs
@@ -38,19 +38,20 @@
         , Projective0, Projective1, Projective2
         , Disk1, Disk2, Cone, OpenCone
         , FibreBundle(..), TangentBundle
+        -- * Trivial manifolds
+        , EmptyMfd(..), ZeroDim(..)
         -- * Linear manifolds
-        , ZeroDim(..)
         , ℝ, ℝ⁰, ℝ¹, ℝ², ℝ³, ℝ⁴
         -- * Hyperspheres
         -- ** General form: Stiefel manifolds
         , Stiefel1(..), stiefel1Project, stiefel1Embed
         -- ** Specific examples
         , HasUnitSphere(..)
-        , S⁰(..), S¹(..), pattern S¹, S²(..), pattern S²
+        , S⁰, S⁰_(..), S¹, S¹_(..), pattern S¹, S², S²_(..), pattern S²
         -- * Projective spaces
-        , ℝP⁰(..), ℝP¹(..), pattern ℝP¹,  ℝP²(..), pattern ℝP²
+        , ℝP⁰, ℝP⁰_(..), ℝP¹, ℝP¹_(..), pattern ℝP¹,  ℝP²,  ℝP²_(..), pattern ℝP²
         -- * Intervals\/disks\/cones
-        , D¹(..), D²(..), pattern D²
+        , D¹, D¹_(..), D², D²_(..), pattern D²
         , ℝay
         , CD¹(..), Cℝay(..)
         -- * Affine subspaces
@@ -100,12 +101,10 @@
 #define deriveAffine(c,t)                \
 instance (c) => Semimanifold (t) where {  \
   type Needle (t) = Diff (t);              \
-  fromInterior = id;                        \
-  toInterior = pure;                         \
-  translateP = Tagged (.+~^);                 \
-  (.+~^) = (.+^) };                            \
-instance (c) => PseudoAffine (t) where {        \
-  a.-~.b = pure (a.-.b);      }
+  (.+~^) = (.+^) };                         \
+instance (c) => PseudoAffine (t) where {     \
+  a.-~.b = pure (a.-.b);                      \
+  a.-~!b = a.-.b }
 
 
 newtype Stiefel1Needle v = Stiefel1Needle { getStiefel1Tangent :: UArr.Vector (Scalar v) }
@@ -177,7 +176,7 @@
   type TensorProduct (Stiefel1Needle v) w = Array w
   scalarSpaceWitness = case scalarSpaceWitness :: ScalarSpaceWitness v of
          ScalarSpaceWitness -> ScalarSpaceWitness
-  linearManifoldWitness = LinearManifoldWitness BoundarylessWitness
+  linearManifoldWitness = LinearManifoldWitness
   zeroTensor = Tensor $ Arr.replicate (freeDimension ([]::[v]) - 1) zeroV
   toFlatTensor = LinearFunction $ Tensor . Arr.convert . getStiefel1Tangent
   fromFlatTensor = LinearFunction $ Stiefel1Needle . Arr.convert . getTensorProduct
@@ -239,14 +238,12 @@
          -> Arr.ifoldl' (\w i u -> w ^+^ ((asLinearMap $ f Arr.! i) +$> u)) zeroV t
   composeLinear = bilinearFunction $ \f (LinearMap g)
                      -> LinearMap $ Arr.map (getLinearFunction applyLinear f$) g
+  useTupleLinearSpaceComponents _ = undefined
 
 instance ∀ v .
    ( LinearSpace v, FiniteFreeSpace v, FiniteFreeSpace (DualVector v)
    , StiefelScalar (Scalar v) ) => Semimanifold (Stiefel1 v) where
   type Needle (Stiefel1 v) = Stiefel1Needle v
-  fromInterior = id
-  toInterior = pure
-  translateP = Tagged (.+~^)
   (.+~^) = tpst dualSpaceWitness
    where tpst :: DualSpaceWitness v -> Stiefel1 v -> Stiefel1Needle v -> Stiefel1 v
          tpst DualSpaceWitness (Stiefel1 s) (Stiefel1Needle n)
@@ -276,10 +273,11 @@
 instance ∀ v .
    ( LinearSpace v, FiniteFreeSpace v, FiniteFreeSpace (DualVector v)
    , StiefelScalar (Scalar v) ) => PseudoAffine (Stiefel1 v) where
-  (.-~.) = dpst dualSpaceWitness
-   where dpst :: DualSpaceWitness v -> Stiefel1 v -> Stiefel1 v -> Maybe (Stiefel1Needle v)
+  p.-~.q = pure (p.-~!q)
+  (.-~!) = dpst dualSpaceWitness
+   where dpst :: DualSpaceWitness v -> Stiefel1 v -> Stiefel1 v -> Stiefel1Needle v
          dpst DualSpaceWitness (Stiefel1 s) (Stiefel1 t)
-             = pure . Stiefel1Needle $ case s' UArr.! im of
+             = Stiefel1Needle $ case s' UArr.! im of
                    0 -> uarrScale (recip $ l2norm delis) delis
                    s'i | v <- uarrScale (recip s'i) delis `uarrSubtract` tpro
                        , absv <- l2norm v
diff --git a/Data/Manifold/Types/Primitive.hs b/Data/Manifold/Types/Primitive.hs
--- a/Data/Manifold/Types/Primitive.hs
+++ b/Data/Manifold/Types/Primitive.hs
@@ -39,16 +39,17 @@
         , Projective0, Projective1, Projective2
         , Disk1, Disk2, Cone, OpenCone
         , FibreBundle(..), TangentBundle
+        -- * Trivial manifolds
+        , EmptyMfd(..), ZeroDim(..)
         -- * Linear manifolds
-        , ZeroDim(..)
         , ℝ, ℝ⁰, ℝ¹, ℝ², ℝ³, ℝ⁴
         -- * Hyperspheres
-        , S⁰(..), otherHalfSphere, S¹(..), pattern S¹, S²(..), pattern S²
+        , S⁰, S⁰_(..), otherHalfSphere, S¹, S¹_(..), pattern S¹, S², S²_(..), pattern S²
         -- * Projective spaces
-        , ℝP⁰(..), ℝP¹(..), pattern ℝP¹,  ℝP²(..), pattern ℝP²
+        , ℝP⁰, ℝP⁰_(..), ℝP¹, ℝP¹_(..), pattern ℝP¹,  ℝP²,  ℝP²_(..), pattern ℝP²
         -- * Intervals\/disks\/cones
-        , D¹(..), fromIntv0to1, D²(..), pattern D²
-        , ℝay
+        , D¹, D¹_(..), fromIntv0to1, D², D²_(..), pattern D²
+        , ℝay, ℝay_
         , CD¹(..), Cℝay(..)
         -- * Tensor products
         , type (⊗)(..)
@@ -60,7 +61,7 @@
 
 
 import Math.Manifold.Core.Types
-import Math.Manifold.Core.PseudoAffine (FibreBundle(..), TangentBundle, Interior)
+import Math.Manifold.Core.PseudoAffine (FibreBundle(..), TangentBundle, Semimanifold(..))
 
 import Data.VectorSpace
 import Data.VectorSpace.Free
@@ -122,21 +123,25 @@
   embed x = (embed x, zeroV)
   coEmbed (x,_) = coEmbed x
 
-instance NaturallyEmbedded ℝ⁰ ℝ⁰ where embed = id; coEmbed = id
+instance (Num s, s~s') => NaturallyEmbedded (ZeroDim s) (ZeroDim s') where
+  embed = id; coEmbed = id
 instance NaturallyEmbedded ℝ  ℝ  where embed = id; coEmbed = id
-instance NaturallyEmbedded ℝ² ℝ² where embed = id; coEmbed = id
-instance NaturallyEmbedded ℝ³ ℝ³ where embed = id; coEmbed = id
-instance NaturallyEmbedded ℝ⁴ ℝ⁴ where embed = id; coEmbed = id
+instance (Num s, s~s') => NaturallyEmbedded (V2 s) (V2 s') where
+  embed = id; coEmbed = id
+instance (Num s, s~s') => NaturallyEmbedded (V3 s) (V3 s') where
+  embed = id; coEmbed = id
+instance (Num s, s~s') => NaturallyEmbedded (V4 s) (V4 s') where
+  embed = id; coEmbed = id
 
-instance NaturallyEmbedded S⁰ ℝ where
+instance (RealFloat s, VectorSpace s, s'~s) => NaturallyEmbedded (S⁰_ s) s' where
   embed PositiveHalfSphere = 1
   embed NegativeHalfSphere = -1
   coEmbed x | x>=0       = PositiveHalfSphere
             | otherwise  = NegativeHalfSphere
-instance NaturallyEmbedded S¹ ℝ² where
+instance (RealFloat s, s'~s) => NaturallyEmbedded (S¹_ s) (V2 s') where
   embed (S¹Polar φ) = V2 (cos φ) (sin φ)
   coEmbed (V2 x y) = S¹Polar $ atan2 y x
-instance NaturallyEmbedded S² ℝ³ where
+instance (RealFloat s, s'~s) => NaturallyEmbedded (S²_ s) (V3 s') where
   embed (S²Polar ϑ φ) = V3 (cos φ * sϑ) (sin φ * sϑ) (cos ϑ)
    where sϑ = sin ϑ
   {-# INLINE embed #-}
@@ -144,17 +149,18 @@
    where rxy = sqrt $ x^2 + y^2
   {-# INLINE coEmbed #-}
  
-instance NaturallyEmbedded ℝP² ℝ³ where
+instance (RealFloat s, s'~s) => NaturallyEmbedded (ℝP²_ s) (V3 s') where
   embed (HemisphereℝP²Polar θ φ) = V3 (cθ * cos φ) (cθ * sin φ) (sin θ)
    where cθ = cos θ
   coEmbed (V3 x y z) = HemisphereℝP²Polar (atan2 rxy z) (atan2 y x)
    where rxy = sqrt $ x^2 + y^2
 
-instance NaturallyEmbedded D¹ ℝ where
+instance (RealFloat s, VectorSpace s, s'~s) => NaturallyEmbedded (D¹_ s) s' where
   embed = xParamD¹
   coEmbed = D¹ . max (-1) . min 1
 
-instance (NaturallyEmbedded x p) => NaturallyEmbedded (Cℝay x) (p,ℝ) where
+instance (Real s, NaturallyEmbedded x p, s ~ Scalar (Needle x))
+            => NaturallyEmbedded (Cℝay x) (p, s) where
   embed (Cℝay h p) = (embed p, h)
   coEmbed (v,z) = Cℝay (max 0 z) (coEmbed v)
 
@@ -173,9 +179,11 @@
 --   of positive numbers (including zero, i.e. closed on one end).
 type ℝay = Cℝay ℝ⁰
 
+type ℝay_ r = Cℝay (ZeroDim r)
 
 
 
+
 type Real0 = ℝ⁰
 type Real1 = ℝ
 type RealPlus = ℝay
@@ -290,5 +298,5 @@
 instance Binary ℝP²
 instance Binary D¹
 instance Binary D²
-instance Binary y => Binary (CD¹ y)
-instance Binary y => Binary (Cℝay y)
+instance (Binary y, Binary (Scalar (Needle y))) => Binary (CD¹ y)
+instance (Binary y, Binary (Scalar (Needle y))) => Binary (Cℝay y)
diff --git a/Data/Manifold/Web.hs b/Data/Manifold/Web.hs
--- a/Data/Manifold/Web.hs
+++ b/Data/Manifold/Web.hs
@@ -27,6 +27,7 @@
 {-# LANGUAGE PatternGuards              #-}
 {-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE LiberalTypeSynonyms        #-}
 {-# LANGUAGE TemplateHaskell            #-}
@@ -92,6 +93,8 @@
 import Data.Manifold.TreeCover
 import Data.SetLike.Intersection
 import Data.Manifold.Riemannian
+import Data.Manifold.WithBoundary
+import Data.Manifold.WithBoundary.Class
 import Data.Manifold.Atlas
 import Data.Manifold.Function.LocalModel
 import Data.Manifold.Function.Quadratic
@@ -134,21 +137,15 @@
 
 unlinkedFromWebNodes :: ∀ x y . (WithField ℝ Manifold x, SimpleSpace (Needle x))
                     => (MetricChoice x) -> [(x,y)] -> PointsWeb x y
-unlinkedFromWebNodes = case boundarylessWitness :: BoundarylessWitness x of
-   BoundarylessWitness ->
-       \mf -> unlinkedFromShaded mf . fromLeafPoints_
+unlinkedFromWebNodes mf = unlinkedFromShaded mf . fromLeafPoints_
 
 fromWebNodes :: ∀ x y . (WithField ℝ Manifold x, SimpleSpace (Needle x))
                     => (MetricChoice x) -> [(x,y)] -> PointsWeb x y
-fromWebNodes = case boundarylessWitness :: BoundarylessWitness x of
-   BoundarylessWitness ->
-       \mf -> fromShaded mf . fromLeafPoints_
+fromWebNodes mf = fromShaded mf . fromLeafPoints_
 
 fromTopWebNodes :: ∀ x y . (WithField ℝ Manifold x, SimpleSpace (Needle x))
                     => (MetricChoice x) -> [((x,[Int+Needle x]),y)] -> PointsWeb x y
-fromTopWebNodes = case boundarylessWitness :: BoundarylessWitness x of
-   BoundarylessWitness ->
-       \mf -> fromTopShaded mf . fromLeafPoints_ . map regroup'
+fromTopWebNodes mf = fromTopShaded mf . fromLeafPoints_ . map regroup'
 
 fromShadeTree_auto :: ∀ x . (WithField ℝ Manifold x, SimpleSpace (Needle x))
                               => ShadeTree x -> PointsWeb x ()
@@ -326,7 +323,6 @@
               findInCone cone ((po,pn):ps) | cone`includes`po  = Just ((po,pn), ps)
               findInCone (coneDir, _) ((po,pn):_)
                 | Just wall <- pn^.webBoundingPlane
-                , BoundarylessWitness <- boundarylessWitness :: BoundarylessWitness x
                 , DualSpaceWitness <- dualSpaceWitness :: DualSpaceWitness (Needle x)
                 , testp <- pn^.thisNodeCoord .+~^ (coMetric<$|wall)
                 , (metric |$| testp.-~!me^.thisNodeCoord) > (metric|$|snd po)
@@ -453,18 +449,17 @@
 splitToGridLines web (GridSetup x₀ [GridPlanes dirΩ spcΩ nΩ, linePln])
     = [ ((x₀', linePln), sliceWeb_lin web $ Cutplane x₀' (Stiefel1 dirΩ))
       | k <- [0 .. nΩ-1]
-      , let x₀' = x₀i.+~^(fromIntegral k *^ spcΩ) ]
- where Just x₀i = toInterior x₀
+      , let x₀' = x₀.+~^(fromIntegral k *^ spcΩ) ]
 
 sampleWebAlongGrid_lin :: ∀ x y . ( WithField ℝ Manifold x, SimpleSpace (Needle x)
                                   , Geodesic x, Geodesic y )
                => PointsWeb x y -> GridSetup x -> [(x,Maybe y)]
-sampleWebAlongGrid_lin web grid = finalLine boundarylessWitness
+sampleWebAlongGrid_lin web grid = finalLine
                                       =<< splitToGridLines web grid
- where finalLine :: BoundarylessWitness x -> ((x, GridPlanes x), [(x,y)]) -> [(x,Maybe y)]
-       finalLine BoundarylessWitness ((x₀, GridPlanes _ dir nSpl), verts)
+ where finalLine :: ((x, GridPlanes x), [(x,y)]) -> [(x,Maybe y)]
+       finalLine ((x₀, GridPlanes _ dir nSpl), verts)
           | length verts < 2  = take nSpl $ (,empty)<$>iterate (.+~^dir) x₀
-       finalLine BoundarylessWitness ((x₀, GridPlanes dx dir nSpl), verts)
+       finalLine ((x₀, GridPlanes dx dir nSpl), verts)
                      = take nSpl $ go (x₀,0) intpseq 
         where intpseq = mkInterpolationSeq_lin $ sortBy (comparing fst)
                          [ (dx <.>^ (x.-~!x₀), y) | (x,y) <- verts ]
@@ -674,17 +669,21 @@
                                           ) )
                        | (nid, (δx, ngbNode)) <- node^.nodeNeighbours
                        , nid > node^.thisNodeId
-                       , Just pn <- [toInterior $ ngbNode^.thisNodeCoord]
+                       , let pn = ngbNode^.thisNodeCoord
                        ]
 
 
-acoSnd :: ∀ s v y . ( Object (Affine s) y, Object (Affine s) v
+acoSnd :: ∀ s v y . ( RealFloat'' s, Object (Affine s) y, Object (Affine s) v
                     , LinearSpace v, Scalar v ~ s ) => Affine s y (v,y)
-acoSnd = case ( linearManifoldWitness :: LinearManifoldWitness v
-              , dualSpaceWitness :: DualSpaceWitness (Needle v)
-              , dualSpaceWitness :: DualSpaceWitness (Needle y) ) of
-   (LinearManifoldWitness BoundarylessWitness, DualSpaceWitness, DualSpaceWitness)
+acoSnd = needleIsOpenMfd @y (boundaryHasSameScalar @y (
+           needleBoundaryIsTriviallyProjectible @y (boundaryHasSameScalar @v (case
+              ( linearManifoldWitness @v
+              , dualSpaceWitness @(Needle v), dualSpaceWitness @(Needle y)
+              , semimanifoldWitness @y
+              ) of
+   (LinearManifoldWitness, DualSpaceWitness, DualSpaceWitness, SemimanifoldWitness)
        -> const zeroV &&& id
+  ))))
 
 
 differentiate²UncertainWebFunction :: ∀ x y
@@ -698,10 +697,9 @@
          => DifferentialEqn ㄇ x y -> WebLocally x (Shade' y) -> Maybe (Shade' y)
 rescanPDELocally = case ( dualSpaceWitness :: DualNeedleWitness x
                         , dualSpaceWitness :: DualNeedleWitness y
-                        , boundarylessWitness :: BoundarylessWitness x
                         , pseudoAffineWitness :: PseudoAffineWitness y ) of
-   ( DualSpaceWitness,DualSpaceWitness,BoundarylessWitness
-    , PseudoAffineWitness (SemimanifoldWitness BoundarylessWitness) )
+   ( DualSpaceWitness,DualSpaceWitness
+    , PseudoAffineWitness SemimanifoldWitness )
      -> \f info
           -> if isJust $ info^.webBoundingPlane
               then return $ info^.thisNodeData
@@ -889,9 +887,8 @@
                      ( ModellableRelation x y, Hask.MonadPlus m, LocalModel ㄇ )
        => InformationMergeStrategy [] m  (x,Shade' y) iy -> Embedding (->) (Shade' y) iy
           -> DifferentialEqn ㄇ x y -> PointsWeb x iy -> m (PointsWeb x iy)
-filterDEqnSolutions_static = case geodesicWitness :: GeodesicWitness y of
-   GeodesicWitness _ -> \strategy shading f
-       -> webLocalInfo
+filterDEqnSolutions_static strategy shading f
+       = webLocalInfo
            >>> fmap (id &&& rescanPDELocally f . fmap (shading>-$))
            >>> localFocusWeb >>> Hask.traverse ( \((_,(me,updShy)), ngbs)
           -> let oldValue = me^.thisNodeData :: iy
@@ -900,8 +897,7 @@
                  else case updShy of
               Just shy -> case ngbs of
                   []  -> pure oldValue
-                  _:_ | BoundarylessWitness <- (boundarylessWitness::BoundarylessWitness x)
-                    -> sequenceA [ maybeAlt sj
+                  _:_ -> sequenceA [ maybeAlt sj
                                 >>= \ngbShyð -> fmap ((me^.thisNodeCoord .+~^ δx,)
                                                    . (shading>-$))
                                   . mergeInformation strategy oldValue . Hask.toList
@@ -929,10 +925,8 @@
           -> InformationMergeStrategy [] m  (x,Shade' y) iy
           -> Embedding (->) (Shade' y) iy
           -> DifferentialEqn ㄇ x y -> PointsWeb x iy -> m (PointsWeb x iy)
-filterDEqnSolutions_pathsTowards = case ( geodesicWitness :: GeodesicWitness y
-                                        , boundarylessWitness :: BoundarylessWitness x ) of
-   (GeodesicWitness _, BoundarylessWitness) -> \targetNode strategy shading f
-       -> traversePathsTowards targetNode
+filterDEqnSolutions_pathsTowards targetNode strategy shading f
+       = traversePathsTowards targetNode
             (\(PathStep stepStart stepEnd) -> StateT $
               \odeState ->
                 let apriori = shading >-$ stepEnd^.thisNodeData
@@ -986,9 +980,8 @@
           -> (x -> iy -> badness)
           -> DifferentialEqn ㄇ x y
           -> PointsWeb x iy -> m (PointsWeb x iy)
-filterDEqnSolutions_static_selective = case geodesicWitness :: GeodesicWitness y of
-   GeodesicWitness _ -> \strategy shading badness f
-       ->  -- Integration step: determine at each point from the function values
+filterDEqnSolutions_static_selective strategy shading badness f
+      =    -- Integration step: determine at each point from the function values
            -- what the derivatives should be, and use them to propagate the solution
            -- in all directions. We only spend a single computation step on regions
            -- where nothing much changes (indicating the a-priori information is
@@ -1004,8 +997,7 @@
                  then return oldValue
                  else case me^.nodeNeighbours of
                   [] -> pure oldValue
-                  _:_ | BoundarylessWitness <- (boundarylessWitness::BoundarylessWitness x)
-                    -> WriterT . fmap (\updated
+                  _:_ -> WriterT . fmap (\updated
                                     -> (updated, pure (oldBadness / badHere updated)))
                        $ sequenceA [ fmap ((me^.thisNodeCoord .+~^ δx,)
                                                    . (shading>-$))
@@ -1095,12 +1087,10 @@
              -> PointsWeb x (SolverNodeState x y)
                         -> m (PointsWeb x (SolverNodeState x y))
 filterDEqnSolutions_adaptive mf strategy f badness' oldState
-            = fmap recomputeJacobian $ filterGo boundarylessWitness geodesicWitness
-                                         =<< tryPreproc boundarylessWitness geodesicWitness
- where tryPreproc :: BoundarylessWitness x -> GeodesicWitness y
-                      -> m (PointsWeb x ( (WebLocally x (SolverNodeState x y)
-                                        , [(Shade' y, badness)]) ))
-       tryPreproc BoundarylessWitness (GeodesicWitness _)
+            = fmap recomputeJacobian $ filterGo =<< tryPreproc
+ where tryPreproc :: m (PointsWeb x ( (WebLocally x (SolverNodeState x y)
+                                    , [(Shade' y, badness)]) ))
+       tryPreproc 
                = Hask.traverse addPropagation $ webLocalInfo oldState
         where addPropagation wl
                  | null neighbourInfo = pure (wl, [])
@@ -1127,11 +1117,10 @@
        errTgtModulation = (1-) . (`mod'`1) . negate . sqrt $ fromIntegral totalAge
        badness x = badness' x . (shadeNarrowness %~ (scaleNorm errTgtModulation))
               
-       filterGo :: BoundarylessWitness x -> GeodesicWitness y
-                   -> (PointsWeb x ( (WebLocally x (SolverNodeState x y)
+       filterGo :: (PointsWeb x ( (WebLocally x (SolverNodeState x y)
                                    , [(Shade' y, badness)]) ))
                    -> m (PointsWeb x (SolverNodeState x y))
-       filterGo BoundarylessWitness (GeodesicWitness _) preproc'd
+       filterGo preproc'd
              = fmap (smoothenWebTopology mf
                                      . fromTopWebNodes mf . concat . fmap retraceBonds
                                         . Hask.toList . webLocalInfo . webLocalInfo)
diff --git a/Data/Manifold/Web/Internal.hs b/Data/Manifold/Web/Internal.hs
--- a/Data/Manifold/Web/Internal.hs
+++ b/Data/Manifold/Web/Internal.hs
@@ -345,7 +345,7 @@
                         -> PointsWeb x y -> PointsWeb x y
 tweakWebGeometry metricf reknit = webLocalInfo >>> fmapNodesInEnvi`id`
          \(NodeInWeb (x₀, (Neighbourhood info _ lm bound)) _)
-             -> let lm' = metricf . Shade (inInterior x₀) $ dualNorm lm
+             -> let lm' = metricf . Shade x₀ $ dualNorm lm
                 in Neighbourhood (info^.thisNodeData)
                             (UArr.fromList . map (subtract $ info^.thisNodeId)
                                      $ reknit info)
diff --git a/Data/Manifold/WithBoundary.hs b/Data/Manifold/WithBoundary.hs
new file mode 100644
--- /dev/null
+++ b/Data/Manifold/WithBoundary.hs
@@ -0,0 +1,629 @@
+-- |
+-- Module      : Data.Manifold.WithBoundary
+-- Copyright   : (c) Justus Sagemüller 2020
+-- License     : GPL v3
+-- 
+-- Maintainer  : (@) jsag $ hvl.no
+-- Stability   : experimental
+-- Portability : portable
+-- 
+
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE UndecidableInstances     #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE FlexibleContexts         #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE DefaultSignatures        #-}
+{-# LANGUAGE DeriveGeneric            #-}
+{-# LANGUAGE StandaloneDeriving       #-}
+{-# LANGUAGE ConstraintKinds          #-}
+{-# LANGUAGE UnicodeSyntax            #-}
+{-# LANGUAGE ScopedTypeVariables      #-}
+{-# LANGUAGE AllowAmbiguousTypes      #-}
+{-# LANGUAGE TypeApplications         #-}
+{-# LANGUAGE EmptyCase                #-}
+{-# LANGUAGE LambdaCase               #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE TypeInType               #-}
+{-# LANGUAGE CPP                      #-}
+
+
+module Data.Manifold.WithBoundary
+        ( SemimanifoldWithBoundary(..), PseudoAffineWithBoundary(..), ProjectableBoundary(..)
+        , SmfdWBoundWitness(..)
+        , AdditiveMonoid(..), HalfSpace(..)
+        ) where
+
+import Data.Manifold.WithBoundary.Class
+
+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 ( Tensor(..), TensorSpace(..)
+                               , LinearMap(..), LinearFunction(..), LinearSpace(..)
+                               , Num', closedScalarWitness, ClosedScalarWitness(..)
+                               , DualSpaceWitness(..), ScalarSpaceWitness(..)
+                               , LinearManifoldWitness(..)
+                               )
+import Math.VectorSpace.Dual
+import Math.VectorSpace.MiscUtil.MultiConstraints (SameScalar)
+import Data.Monoid.Additive
+import Data.Void
+import Linear (V0, V1, V2, V3, V4)
+import qualified Linear.Affine as LinAff
+
+import Control.Applicative
+import Control.Arrow
+
+import qualified GHC.Generics as Gnrx
+import GHC.Generics (Generic, (:*:)(..))
+import Data.Kind (Type)
+import Proof.Propositional (Empty(..))
+
+import Data.CallStack (HasCallStack)
+
+
+
+
+
+#define VectorSpaceSansBoundary(v, s)                         \
+instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
+                   => SemimanifoldWithBoundary (v) where {      \
+  type Interior (v) = v;                                 \
+  type Boundary (v) = EmptyMfd (ZeroDim s);               \
+  type HalfNeedle (v) = ℝay;                             \
+  smfdWBoundWitness = OpenManifoldWitness;                \
+  fromInterior = id;                                     \
+  fromBoundary b = case b of {};                          \
+  separateInterior = Right;                              \
+  p|+^_ = case p of {};                                   \
+  a.+^|b = Right $ a^+^b;                                \
+  extendToBoundary _ _ = Nothing };                       \
+instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
+                  => PseudoAffineWithBoundary (v) where {\
+  _!-|p = case p of {};                                   \
+  (.--!) = (-) };                                        \
+instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
+                => ProjectableBoundary (v) where {              \
+  projectToBoundary _ p = case p of {};                  \
+  marginFromBoundary p = case p of {} }
+
+VectorSpaceSansBoundary(ℝ,ℝ)
+VectorSpaceSansBoundary(V0 s, s)
+VectorSpaceSansBoundary(V1 s, s)
+VectorSpaceSansBoundary(V2 s, s)
+VectorSpaceSansBoundary(V3 s, s)
+VectorSpaceSansBoundary(V4 s, s)
+
+data ProductBoundary a b
+  = BoundOfL !(Boundary a) !(Interior b)
+  | BoundOfR !(Interior a) !(Boundary b)
+
+data ProductBoundaryNeedleT (dn :: Dualness) a b v
+  = ZeroProductBoundaryNeedle
+  | NBoundOfL !(dn`Space`Needle (Boundary a)) !(dn`Space`Needle (Interior b)) !v
+  | NBoundOfR !(dn`Space`Needle (Interior a)) !(dn`Space`Needle (Boundary b)) !v
+type ProductBoundaryNeedle a b = ProductBoundaryNeedleT Vector a b
+                                     (Scalar (Needle (Interior a)))
+
+instance ( AdditiveGroup (dn`Space`Needle (Boundary a))
+         , AdditiveGroup (dn`Space`Needle (Interior b))
+         , AdditiveGroup (dn`Space`Needle (Interior a))
+         , AdditiveGroup (dn`Space`Needle (Boundary b))
+         , AdditiveGroup v
+         , ValidDualness dn )
+    => AffineSpace (ProductBoundaryNeedleT dn a b v) where
+  type Diff (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
+  ZeroProductBoundaryNeedle .+^ n = n
+  n .+^ ZeroProductBoundaryNeedle = n
+  NBoundOfL x y v .+^ NBoundOfL ξ υ β = NBoundOfL (x^+^ξ) (y^+^υ) (v^+^β)
+  NBoundOfR x y v .+^ NBoundOfR ξ υ β = NBoundOfR (x^+^ξ) (y^+^υ) (v^+^β)
+  n .-. ZeroProductBoundaryNeedle = n
+  NBoundOfL x y v .-. NBoundOfL ξ υ β = NBoundOfL (x^-^ξ) (y^-^υ) (v^-^β)
+  NBoundOfR x y v .-. NBoundOfR ξ υ β = NBoundOfR (x^-^ξ) (y^-^υ) (v^-^β)
+
+instance ( AdditiveGroup (dn`Space`Needle (Boundary a))
+         , AdditiveGroup (dn`Space`Needle (Interior b))
+         , AdditiveGroup (dn`Space`Needle (Interior a))
+         , AdditiveGroup (dn`Space`Needle (Boundary b))
+         , AdditiveGroup v
+         , ValidDualness dn )
+    => AdditiveGroup (ProductBoundaryNeedleT dn a b v) where
+  zeroV = ZeroProductBoundaryNeedle
+  (^+^) = (.+^)
+  negateV ZeroProductBoundaryNeedle = ZeroProductBoundaryNeedle
+  negateV (NBoundOfL x y v) = NBoundOfL (negateV x) (negateV y) (negateV v)
+  negateV (NBoundOfR x y v) = NBoundOfR (negateV x) (negateV y) (negateV v)
+
+instance ∀ a b v dn .
+         ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
+         , SameScalar VectorSpace
+           '[ 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 )
+    => VectorSpace (ProductBoundaryNeedleT dn a b v) where
+  type Scalar (ProductBoundaryNeedleT dn a b v) = Scalar v
+  (*^) = boundaryHasSameScalar @a (boundaryHasSameScalar @b (
+            case (decideDualness @dn, smfdWBoundWitness @a, smfdWBoundWitness @b) of
+     (VectorWitness, _, _) -> \μ -> \case
+        ZeroProductBoundaryNeedle -> ZeroProductBoundaryNeedle
+        NBoundOfL x y v -> NBoundOfL (μ*^x) (μ*^y) (μ*^v)
+        NBoundOfR x y v -> NBoundOfR (μ*^x) (μ*^y) (μ*^v)
+     (FunctionalWitness, SmfdWBoundWitness, SmfdWBoundWitness)
+                       -> case ( dualSpaceWitness @(Needle (Interior a))
+                               , dualSpaceWitness @(Needle (Boundary a))
+                               , dualSpaceWitness @(Needle (Interior b))
+                               , dualSpaceWitness @(Needle (Boundary b)) ) of
+       (DualSpaceWitness, DualSpaceWitness, DualSpaceWitness, DualSpaceWitness)
+            -> \μ -> \case
+        ZeroProductBoundaryNeedle -> ZeroProductBoundaryNeedle
+        NBoundOfL x y v -> NBoundOfL (μ*^x) (μ*^y) (μ*^v)
+        NBoundOfR x y v -> NBoundOfR (μ*^x) (μ*^y) (μ*^v)
+    ))
+
+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 )
+    => TensorSpace (ProductBoundaryNeedleT dn a b v) where
+  type TensorProduct (ProductBoundaryNeedleT dn a b v) w
+          = ProductBoundaryNeedleT dn a b (v⊗w)
+  wellDefinedVector ZeroProductBoundaryNeedle = Just ZeroProductBoundaryNeedle
+  wellDefinedTensor t@(Tensor ZeroProductBoundaryNeedle) = Just t
+  
+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
+         )
+    => LinearSpace (ProductBoundaryNeedleT dn a b v) where
+  type DualVector (ProductBoundaryNeedleT dn a b v)
+         = ProductBoundaryNeedleT (Dual dn) a b (DualVector v)
+  
+
+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
+         )
+    => Semimanifold (ProductBoundaryNeedleT dn a b v) where
+  type Needle (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
+  (.+~^) = (^+^)
+  semimanifoldWitness = SemimanifoldWitness
+  
+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
+         )
+    => PseudoAffine (ProductBoundaryNeedleT dn a b v) where
+  p.-~.q = pure (p^-^q)
+  (.-~!) = (^-^)
+  
+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))
+         , OpenManifold (Scalar v)
+         , ValidDualness dn
+         )
+    => SemimanifoldWithBoundary (ProductBoundaryNeedleT dn a b v) where
+  type Interior (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
+  type Boundary (ProductBoundaryNeedleT dn a b v) = EmptyMfd v
+  type HalfNeedle (ProductBoundaryNeedleT dn a b v) = ℝay
+  smfdWBoundWitness = OpenManifoldWitness
+
+instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
+                 , SameScalar LinearSpace
+                    '[ Needle (Interior a), Needle (Interior b) ]
+                 , Num' (Scalar (Needle (Interior a)))
+                 )
+   => Semimanifold (ProductBoundary a b) where
+  type Needle (ProductBoundary a b) = ProductBoundaryNeedle a b
+--ProductBoundary x y.+~^(δx, δy)
+--     = case (separateInterior x, separateInterior y) of
+-- (Left bx, Right _) -> case y .+^| δy of
+--            Right iy' -> undefined
+  (.+~^) = undefined
+  semimanifoldWitness = case ( semimanifoldWitness @(Interior a)
+                             , semimanifoldWitness @(Interior b) ) of
+    (SemimanifoldWitness, SemimanifoldWitness)
+       -> undefined -- SemimanifoldWitness
+
+instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
+                 , SameScalar LinearSpace
+                    '[ Needle (Interior a), Needle (Interior b) ]
+                 , Num' (Scalar (Needle (Interior a)))
+                 )
+   => PseudoAffine (ProductBoundary a b) where
+  p.-~!q = case p.-~.q of
+             Just v -> v
+             Nothing -> error "No path found in product-space boundary."
+  (.-~.) = case ( pseudoAffineWitness @(Interior a)
+                , pseudoAffineWitness @(Interior b) ) of
+   (PseudoAffineWitness SemimanifoldWitness, PseudoAffineWitness SemimanifoldWitness)
+    -> let BoundOfL bx y − BoundOfL bξ υ
+             = case (bx.-~.bξ, fromInterior @b y.--.fromInterior υ) of
+                 (Just δbx, Just δy) -> Just $ NBoundOfL δbx δy 1
+                 (_, Nothing) -> Nothing
+           BoundOfL bx y − BoundOfR ξ bυ
+             = case ( fromBoundary @a bx.--.fromInterior ξ
+                    , projectToBoundary (fromInterior @b y) bυ ) of
+                 (Just δbx, Just (δby, dy))
+                    -> Just $ NBoundOfR (δbx^*(1+dy)) δby 1
+                 _ -> Nothing
+       in (−)
+  pseudoAffineWitness = case ( pseudoAffineWitness @(Interior a)
+                             , pseudoAffineWitness @(Interior b) ) of
+    (PseudoAffineWitness SemimanifoldWitness
+     , PseudoAffineWitness SemimanifoldWitness)
+       -> undefined {- PseudoAffineWitness SemimanifoldWitness -}
+
+instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
+                 , SameScalar LinearSpace
+                    '[ Needle (Interior a), Needle (Interior b)
+                     , FullSubspace (HalfNeedle a)
+                     ]
+                 , RealFrac'' (Scalar (Needle (Interior a)))
+                 )
+   => SemimanifoldWithBoundary (ProductBoundary a b) where
+  type Interior (ProductBoundary a b) = ProductBoundary a b
+  type Boundary (ProductBoundary a b) = EmptyMfd (Needle (Boundary a), Needle (Boundary b))
+  type HalfNeedle (ProductBoundary a b) = (HalfNeedle a, Needle (Boundary b))
+  q|+^_ = case q of {}
+  p.+^|q = Right $ p.+~^q
+  fromInterior = id
+  fromBoundary q = case q of {}
+  smfdWBoundWitness = boundaryHasSameScalar @a
+     (case closedScalarWitness @(Scalar (Needle (Interior a))) of
+              ClosedScalarWitness -> OpenManifoldWitness)
+  needleIsOpenMfd r = needleIsOpenMfd @a (needleIsOpenMfd @b
+                        (case closedScalarWitness @(Scalar (Needle (Interior a))) of
+                           ClosedScalarWitness -> r))
+  extendToBoundary q = case q of {}
+  scalarIsOpenMfd r = boundaryHasSameScalar @a
+     (case closedScalarWitness @(Scalar (Needle (Interior a))) of
+              ClosedScalarWitness -> r)
+  boundaryHasSameScalar r = boundaryHasSameScalar @a (boundaryHasSameScalar @b
+     (case closedScalarWitness @(Scalar (Needle (Interior a))) of
+              ClosedScalarWitness -> r))
+
+instance (Empty (Boundary a), Empty (Boundary b)) => Empty (ProductBoundary a b) where
+  eliminate (BoundOfL ba _) = eliminate ba
+  eliminate (BoundOfR _ bb) = eliminate bb
+
+data ProductHalfNeedle a b
+  = ProductHalfNeedle !(Needle (Interior a)) !(Needle (Interior b))
+
+instance (AdditiveGroup (Needle (Interior a)), AdditiveGroup (Needle (Interior b)))
+             => AdditiveMonoid (ProductHalfNeedle a b) where
+  zeroHV = ProductHalfNeedle zeroV zeroV
+  addHVs (ProductHalfNeedle v w) (ProductHalfNeedle ϋ ĥ)
+            = ProductHalfNeedle (v^+^ϋ) (w^+^ĥ)
+instance ( SemimanifoldWithBoundary a
+         , SameScalar VectorSpace
+            '[ Needle (Interior a), Needle (Interior b) ]
+         , RealFrac'' (Scalar (Needle (Interior a)))
+         ) => HalfSpace (ProductHalfNeedle a b) where
+  type FullSubspace (ProductHalfNeedle a b) = ProductBoundaryNeedle a b
+  type Ray (ProductHalfNeedle a b) = ℝay_ (Scalar (Needle (Interior a)))
+  type MirrorJoin (ProductHalfNeedle a b) = (Needle (Interior a), Needle (Interior b))
+  scaleNonNeg = case smfdWBoundWitness @a of
+     SmfdWBoundWitness 
+        -> boundaryHasSameScalar @a (\(Cℝay μ Origin) (ProductHalfNeedle v w)
+         -> ProductHalfNeedle (μ*^v) (μ*^w))
+  fromFullSubspace ZeroProductBoundaryNeedle = zeroHV
+  fullSubspaceIsVectorSpace q = undefined
+  projectToFullSubspace = undefined
+  rayIsHalfSpace _ = undefined
+  fromPositiveHalf = undefined
+  fromNegativeHalf = undefined
+
+instance ∀ a b .
+         ( ProjectableBoundary a, ProjectableBoundary b
+         , SameScalar LinearSpace
+            '[ Needle (Interior a), Needle (Interior b)
+             ]
+         , RealFrac'' (Scalar (Needle (Interior a)))
+         , ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
+         ) => SemimanifoldWithBoundary (a,b) where
+  type Interior (a,b) = (Interior a, Interior b)
+  type Boundary (a,b) = ProductBoundary a b
+  type HalfNeedle (a,b) = ProductHalfNeedle a b
+  extendToBoundary = undefined
+  smfdWBoundWitness = case (smfdWBoundWitness @a, smfdWBoundWitness @b) of
+    (OpenManifoldWitness, OpenManifoldWitness)
+        -> needleIsOpenMfd @a (needleIsOpenMfd @b (
+             boundaryHasSameScalar @(Needle a) (boundaryHasSameScalar @(Needle b)
+               (case (semimanifoldWitness @(Interior a), semimanifoldWitness @(Interior b))
+                 of (SemimanifoldWitness, SemimanifoldWitness)
+                        -> needleBoundaryIsTriviallyProjectible @a
+                            (needleBoundaryIsTriviallyProjectible @b OpenManifoldWitness) )
+            )))
+    (SmfdWBoundWitness, SmfdWBoundWitness)
+        -> boundaryHasSameScalar @a
+            (boundaryHasSameScalar @b
+              (needleIsOpenMfd @(Interior a)
+                (needleIsOpenMfd @(Interior b)
+                  (case ( semimanifoldWitness @(Interior a)
+                        , semimanifoldWitness @(Interior b)
+                        , closedScalarWitness @(Scalar (Needle (Interior a)))
+                        )
+                 of (SemimanifoldWitness, SemimanifoldWitness, ClosedScalarWitness)
+                        -> needleBoundaryIsTriviallyProjectible @a
+                            (needleBoundaryIsTriviallyProjectible @b
+                              (boundaryHasSameScalar @(Needle (Interior a))
+                                (boundaryHasSameScalar @(Needle (Interior b))
+                                  SmfdWBoundWitness)))))))
+  boundaryHasSameScalar q = undefined
+  needleIsOpenMfd _ = undefined
+
+instance ∀ a b .
+         ( ProjectableBoundary a, ProjectableBoundary b
+         , SameScalar LinearSpace
+            '[ Needle (Interior a), Needle (Interior b)
+             , Needle (Boundary a), Needle (Boundary b)
+             ]
+         , ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
+         , RealFrac'' (Scalar (Needle (Interior a)))
+         ) => PseudoAffineWithBoundary (a,b) where
+
+instance ∀ a b .
+         ( ProjectableBoundary a, ProjectableBoundary b
+         , SameScalar LinearSpace
+            '[ Needle (Interior a), Needle (Interior b)
+             , Needle (Boundary a), Needle (Boundary b)
+             ]
+         , ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
+         , RealFrac'' (Scalar (Needle (Interior a)))
+         ) => ProjectableBoundary (a,b) where
+  needleBoundaryIsTriviallyProjectible q
+      = needleBoundaryIsTriviallyProjectible @a
+         (needleBoundaryIsTriviallyProjectible @b
+           (boundaryHasSameScalar @(Needle (Interior a))
+             (boundaryHasSameScalar @(Needle (Interior b))
+               (needleIsOpenMfd @a
+                 (needleIsOpenMfd @b
+                   (case (semimanifoldWitness @(Interior a), semimanifoldWitness @(Interior b))
+                     of (SemimanifoldWitness, SemimanifoldWitness) -> q))))))
+
+instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S⁰_ s) where
+  type Interior (S⁰_ s) = S⁰_ s
+  type Boundary (S⁰_ s) = EmptyMfd (ZeroDim s)
+  type HalfNeedle (S⁰_ s) = ZeroDim s
+  fromInterior = id
+  fromBoundary b = case b of {}
+  separateInterior = Right
+  p|+^_ = case p of {}
+  NegativeHalfSphere .+^| Origin = Right NegativeHalfSphere
+  PositiveHalfSphere .+^| Origin = Right PositiveHalfSphere
+  extendToBoundary _ _ = Nothing
+  smfdWBoundWitness = OpenManifoldWitness
+
+instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S¹_ s) where
+  type Interior (S¹_ s) = (S¹_ s)
+  type Boundary (S¹_ s) = EmptyMfd (ZeroDim s)
+  type HalfNeedle (S¹_ s) = ℝay_ s
+  fromInterior = id
+  fromBoundary b = case b of {}
+  separateInterior = Right
+  p|+^_ = case p of {}
+  _ .+^| p = case p of {}
+  extendToBoundary _ _ = Nothing
+  smfdWBoundWitness = case closedScalarWitness @s of ClosedScalarWitness -> OpenManifoldWitness
+  scalarIsOpenMfd q = case closedScalarWitness @s of ClosedScalarWitness -> q
+  boundaryHasSameScalar q = case closedScalarWitness @s of ClosedScalarWitness -> q
+
+instance ∀ s . RealFloat'' s => PseudoAffineWithBoundary (S¹_ s) where
+  _!-|p = case p of {}
+  (.--!) = (.-~!)
+
+instance ∀ s . RealFloat'' s => ProjectableBoundary (S¹_ s) where
+  scalarBoundaryIsTriviallyProjectible q = case closedScalarWitness @s of
+     ClosedScalarWitness -> q
+  projectToBoundary _ p = case p of {}
+  marginFromBoundary p = case p of {}
+
+instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S²_ s) where
+  type Interior (S²_ s) = S²_ s
+  type Boundary (S²_ s) = EmptyMfd s
+  type HalfNeedle (S²_ s) = ℝay_ s
+  fromInterior = id
+  fromBoundary b = case b of {}
+  separateInterior = Right
+  p|+^_ = case p of {}
+  _ .+^| p = case p of {}
+  extendToBoundary _ _ = Nothing
+  smfdWBoundWitness = case closedScalarWitness @s of ClosedScalarWitness -> OpenManifoldWitness
+  scalarIsOpenMfd q = case closedScalarWitness @s of ClosedScalarWitness -> q
+  boundaryHasSameScalar q = case closedScalarWitness @s of ClosedScalarWitness -> q
+
+instance ∀ s . RealFloat'' s => PseudoAffineWithBoundary (S²_ s) where
+  _!-|p = case p of {}
+  (.--!) = (.-~!)
+
+instance ∀ s . RealFloat'' s => ProjectableBoundary (S²_ s) where
+  scalarBoundaryIsTriviallyProjectible q = case closedScalarWitness @s of
+     ClosedScalarWitness -> q
+  projectToBoundary _ p = case p of {}
+  marginFromBoundary p = case p of {}
+
+
+instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (D¹_ s) where
+  type Interior (D¹_ s) = s
+  type Boundary (D¹_ s) = (S⁰_ s)
+  type HalfNeedle (D¹_ s) = ℝay_ s
+  fromBoundary NegativeHalfSphere = D¹ (-1)
+  fromBoundary PositiveHalfSphere = D¹ 1
+  fromInterior = D¹ . tanh
+  separateInterior (D¹ (-1)) = Left NegativeHalfSphere
+  separateInterior (D¹ 1) = Left PositiveHalfSphere
+  separateInterior (D¹ x) = Right $ atanh x
+  NegativeHalfSphere|+^Cℝay l Origin = D¹ $ 1 - 4/(l+2)
+  PositiveHalfSphere|+^Cℝay l Origin = D¹ $ 4/(l+2) - 1
+  (.+^|) = case (linearManifoldWitness @s, closedScalarWitness @s) of
+   (LinearManifoldWitness, ClosedScalarWitness) ->
+    let addBD¹ (D¹ p) l
+          | p' >= 1    = Left (PositiveHalfSphere, (p'-1) / l)
+          | p' <= -1   = Left (NegativeHalfSphere, (p'+1) / l)
+          | otherwise  = Right $ atanh p'
+         where p' = p+l
+    in addBD¹
+  extendToBoundary = case (linearManifoldWitness @s, closedScalarWitness @s) of
+   (LinearManifoldWitness, ClosedScalarWitness) ->
+    let e2b _ dir
+         | dir > 0    = Just PositiveHalfSphere
+         | dir < 0    = Just NegativeHalfSphere
+         | otherwise  = Nothing
+    in e2b
+  smfdWBoundWitness = case closedScalarWitness @s of ClosedScalarWitness -> SmfdWBoundWitness
+  scalarIsOpenMfd q = case (closedScalarWitness @s, linearManifoldWitness @s) of
+   (ClosedScalarWitness, LinearManifoldWitness) -> q
+  boundaryHasSameScalar q = case (closedScalarWitness @s, linearManifoldWitness @s) of
+   (ClosedScalarWitness, LinearManifoldWitness) -> q
+  needleIsOpenMfd q = case (closedScalarWitness @s, linearManifoldWitness @s) of
+   (ClosedScalarWitness, LinearManifoldWitness) -> q
+
+
+instance ( Num' n, OpenManifold n, LinearManifold (a n)
+         , Scalar (a n) ~ n, Needle (a n) ~ a n )
+            => SemimanifoldWithBoundary (LinAff.Point a n) where
+  type Boundary (LinAff.Point a n) = EmptyMfd (ZeroDim n)
+  type Interior (LinAff.Point a n) = LinAff.Point a n
+  type HalfNeedle (LinAff.Point a n) = ℝay
+  smfdWBoundWitness = OpenManifoldWitness
+  LinAff.P p.+^|v = Right . LinAff.P $ p^+^v
+  fromInterior = id
+  fromBoundary b = case b of {}
+  b|+^_ = case b of {}
+
+instance ( Num' n, OpenManifold n, LinearManifold (a n)
+         , Scalar (a n) ~ n, Needle (a n) ~ a n )
+            => PseudoAffineWithBoundary (LinAff.Point a n) where
+  LinAff.P p.--!LinAff.P q = p^-^q
+  _!-|b = case b of {}
+
+instance ∀ n a .  ( Num' n, OpenManifold n, LinearManifold (a n), ProjectableBoundary n
+                  , Scalar (a n) ~ n, Needle (a n) ~ a n )
+            => ProjectableBoundary (LinAff.Point a n) where
+  projectToBoundary _ b = case b of {}
+  marginFromBoundary b _ = case b of {}
+
+instance ( LinearSpace v, LinearSpace w
+         , s ~ Scalar v, s ~ Scalar w
+         , Num' s, OpenManifold s
+         ) => SemimanifoldWithBoundary (Tensor s v w) where
+  type Interior (Tensor s v w) = (Tensor s v w)
+  type Boundary (Tensor s v w) = EmptyMfd (ZeroDim s)
+  type HalfNeedle (Tensor s v w) = ℝay_ s
+  smfdWBoundWitness = OpenManifoldWitness
+  fromInterior = id
+  fromBoundary b = case b of {}
+  separateInterior = Right
+  p|+^_ = case p of {}
+  a.+^|b = Right $ a^+^b
+  extendToBoundary _ _ = Nothing
+
+instance ( LinearSpace v, LinearSpace w
+         , s ~ Scalar v, s ~ Scalar w
+         , Num' s, OpenManifold s
+         ) => PseudoAffineWithBoundary (Tensor s v w) where
+  _!-|p = case p of {}
+  (.--!) = (^-^)
+
+instance ( LinearSpace v, LinearSpace w
+         , s ~ Scalar v, s ~ Scalar w
+         , Num' s, OpenManifold s
+         ) => SemimanifoldWithBoundary (LinearMap s v w) where
+  type Interior (LinearMap s v w) = (LinearMap s v w)
+  type Boundary (LinearMap s v w) = EmptyMfd (ZeroDim s)
+  type HalfNeedle (LinearMap s v w) = ℝay
+  smfdWBoundWitness = OpenManifoldWitness
+  fromInterior = id
+  fromBoundary b = case b of {}
+  separateInterior = Right
+  p|+^_ = case p of {}
+  a.+^|b = Right $ a^+^b
+  extendToBoundary _ _ = Nothing
+
+instance ( LinearSpace v, LinearSpace w
+         , s ~ Scalar v, s ~ Scalar w
+         , Num' s, OpenManifold s, ProjectableBoundary s
+         ) => ProjectableBoundary (LinearMap s v w) where
+  projectToBoundary _ p = case p of {}
+  marginFromBoundary p = case p of {}
+
+instance ( LinearSpace v, LinearSpace w
+         , s ~ Scalar v, s ~ Scalar w
+         , Num' s, OpenManifold s
+         ) => PseudoAffineWithBoundary (LinearMap s v w) where
+  _!-|p = case p of {}
+  (.--!) = (^-^)
+
+instance ( LinearSpace v, LinearSpace w
+         , s ~ Scalar v, s ~ Scalar w
+         , Num' s, OpenManifold s
+         ) => SemimanifoldWithBoundary (LinearFunction s v w) where
+  type Interior (LinearFunction s v w) = (LinearFunction s v w)
+  type Boundary (LinearFunction s v w) = EmptyMfd (ZeroDim s)
+  type HalfNeedle (LinearFunction s v w) = ℝay
+  smfdWBoundWitness = OpenManifoldWitness
+  fromInterior = id
+  fromBoundary b = case b of {}
+  separateInterior = Right
+  p|+^_ = case p of {}
+  a.+^|b = Right $ a^+^b
+  extendToBoundary _ _ = Nothing
+
+instance ( LinearSpace v, LinearSpace w
+         , s ~ Scalar v, s ~ Scalar w
+         , Num' s, OpenManifold s
+         ) => PseudoAffineWithBoundary (LinearFunction s v w) where
+  _!-|p = case p of {}
+  (.--!) = (^-^)
+
+
+
+instance ( Semimanifold a
+         , Semimanifold (VRep a), Needle a ~ GenericNeedle a
+         , OpenManifold (Scalar (Needle (Gnrx.Rep a Void)))
+         , LinearSpace (Needle (Gnrx.Rep a Void))
+         , Num' (Scalar (Needle (Gnrx.Rep a Void))) )
+            => SemimanifoldWithBoundary (GenericNeedle a) where
+  type Interior (GenericNeedle a) = GenericNeedle a
+  type Boundary (GenericNeedle a) = EmptyMfd (ZeroDim (Scalar (Needle (Gnrx.Rep a Void))))
+  type HalfNeedle (GenericNeedle a) = ℝay_ (Scalar (Needle (Gnrx.Rep a Void)))
+  extendToBoundary _ _ = Nothing
+  smfdWBoundWitness = OpenManifoldWitness
+  needleIsOpenMfd q = q
+  scalarIsOpenMfd q = q
+  boundaryHasSameScalar q = q
+  b|+^_ = case b of {}
+  p .+^| k = Right $ p^+^k
+  fromBoundary b = case b of {}
+
+
+instance ( Semimanifold a
+         , Semimanifold (VRep a), Needle a ~ GenericNeedle a
+         , OpenManifold (Scalar (Needle (Gnrx.Rep a Void)))
+         , LinearSpace (Needle (Gnrx.Rep a Void))
+         , Num' (Scalar (Needle (Gnrx.Rep a Void))) )
+            => PseudoAffineWithBoundary (GenericNeedle a) where
+  _ !-| b = case b of {}
+  (.--!) = (^-^)
diff --git a/Data/Manifold/WithBoundary/Class.hs b/Data/Manifold/WithBoundary/Class.hs
new file mode 100644
--- /dev/null
+++ b/Data/Manifold/WithBoundary/Class.hs
@@ -0,0 +1,229 @@
+-- |
+-- Module      : Data.Manifold.WithBoundary.Class
+-- Copyright   : (c) Justus Sagemüller 2021
+-- License     : GPL v3
+-- 
+-- Maintainer  : (@) jsag $ hvl.no
+-- Stability   : experimental
+-- Portability : portable
+-- 
+
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE UndecidableInstances     #-}
+{-# LANGUAGE TypeFamilies             #-}
+{-# LANGUAGE FlexibleContexts         #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE DefaultSignatures        #-}
+{-# LANGUAGE DeriveGeneric            #-}
+{-# LANGUAGE StandaloneDeriving       #-}
+{-# LANGUAGE ConstraintKinds          #-}
+{-# LANGUAGE UnicodeSyntax            #-}
+{-# LANGUAGE ScopedTypeVariables      #-}
+{-# LANGUAGE AllowAmbiguousTypes      #-}
+{-# LANGUAGE TypeApplications         #-}
+{-# LANGUAGE RankNTypes               #-}
+{-# LANGUAGE EmptyCase                #-}
+{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE TypeInType               #-}
+{-# LANGUAGE CPP                      #-}
+
+
+module Data.Manifold.WithBoundary.Class where
+
+import Data.VectorSpace
+import Data.AffineSpace
+import Data.Basis
+
+import Math.Manifold.Core.PseudoAffine
+import Math.Manifold.Core.Types
+import Data.Manifold.Types.Primitive
+import Math.Manifold.VectorSpace.ZeroDimensional
+import Math.LinearMap.Category ( Tensor(..), TensorSpace(..)
+                               , LinearMap(..), LinearFunction(..), LinearSpace(..)
+                               , Num'
+                               )
+import Math.VectorSpace.Dual
+import Math.VectorSpace.MiscUtil.MultiConstraints (SameScalar)
+import Linear (V0, V1, V2, V3, V4)
+import qualified Linear.Affine as LinAff
+import Data.Monoid.Additive
+
+import Control.Applicative
+import Control.Arrow
+
+import qualified GHC.Generics as Gnrx
+import GHC.Generics (Generic, (:*:)(..))
+import Data.Kind (Type)
+import Proof.Propositional (Empty(..))
+
+import Data.CallStack (HasCallStack)
+
+
+type OpenManifold m = ( SemimanifoldWithBoundary m
+                      , SemimanifoldWithBoundary (Needle m)
+                      , LinearSpace (Needle m)
+                      , SemimanifoldWithBoundary (Scalar (Needle m))
+                      , Interior m ~ m
+                      , Empty (Boundary m)
+                      )
+
+data SmfdWBoundWitness m where
+  OpenManifoldWitness :: ∀ m . OpenManifold m
+              => SmfdWBoundWitness m
+  SmfdWBoundWitness :: ∀ m .
+         ( OpenManifold (Interior m), OpenManifold (Boundary m)
+         , FullSubspace (HalfNeedle m) ~ Needle (Boundary m) )
+              => SmfdWBoundWitness m
+
+-- | The class of spaces with a displacement operation like 'Semimanifold', but there
+--   may be a limited range how far it is possible to move before leaving the space.
+-- 
+--   Such spaces decompose into two 'Semimanifold' spaces: the 'Interior' and the 'Boundary'.
+class -- ( Semimanifold (Interior m), Semimanifold (Boundary m)
+      -- , HalfSpace (HalfNeedle m) ) =>
+    SemimanifoldWithBoundary m where
+  -- | Subspace of @m@ representing the set of points where it is possible to move at
+  --   least a small distance in any direction (with '.+^|') without leaving @m@.
+  type Interior m :: Type
+  -- | The set of points where an infinitesimal movement is sufficient to leave @m@.
+  type Boundary m :: Type
+  type HalfNeedle m :: Type
+  -- | Boundary-aware pendant to '.+~^'.
+  (.+^|) :: m
+         -- ^ Starting point @p@
+         -> Needle (Interior m)
+         -- ^ Displacement @v@
+         -> Either (Boundary m, Scalar (Needle (Interior m)))
+                   (Interior m)
+         -- ^ If @v@ is enough to leave @m@, yield the point where it does and what
+         --   fraction of the length is still left (i.e. how much of @v@ “pokes out
+         --   of the space”). If it stays within the space, just give back the result.
+  fromInterior :: Interior m -> m
+  fromBoundary :: Boundary m -> m
+  (|+^) :: Boundary m -> HalfNeedle m -> m
+  separateInterior :: m -> Either (Boundary m) (Interior m)
+  separateInterior p = case smfdWBoundWitness @m of
+   OpenManifoldWitness -> Right p
+   SmfdWBoundWitness -> case p .+^| zeroV of
+    Left (b,_) -> Left b 
+    Right i -> Right i
+  toInterior :: m -> Maybe (Interior m)
+  toInterior p = case separateInterior p of
+    Right i -> Just i
+    Left _  -> Nothing
+  extendToBoundary :: Interior m -> Needle (Interior m) -> Maybe (Boundary m)
+  default extendToBoundary :: ( VectorSpace (Needle (Interior m))
+                              , Num (Scalar (Needle (Interior m))) )
+           => Interior m -> Needle (Interior m) -> Maybe (Boundary m)
+  extendToBoundary p dir = case fromInterior @m p .+^| dir of
+    Right _ -> extendToBoundary @m p $ dir^*2
+    Left (p, _) -> Just p
+  smfdWBoundWitness :: SmfdWBoundWitness m
+  default smfdWBoundWitness 
+              :: ( OpenManifold (Interior m)
+                 , OpenManifold (Boundary m)
+                 , FullSubspace (HalfNeedle m) ~ Needle (Boundary m) )
+                   => SmfdWBoundWitness m
+  smfdWBoundWitness = SmfdWBoundWitness @m
+  needleIsOpenMfd :: (OpenManifold (Needle (Interior m)) => r) -> r
+  default needleIsOpenMfd :: OpenManifold (Needle (Interior m))
+                                 => (OpenManifold (Needle (Interior m)) => r) -> r
+  needleIsOpenMfd q = q
+  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior m))) => r) -> r
+  default scalarIsOpenMfd :: OpenManifold (Scalar (Needle (Interior m)))
+                                 => (OpenManifold (Scalar (Needle (Interior m))) => r) -> r
+  scalarIsOpenMfd q = q
+  boundaryHasSameScalar
+        :: ( ( LinearSpace (Needle (Boundary m))
+             , Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m)) )
+                                => r)-> r
+  default boundaryHasSameScalar
+           :: (( LinearSpace (Needle (Boundary m))
+               , Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))))
+     => (( LinearSpace (Needle (Boundary m))
+         , Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) => r) -> r
+  boundaryHasSameScalar q = q
+  
+
+class (SemimanifoldWithBoundary m, PseudoAffine (Interior m), PseudoAffine (Boundary m))
+          => PseudoAffineWithBoundary m where
+  -- | Inverse of '.+^|', provided the space is connected. For @p :: Interior m@, @q :: m@
+  --   and @v = fromInterior p.--!q@,
+  -- 
+  --   @
+  --   q '.+^|' v ≡ Right p
+  --   @
+  --
+  --   (up to floating-point). Similary, for @b :: Boundary m@ and @w = fromBoundary m.--!q@,
+  -- 
+  --   @
+  --   q '.+^|' w ≡ Left (b, 0)
+  --   @
+  (.--!) :: m -> m -> Needle (Interior m)
+  
+  (.-|) :: m -> Boundary m -> Maybe (HalfNeedle m)
+  p.-|b = Just $ p!-|b
+  (!-|) :: m -> Boundary m -> HalfNeedle m
+  (.--.) :: m -> m -> Maybe (Needle (Interior m))
+  p.--.q = Just $ p.--!q
+
+
+class PseudoAffineWithBoundary m => ProjectableBoundary m where
+  projectToBoundary :: m
+                    -- ^ Point @p@ to project
+                    -> Boundary m 
+                    -- ^ Intended “course region” representative @r@ on boundary – we
+                    --   seek a point that is reachable from there.
+                    -> Maybe ( Needle (Boundary m)
+                             , Scalar (Needle (Interior m)) )
+                    -- ^ Needle @δr@ connecting @r@ to projection of the @p@, and
+                    --   a measure @d@ of normal-distance such that
+                    --   @'marginFromBoundary' (r.+~^δr) d == p@.
+  marginFromBoundary :: Boundary m -> Scalar (Needle (Interior m)) -> m
+  needleBoundaryIsTriviallyProjectible :: ∀ r .
+        (ProjectableBoundary (Needle (Interior m)) => r) -> r
+  default needleBoundaryIsTriviallyProjectible :: ProjectableBoundary (Needle (Interior m))
+           => (ProjectableBoundary (Needle (Interior m)) => r) -> r
+  needleBoundaryIsTriviallyProjectible q = q
+  scalarBoundaryIsTriviallyProjectible :: ∀ r .
+        (ProjectableBoundary (Scalar (Needle (Interior m))) => r) -> r
+  default scalarBoundaryIsTriviallyProjectible
+                      :: ProjectableBoundary (Scalar (Needle (Interior m)))
+           => (ProjectableBoundary (Scalar (Needle (Interior m))) => r) -> r
+  scalarBoundaryIsTriviallyProjectible q = q
+
+instance ∀ k . ( LinearSpace k, OpenManifold k, OpenManifold (Scalar k) )
+             => SemimanifoldWithBoundary (EmptyMfd k) where
+  type Interior (EmptyMfd k) = EmptyMfd k
+  type Boundary (EmptyMfd k) = EmptyMfd k
+  type HalfNeedle (EmptyMfd k) = ZeroDim (Scalar k)
+  smfdWBoundWitness = OpenManifoldWitness @(EmptyMfd k)
+  q|+^_ = case q of {}
+  q.+^|_ = case q of {}
+  fromInterior = id
+  fromBoundary = id
+  scalarIsOpenMfd q = scalarIsOpenMfd @k q
+
+instance ∀ k . (Num' k, OpenManifold k)
+            => SemimanifoldWithBoundary (ZeroDim k) where
+  type Interior (ZeroDim k) = ZeroDim k
+  type Boundary (ZeroDim k) = EmptyMfd (ZeroDim k)
+  type HalfNeedle (ZeroDim k) = ZeroDim k
+  fromInterior = id
+  fromBoundary b = case b of {}
+  separateInterior = Right
+  p|+^_ = case p of {}
+  Origin .+^| Origin = Right Origin
+  extendToBoundary _ _ = Nothing
+  smfdWBoundWitness = scalarIsOpenMfd @k SmfdWBoundWitness
+  scalarIsOpenMfd q = scalarIsOpenMfd @k q
+
+instance (Num' k, OpenManifold k) => PseudoAffineWithBoundary (ZeroDim k) where
+  _.-|p = case p of {}
+  Origin .--! Origin = Origin
+  _!-|q = case q of {}
+
+instance (Num' k, ProjectableBoundary k, OpenManifold k)
+            => ProjectableBoundary (ZeroDim k) where
+  projectToBoundary Origin b = case b of {}
+  marginFromBoundary b _ = case b of {}
diff --git a/Math/Manifold/Real/Coordinates.hs b/Math/Manifold/Real/Coordinates.hs
--- a/Math/Manifold/Real/Coordinates.hs
+++ b/Math/Manifold/Real/Coordinates.hs
@@ -41,6 +41,7 @@
 import Data.Manifold.Types.Stiefel
 import Data.Manifold.PseudoAffine
 import Math.LinearMap.Category
+import Math.VectorSpace.Dual
 import Data.VectorSpace
 
 import Control.Lens hiding ((<.>))
@@ -263,7 +264,7 @@
 shrinkElems l = filter ((==length l) . length) . transpose $ map QC.shrink l
 
 
-location's :: (HasCoordinates b, Interior b ~ b, HasCoordinates f)
+location's :: (HasCoordinates b, HasCoordinates f)
                 => CoordinateIdentifier b -> Coordinate (FibreBundle b f)
 location's = coordinate . BaseSpaceCoordinate
 
@@ -277,7 +278,7 @@
   --   because it has to compensate for the sensitive rotation of the @eφ@ unit vector.
   delta :: CoordinateIdentifier m -> Coordinate (TangentBundle m)
 
-instance ( CoordDifferential m, f ~ Needle m, m ~ Interior m
+instance ( CoordDifferential m, f ~ Needle m
          , QC.Arbitrary m
          , QC.Arbitrary (CoordinateIdentifier m)
          , QC.Arbitrary (CoordinateIdentifier f) )
diff --git a/manifolds.cabal b/manifolds.cabal
--- a/manifolds.cabal
+++ b/manifolds.cabal
@@ -1,5 +1,5 @@
 Name:                manifolds
-Version:             0.5.1.0
+Version:             0.6.0.0
 Category:            Math
 Synopsis:            Coordinate-free hypersurfaces
 Description:         Manifolds, a generalisation of the notion of &#x201c;smooth curves&#x201d; or surfaces,
@@ -28,7 +28,7 @@
 Homepage:            https://github.com/leftaroundabout/manifolds
 Maintainer:          (@) jsag $ hvl.no
 Build-Type:          Simple
-Cabal-Version:       >=1.18
+Cabal-Version:       1.18
 Extra-Doc-Files:     images/examples/*.png,
                      images/examples/ShadeCombinations/2Dconvolution-skewed.png
                      images/examples/TreesAndWebs/*.png
@@ -40,14 +40,15 @@
 
 Library
   Build-Depends:     base>=4.5 && < 6
-                     , manifolds-core == 0.5.1.0
+                     , manifolds-core == 0.6.0.0
                      , transformers
                      , vector-space>=0.8
                      , free-vector-spaces>=0.1.5
+                     , half-space >=0.1 && <0.2
                      , linear
                      , MemoTrie
                      , vector
-                     , linearmap-category >= 0.3.4 && < 0.5
+                     , linearmap-category >= 0.4.2.0 && < 0.5
                      , spatial-rotations >= 0.1 && < 0.2
                      , containers
                      , array
@@ -59,6 +60,7 @@
                      , number-show >= 0.1 && < 0.2
                      , ieee754 >= 0.8 && < 1
                      , tagged
+                     , equational-reasoning
                      , deepseq
                      , placeholders
                      , lens
@@ -79,6 +81,7 @@
   ghc-options:       -O2
   Exposed-modules:   Data.Manifold
                      Data.Manifold.PseudoAffine
+                     Data.Manifold.WithBoundary
                      Data.Manifold.TreeCover
                      Data.Manifold.Shade
                      Data.Manifold.Web
@@ -100,6 +103,7 @@
                      Math.Manifold.Embedding.Simple.Class
   Other-modules:   Data.List.FastNub
                    Data.Manifold.Types.Primitive
+                   Data.Manifold.WithBoundary.Class
                    Data.SetLike.Intersection
                    Data.Manifold.Cone
                    Data.Embedding
diff --git a/test/tasty/test.hs b/test/tasty/test.hs
--- a/test/tasty/test.hs
+++ b/test/tasty/test.hs
@@ -74,82 +74,83 @@
    , QC.testProperty "2-sphere" (originCancellation @S²)
    , testGroup "2-sphere corner cases"
     [ QC.testProperty "To north pole"
-        $ \(S¹Polar φ) p -> originCancellation (S²Polar 0 φ) p
+        $ \(S¹Polar φ) p -> originCancellation @S² (S²Polar 0 φ) p
     , QC.testProperty "From north pole"
-        $ \(S¹Polar φ) p -> originCancellation p (S²Polar 0 φ)
+        $ \(S¹Polar φ) p -> originCancellation @S² p (S²Polar 0 φ)
     , QC.testProperty "To south pole"
-        $ \(S¹Polar φ) p -> originCancellation (S²Polar pi φ) p
+        $ \(S¹Polar φ) p -> originCancellation @S² (S²Polar pi φ) p
     , QC.testProperty "From south pole"
-        $ \(S¹Polar φ) p -> originCancellation p (S²Polar pi φ)
+        $ \(S¹Polar φ) p -> originCancellation @S² p (S²Polar pi φ)
     , QC.testProperty "South- to north pole"
-        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation (S²Polar 0 φ) (S²Polar pi ψ)
+        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation @S² (S²Polar 0 φ) (S²Polar pi ψ)
     , QC.testProperty "North- to south pole"
-        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation (S²Polar pi ψ) (S²Polar 0 φ)
+        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation @S² (S²Polar pi ψ) (S²Polar 0 φ)
     , QC.testProperty "Along equator"
-        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation (S²Polar (pi/2) ψ) (S²Polar (pi/2) φ)
+        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation @S² (S²Polar (pi/2) ψ) (S²Polar (pi/2) φ)
     , QC.testProperty "Just south of equator"
-        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation (S²Polar (pi/2 + 1e-10) ψ) (S²Polar (pi/2 + 1e-10) φ)
+        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation @S² (S²Polar (pi/2 + 1e-10) ψ) (S²Polar (pi/2 + 1e-10) φ)
     , QC.testProperty "Just across the equator"
-        $ \(S¹Polar φ) (S¹Polar ψ) -> originCancellation (S²Polar (pi/2) ψ) (S²Polar (pi/2 + 1e-10) φ)
+        $ \(S¹Polar φ) (S¹Polar ψ)
+              -> originCancellation @S² (S²Polar (pi/2) ψ) (S²Polar (pi/2 + 1e-10) φ)
     , QC.testProperty "To equator"
-        $ \(S¹Polar φ) p -> originCancellation (S²Polar (pi/2) φ) p
+        $ \(S¹Polar φ) p -> originCancellation @S² (S²Polar (pi/2) φ) p
     , QC.testProperty "From equator"
-        $ \(S¹Polar φ) p -> originCancellation p (S²Polar (pi/2) φ)
+        $ \(S¹Polar φ) p -> originCancellation @S² p (S²Polar (pi/2) φ)
     ]
    , QC.testProperty "Projective plane" (originCancellation @ℝP²)
    ]
   ]
  , testGroup "Natural embeddings"
   [ testGroup "1-sphere"
-     [ testCase "North pole" $ embed (S¹Polar $ pi/2) @?≈ (V2 0 1 :: ℝ²)
-     , testCase "South pole" $ embed (S¹Polar $ -pi/2) @?≈ (V2 0 (-1) :: ℝ²)
+     [ testCase "North pole" $ embed @S¹ (S¹Polar $ pi/2) @?≈ (V2 0 1 :: ℝ²)
+     , testCase "South pole" $ embed @S¹ (S¹Polar $ -pi/2) @?≈ (V2 0 (-1) :: ℝ²)
      ]
   , testGroup "2-sphere"
-     [ testCase "North pole" $ embed (S²Polar 0 0) @?≈ (V3 0 0 1 :: ℝ³)
-     , testCase "South pole" $ embed (S²Polar pi 0) @?≈ (V3 0 0 (-1) :: ℝ³)
+     [ testCase "North pole" $ embed @S² (S²Polar 0 0) @?≈ (V3 0 0 1 :: ℝ³)
+     , testCase "South pole" $ embed @S² (S²Polar pi 0) @?≈ (V3 0 0 (-1) :: ℝ³)
      ]
   , testGroup "1-sphere tangent bundle"
      [ testCase "North pole"
-           $ embed (TangentBundle (S¹Polar $  pi/2) 1)
-               @?≈ (FibreBundle (V2 0 1) (V2 (-1) 0) :: TangentBundle ℝ²)
+           $ embed (TangentBundle @S¹ (S¹Polar $  pi/2) 1)
+               @?≈ (FibreBundle @ℝ² (V2 0 1) (V2 (-1) 0))
      , testCase "South pole"
-           $ embed (TangentBundle (S¹Polar $ -pi/2) 1)
-               @?≈ (FibreBundle (V2 0 (-1)) (V2 1 0) :: TangentBundle ℝ²)
+           $ embed (TangentBundle @S¹ (S¹Polar $ -pi/2) 1)
+               @?≈ (FibreBundle @ℝ² (V2 0 (-1)) (V2 1 0))
      , testCase "45°"
-           $ embed (TangentBundle (S¹Polar $ pi/4) 1)
-               @?≈ (FibreBundle (V2 1 1^/sqrt 2) (V2 (-1) 1^/sqrt 2) :: TangentBundle ℝ²)
+           $ embed (TangentBundle @S¹ (S¹Polar $ pi/4) 1)
+               @?≈ (FibreBundle @ℝ² (V2 1 1^/sqrt 2) (V2 (-1) 1^/sqrt 2))
      ]
   , testGroup "2-sphere tangent bundle"
      [ testCase "North pole, x-dir"
-           $ embed (TangentBundle (S²Polar 0 0) (V2 1 0))
-               @?≈ (FibreBundle (V3 0 0 1) (V3 1 0 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar 0 0) (V2 1 0))
+               @?≈ (FibreBundle @ℝ³ (V3 0 0 1) (V3 1 0 0))
      , testCase "North pole (alternative φ), x-dir"
-           $ embed (TangentBundle (S²Polar 0 1.524) (V2 1 0))
-               @?≈ (FibreBundle (V3 0 0 1) (V3 1 0 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar 0 1.524) (V2 1 0))
+               @?≈ (FibreBundle @ℝ³ (V3 0 0 1) (V3 1 0 0))
      , testCase "North pole, y-dir"
-           $ embed (TangentBundle (S²Polar 0 0) (V2 0 1))
-               @?≈ (FibreBundle (V3 0 0 1) (V3 0 1 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar 0 0) (V2 0 1))
+               @?≈ (FibreBundle @ℝ³ (V3 0 0 1) (V3 0 1 0))
      , testCase "Close to north pole"
-           $ embed (TangentBundle (S²Polar 1e-11 0.602) (V2 3.7 1.1))
-               @?≈ (FibreBundle (V3 0 0 1) (V3 3.7 1.1 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar 1e-11 0.602) (V2 3.7 1.1))
+               @?≈ (FibreBundle @ℝ³ (V3 0 0 1) (V3 3.7 1.1 0))
      , testCase "South pole, x-dir"
-           $ embed (TangentBundle (S²Polar pi 0) (V2 1 0))
-               @?≈ (FibreBundle (V3 0 0 (-1)) (V3 (-1) 0 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar pi 0) (V2 1 0))
+               @?≈ (FibreBundle @ℝ³ (V3 0 0 (-1)) (V3 (-1) 0 0))
      , testCase "South pole, y-dir"
-           $ embed (TangentBundle (S²Polar pi 0) (V2 0 1))
-               @?≈ (FibreBundle (V3 0 0 (-1)) (V3 0 1 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar pi 0) (V2 0 1))
+               @?≈ (FibreBundle @ℝ³ (V3 0 0 (-1)) (V3 0 1 0))
      , testCase "Close to south pole"
-           $ embed (TangentBundle (S²Polar (pi-1e-11) 0.602) (V2 3.7 1.1))
-               @?≈ (FibreBundle (V3 0 0 (-1)) (V3 (-3.7) 1.1 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar (pi-1e-11) 0.602) (V2 3.7 1.1))
+               @?≈ (FibreBundle @ℝ³ (V3 0 0 (-1)) (V3 (-3.7) 1.1 0))
      , testCase "Equator, y-dir"
-           $ embed (TangentBundle (S²Polar (pi/2) 0) (V2 0 1))
-               @?≈ (FibreBundle (V3 1 0 0) (V3 0 1 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar (pi/2) 0) (V2 0 1))
+               @?≈ (FibreBundle @ℝ³ (V3 1 0 0) (V3 0 1 0))
      , testCase "Equator, x-dir"
-           $ embed (TangentBundle (S²Polar (pi/2) (pi/2)) (V2 1 0))
-               @?≈ (FibreBundle (V3 0 1 0) (V3 (-1) 0 0) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar (pi/2) (pi/2)) (V2 1 0))
+               @?≈ (FibreBundle @ℝ³ (V3 0 1 0) (V3 (-1) 0 0))
      , testCase "Equator, z-dir"
-           $ embed (TangentBundle (S²Polar (pi/2) 0) (V2 1 0))
-               @?≈ (FibreBundle (V3 1 0 0) (V3 0 0 (-1)) :: TangentBundle ℝ³)
+           $ embed (TangentBundle @S² (S²Polar (pi/2) 0) (V2 1 0))
+               @?≈ (FibreBundle @ℝ³ (V3 1 0 0) (V3 0 0 (-1)))
      ]
   ]
  , testGroup "Embedding tangent bundles"
@@ -187,11 +188,11 @@
   ]
  , testGroup "Rotation"
   [ testCase "Pole to eqt / prime meridian"
-           $ let rotated = 90° yAxis $ V2 1 0 :@. S²Polar 0 0
+           $ let rotated = 90° yAxis $ V2 1 0 :@. (S²Polar 0 0 :: S²)
              in V2 (rotated ^. delta zenithAngle) (rotated ^. delta azimuth)
                     @?≈ V2 1 0
   , testCase "Pole to eqt / 90°E"
-           $ let rotated = 90° xAxis $ V2 1 0 :@. S²Polar 0 0
+           $ let rotated = 90° xAxis $ V2 1 0 :@. (S²Polar 0 0 :: S²)
              in V2 (rotated ^. delta zenithAngle) (rotated ^. delta azimuth)
                     @?≈ V2 0 1
   , QC.testProperty "Undo – arbitrary axis / angle and points in 𝑇S²."
@@ -263,16 +264,16 @@
                -> (zenithAngle .~ θ₁) (S²Polar θ₀ φ) ≈ S²Polar θ₁ φ
     , testGroup "Tangent space examples"
      [ testCase "Zenith-angle at equator | prime meridian"
-         $ (TangentBundle (S²Polar (pi/2-1e-6) 0) (V2 1 0))
+         $ (TangentBundle @S² (S²Polar (pi/2-1e-6) 0) (V2 1 0))
               ^. delta zenithAngle @?≈ 1
      , testCase "Azimuth at just north of equator | prime meridian"
-         $ (TangentBundle (S²Polar (pi/2-1e-6) 0) (V2 0 1))
+         $ (TangentBundle @S² (S²Polar (pi/2-1e-6) 0) (V2 0 1))
               ^. delta azimuth @?≈ 1
      , testCase "Azimuth at just north of equator | 90°E"
-         $ (TangentBundle (S²Polar (pi/2-1e-6) (pi/2)) (V2 1 0))
+         $ (TangentBundle @S² (S²Polar (pi/2-1e-6) (pi/2)) (V2 1 0))
               ^. delta azimuth @?≈ -1
      , testCase "Azimuth at 45°N | prime meridian"
-         $ (TangentBundle (S²Polar (pi/4) 0) (V2 0 1))
+         $ (TangentBundle @S² (S²Polar (pi/4) 0) (V2 0 1))
               ^. delta azimuth @?≈ sqrt 2
      ]
     ]
@@ -331,29 +332,29 @@
             (S²Polar (pi/4) (-pi/2)) (S²Polar (3*pi/4) (-pi/2)) [V3 1 0 0, V3 0   1  1]
                                                                 [V3 1 0 0, V3 0 (-1) 1]
    , QC.testProperty "Movement on the equator" . QC.expectFailure
-        $ \(S¹Polar φ₀) (S¹Polar φ₁) -> assertParTransportNeedleTargetFixpoint
+        $ \(S¹Polar φ₀) (S¹Polar φ₁) -> assertParTransportNeedleTargetFixpoint @S²
                  (S²Polar 0 0, Just "north pole")
                  (S²Polar (pi/2) φ₀)
                  (S²Polar (pi/2) φ₁)
    , QC.testProperty "Just north of the equator"
         $ \p@(S¹Polar φ₀) q@(S¹Polar φ₁) -> abs (p.-~!q) < 2
-            ==> assertParTransportNeedleTargetFixpoint
+            ==> assertParTransportNeedleTargetFixpoint @S²
                  (S²Polar 0 0, Just "north pole")
                  (S²Polar (pi/2-1e-13) φ₀)
                  (S²Polar (pi/2-1e-13) φ₁)
    , QC.testProperty "Just slightly crossing the equator"
-        $ \(S¹Polar φ₀) (S¹Polar φ₁) -> assertParTransportNeedleTargetFixpoint
+        $ \(S¹Polar φ₀) (S¹Polar φ₁) -> assertParTransportNeedleTargetFixpoint @S²
                  (S²Polar 0 0, Just "north pole")
                  (S²Polar (pi/2-1e-13) φ₀)
                  (S²Polar (pi/2+1e-13) φ₁)
    , QC.testProperty "Just south of the equator"
         $ \p@(S¹Polar φ₀) q@(S¹Polar φ₁) -> abs (p.-~!q) < 2
-            ==> assertParTransportNeedleTargetFixpoint
+            ==> assertParTransportNeedleTargetFixpoint @S²
                  (S²Polar pi 0, Just "south pole")
                  (S²Polar (pi/2+1e-13) φ₀)
                  (S²Polar (pi/2+1e-13) φ₁)
    , QC.testProperty "Movement on the zero meridian"
-        $ \(S¹Polar θ₀) (S¹Polar θ₁) -> assertParTransportNeedleTargetFixpoint
+        $ \(S¹Polar θ₀) (S¹Polar θ₁) -> assertParTransportNeedleTargetFixpoint @S²
                  (S²Polar (pi/2) (pi/2), Nothing)
                  (S²Polar (abs θ₀) (if θ₀>0 then 0 else pi))
                  (S²Polar (abs θ₁) (if θ₁>0 then 0 else pi))
@@ -821,7 +822,7 @@
 instance AEq Double where
   fuzzyEq η x y  = x + abs x*η >= y
           && x - abs x*η <= y
-instance (SimpleSpace v, Needle v~v, Interior v~v, Floating (Scalar v))
+instance (SimpleSpace v, Needle v~v, Floating (Scalar v))
              => AEq (Shade' v) where
   fuzzyEq η (Shade' c₀ σ₀) (Shade' c₁ σ₁)
     = (σ₀|$|δ) < ε && (σ₀|$|δ) < ε
@@ -830,7 +831,7 @@
    where δ = c₁ ^-^ c₀
          ε = 1e-2 + realToFrac η
          is1 x = abs (x-1) < ε
-instance ( SimpleSpace v, DualVector (Needle' v) ~ v, Interior v ~ v
+instance ( SimpleSpace v, DualVector (Needle' v) ~ v
          , InnerSpace (Scalar v), Scalar (Needle' v) ~ Scalar v )
               => AEq (Shade v) where
   fuzzyEq η (Shade c₀ σ₀) (Shade c₁ σ₁)
@@ -912,17 +913,16 @@
                          <*> ((/12)<$>QC.shrink (y*12))
                          <*> ((/12)<$>QC.shrink (z*12))
 
-nearlyAssociative :: ∀ m . ( AEq m, Semimanifold m, Interior m ~ m
+nearlyAssociative :: ∀ m . ( AEq m, Semimanifold m
                            , InnerSpace (Needle m), RealFloat (Scalar (Needle m)) )
                          => m -> Needle m -> Needle m -> QC.Property
 nearlyAssociative p v w = maximum (map magnitude [v,w]) < 1e6
          ==> (p .+~^ v) .+~^ w ≈ (p .+~^ (v^+^w) :: m)
 
-originCancellation :: ∀ m . (AEq m, Manifold m, Show m, Show (Needle m))
+originCancellation :: ∀ m . (AEq m, PseudoAffine m, Show m, Show (Needle m))
                          => m -> m -> QC.Property
-originCancellation p q = case ( boundarylessWitness :: BoundarylessWitness m
-                              , p.-~.q ) of
-      (BoundarylessWitness, Just v)
+originCancellation p q = case p.-~.q of
+      Just v
           -> let p' = q.+~^v
              in QC.counterexample ("v = "++show v++", q+v = "++show p') $ p' ≈ p
 
@@ -935,7 +935,6 @@
        p' = coEmbed ep
 
 embeddingTangentiality :: ∀ m n . ( Semimanifold m, Semimanifold n
-                                  , Interior m ~ m, Interior n ~ n
                                   , NaturallyEmbedded n m
                                   , NaturallyEmbedded (TangentBundle n) (TangentBundle m)
                                   , SP.Show n, AEq n
@@ -953,13 +952,12 @@
 
 nearbyTangentSpaceEmbedding :: ∀ m n
                      . ( Semimanifold m, Semimanifold n
-                       , m ~ Interior m, n ~ Interior n
                        , NaturallyEmbedded n m
                        , NaturallyEmbedded (TangentBundle n) (TangentBundle m)
                        , ParallelTransporting (->) n (Needle n)
                        , SP.Show n, SP.Show (Needle n), AEq (Needle n)
                        , InnerSpace (Needle n), RealFloat (Scalar (Needle n)) )
-       => Scalar (Needle n) -> Interior n -> Needle n -> Needle n -> QC.Property
+       => Scalar (Needle n) -> n -> Needle n -> Needle n -> QC.Property
 nearbyTangentSpaceEmbedding consistRadius p vub f
          = QC.counterexample ("𝑓 embd. at 𝑝, then proj. at 𝑝+𝑣 = "++SP.show fReProj
                               ++", 𝑓 moved by 𝑣 = "++SP.show g)
@@ -1057,7 +1055,7 @@
 
 
 coordinateFiniteDifference :: ∀ m .
-       ( Semimanifold m, HasCoordinates m, m ~ Interior m
+       ( Semimanifold m, HasCoordinates m
        , HasCoordinates (Needle m), CoordDifferential m
        , AEq (Needle m), InnerSpace (Needle m), Scalar (Needle m) ~ ℝ
        , SP.Show m )