-- |
-- Module      : Data.Manifold.PseudoAffine
-- Copyright   : (c) Justus Sagemüller 2015
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 
-- This is the second prototype of a manifold class. It appears to give considerable
-- advantages over 'Data.Manifold.Manifold', so that class will probably soon be replaced
-- with the one we define here (though 'PseudoAffine' does not follow the standard notion
-- of a manifold very closely, it should work quite equivalently for pretty much all
-- Haskell types that qualify as manifolds).
-- 
-- Manifolds are interesting as objects of various categories, from continuous to
-- diffeomorphic. At the moment, we mainly focus on /region-wise differentiable functions/,
-- which are a promising compromise between flexibility of definition and provability of
-- analytic properties. In particular, they are well-suited for visualisation purposes.
-- 
-- The classes in this module are mostly aimed at manifolds /without boundary/.
-- Manifolds with boundary (which we call @MWBound@, never /manifold/!)
-- are more or less treated as a disjoint sum of the interior and the boundary.
-- To understand how this module works, best first forget about boundaries – in this case,
-- @'Interior' x ~ x@, 'fromInterior' and 'toInterior' are trivial, and
-- '.+~|', '|-~.' and 'betweenBounds' are irrelevant.
-- The manifold structure of the boundary itself is not considered at all here.

{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE FunctionalDependencies   #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE LiberalTypeSynonyms      #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE TupleSections            #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DefaultSignatures        #-}
{-# LANGUAGE PatternGuards            #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UnicodeSyntax            #-}
{-# LANGUAGE MultiWayIf               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE RecordWildCards          #-}
{-# LANGUAGE CPP                      #-}


module Data.Manifold.PseudoAffine (
            -- * Manifold class
              Manifold
            , Semimanifold(..), Needle'
            , PseudoAffine(..)
            , LinearManifold, ScalarManifold
            , Num'', RealFrac'', RealFloat''
            -- * Type definitions
            -- ** Needles
            , Local(..)
#if !MIN_VERSION_manifolds_core(0,6,0)
            , (!+~^)
#endif
            -- ** Metrics
            , Metric, Metric'
            , RieMetric, RieMetric'
            -- ** Constraints
            , SemimanifoldWitness(..)
            , PseudoAffineWitness(..)
            , DualNeedleWitness 
            , WithField
            , LocallyScalable
            -- ** Local functions
            , LocalLinear, LocalBilinear, LocalAffine
            -- * Misc
            , alerpB, palerp, palerpB, LocallyCoercible(..), CanonicalDiffeomorphism(..)
            , ImpliesMetric(..), coerceMetric, coerceMetric'
            , Connected (..)
            ) where
    

import Math.Manifold.Core.PseudoAffine
import Data.Manifold.WithBoundary.Class

import Data.Maybe
import Data.Fixed

import Data.VectorSpace
import Linear.V0
import Linear.V1
import Linear.V2
import Linear.V3
import Linear.V4
import qualified Linear.Affine as LinAff
import Data.Embedding
import Data.LinearMap
import Data.VectorSpace.Free
import Math.LinearMap.Category
import Data.AffineSpace
import Data.Tagged
import Data.Manifold.Types.Primitive

import qualified Prelude as Hask
import qualified Control.Applicative as Hask

import Control.Category.Constrained.Prelude hiding ((^))
import Control.Arrow.Constrained
import Control.Monad.Constrained
import Data.Foldable.Constrained

import Control.Lens (Lens', lens, (^.), (&), (%~), (.~))

import Data.CallStack (HasCallStack)
import GHC.Exts (Constraint)


  
  

-- | See 'Semimanifold' and 'PseudoAffine' for the methods.
--   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



-- | Instances of this class must be diffeomorphic manifolds, and even have
--   /canonically isomorphic/ tangent spaces, so that
--   @'fromPackedVector' . 'asPackedVector' :: 'Needle' x -> 'Needle' ξ@
--   defines a meaningful “representational identity“ between these spaces.
class ( Semimanifold x, Semimanifold ξ, LSpace (Needle x), LSpace (Needle ξ)
      , Scalar (Needle x) ~ Scalar (Needle ξ) )
         => LocallyCoercible x ξ where
  -- | Must be compatible with the isomorphism on the tangent spaces, i.e.
  -- @
  -- locallyTrivialDiffeomorphism (p .+~^ v)
  --   ≡ locallyTrivialDiffeomorphism p .+~^ 'coerceNeedle' v
  -- @
  locallyTrivialDiffeomorphism :: x -> ξ
  coerceNeedle :: Hask.Functor p => p (x,ξ) -> (Needle x -+> Needle ξ)
  coerceNeedle' :: Hask.Functor p => p (x,ξ) -> (Needle' x -+> Needle' ξ)
  coerceNorm :: Hask.Functor p => p (x,ξ) -> Metric x -> Metric ξ
  coerceNorm p (x, ξ)
p = case ( CanonicalDiffeomorphism ξ x
forall x ξ. LocallyCoercible x ξ => CanonicalDiffeomorphism ξ x
oppositeLocalCoercion :: CanonicalDiffeomorphism ξ x
                      , DualSpaceWitness (Needle x)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualSpaceWitness (Needle x)
                      , DualSpaceWitness (Needle ξ)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualSpaceWitness (Needle ξ) ) of
    (CanonicalDiffeomorphism ξ x
CanonicalDiffeomorphism, DualSpaceWitness (Needle x)
DualSpaceWitness, DualSpaceWitness (Needle ξ)
DualSpaceWitness)
          -> case ( p (ξ, x) -> Needle ξ -+> Needle x
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> Needle x -+> Needle ξ
coerceNeedle ((x, ξ) -> (ξ, x)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap((x, ξ) -> (ξ, x)) -> p (x, ξ) -> p (ξ, x)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$>p (x, ξ)
p), p (x, ξ) -> DualVector (Needle x) -+> DualVector (Needle ξ)
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> DualVector (Needle x) -+> DualVector (Needle ξ)
coerceNeedle' p (x, ξ)
p ) of
              (LinearFunction (Scalar (Needle ξ)) (Needle ξ) (Needle x)
f, LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle x)) (DualVector (Needle ξ))
f') -> \(Norm Needle x -+> DualVector (Needle x)
n) -> LinearFunction
  (Scalar (Needle ξ)) (Needle ξ) (DualVector (Needle ξ))
-> Metric ξ
forall v. (v -+> DualVector v) -> Norm v
Norm (LinearFunction
   (Scalar (Needle ξ)) (Needle ξ) (DualVector (Needle ξ))
 -> Metric ξ)
-> LinearFunction
     (Scalar (Needle ξ)) (Needle ξ) (DualVector (Needle ξ))
-> Metric ξ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle x)) (DualVector (Needle ξ))
f' LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle x)) (DualVector (Needle ξ))
-> LinearFunction
     (Scalar (Needle ξ)) (Needle ξ) (DualVector (Needle x))
-> LinearFunction
     (Scalar (Needle ξ)) (Needle ξ) (DualVector (Needle ξ))
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. Needle x -+> DualVector (Needle x)
LinearFunction
  (Scalar (Needle ξ)) (Needle x) (DualVector (Needle x))
n LinearFunction
  (Scalar (Needle ξ)) (Needle x) (DualVector (Needle x))
-> LinearFunction (Scalar (Needle ξ)) (Needle ξ) (Needle x)
-> LinearFunction
     (Scalar (Needle ξ)) (Needle ξ) (DualVector (Needle x))
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. LinearFunction (Scalar (Needle ξ)) (Needle ξ) (Needle x)
f
  coerceVariance :: Hask.Functor p => p (x,ξ) -> Metric' x -> Metric' ξ
  coerceVariance p (x, ξ)
p = case ( CanonicalDiffeomorphism ξ x
forall x ξ. LocallyCoercible x ξ => CanonicalDiffeomorphism ξ x
oppositeLocalCoercion :: CanonicalDiffeomorphism ξ x
                          , DualSpaceWitness (Needle x)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualSpaceWitness (Needle x)
                          , DualSpaceWitness (Needle ξ)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualSpaceWitness (Needle ξ) ) of
    (CanonicalDiffeomorphism ξ x
CanonicalDiffeomorphism, DualSpaceWitness (Needle x)
DualSpaceWitness, DualSpaceWitness (Needle ξ)
DualSpaceWitness)
          -> case ( p (x, ξ) -> Needle x -+> Needle ξ
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> Needle x -+> Needle ξ
coerceNeedle p (x, ξ)
p, p (ξ, x) -> DualVector (Needle ξ) -+> DualVector (Needle x)
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> DualVector (Needle x) -+> DualVector (Needle ξ)
coerceNeedle' ((x, ξ) -> (ξ, x)
forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap((x, ξ) -> (ξ, x)) -> p (x, ξ) -> p (ξ, x)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$>p (x, ξ)
p) ) of
              (Needle x -+> Needle ξ
f, LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle ξ)) (DualVector (Needle x))
f') -> \(Norm DualVector (Needle x) -+> DualVector (DualVector (Needle x))
n) -> LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle ξ)) (Needle ξ)
-> Metric' ξ
forall v. (v -+> DualVector v) -> Norm v
Norm (LinearFunction
   (Scalar (Needle ξ)) (DualVector (Needle ξ)) (Needle ξ)
 -> Metric' ξ)
-> LinearFunction
     (Scalar (Needle ξ)) (DualVector (Needle ξ)) (Needle ξ)
-> Metric' ξ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Needle x -+> Needle ξ
f (Needle x -+> Needle ξ)
-> LinearFunction
     (Scalar (Needle ξ)) (DualVector (Needle ξ)) (Needle x)
-> LinearFunction
     (Scalar (Needle ξ)) (DualVector (Needle ξ)) (Needle ξ)
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. DualVector (Needle x) -+> DualVector (DualVector (Needle x))
LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle x)) (Needle x)
n LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle x)) (Needle x)
-> LinearFunction
     (Scalar (Needle ξ)) (DualVector (Needle ξ)) (DualVector (Needle x))
-> LinearFunction
     (Scalar (Needle ξ)) (DualVector (Needle ξ)) (Needle x)
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. LinearFunction
  (Scalar (Needle ξ)) (DualVector (Needle ξ)) (DualVector (Needle x))
f'
  oppositeLocalCoercion :: CanonicalDiffeomorphism ξ x
  default oppositeLocalCoercion :: LocallyCoercible ξ x => CanonicalDiffeomorphism ξ x
  oppositeLocalCoercion = CanonicalDiffeomorphism ξ x
forall a b. LocallyCoercible a b => CanonicalDiffeomorphism a b
CanonicalDiffeomorphism

type NumPrime n = (Num' n, Eq n)

#define identityCoercion(c,t)                   \
instance (c) => LocallyCoercible (t) (t) where { \
  locallyTrivialDiffeomorphism = id;              \
  coerceNeedle _ = id;                             \
  coerceNeedle' _ = id;                             \
  oppositeLocalCoercion = CanonicalDiffeomorphism }
identityCoercion(NumPrime s, ZeroDim s)
identityCoercion(NumPrime s, V0 s)
identityCoercion((), ℝ)
identityCoercion(NumPrime s, V1 s)
identityCoercion((), (ℝ,ℝ))
identityCoercion(NumPrime s, V2 s)
identityCoercion((), (ℝ,(ℝ,ℝ)))
identityCoercion((), ((ℝ,ℝ),ℝ))
identityCoercion(NumPrime s, V3 s)
identityCoercion(NumPrime s, V4 s)


data CanonicalDiffeomorphism a b where
  CanonicalDiffeomorphism :: LocallyCoercible a b => CanonicalDiffeomorphism a b

-- | A point on a manifold, as seen from a nearby reference point.
newtype Local x = Local { Local x -> Needle x
getLocalOffset :: Needle x }
deriving instance (Show (Needle x)) => Show (Local x)

type LocallyScalable s x = ( PseudoAffine x
                           , LSpace (Needle x)
                           , s ~ Scalar (Needle x)
                           , s ~ Scalar (Needle' x)
                           , Num' s )

type LocalLinear x y = LinearMap (Scalar (Needle x)) (Needle x) (Needle y)
type LocalBilinear x y = LinearMap (Scalar (Needle x))
                                   (SymmetricTensor (Scalar (Needle x)) (Needle x))
                                   (Needle y)



type LocalAffine x y = (Needle y, LocalLinear x y)

-- | Require some constraint on a manifold, and also fix the type of the manifold's
--   underlying field. For example, @WithField &#x211d; 'HilbertManifold' v@ constrains
--   @v@ to be a real (i.e., 'Double'-) Hilbert space.
--   Note that for this to compile, you will in
--   general need the @-XLiberalTypeSynonyms@ extension (except if the constraint
--   is an actual type class (like 'Manifold'): only those can always be partially
--   applied, for @type@ constraints this is by default not allowed).
type WithField s c x = ( c x, s ~ Scalar (Needle x), s ~ Scalar (Needle' x) )


-- | A co-needle can be understood as a “paper stack”, with which you can measure
--   the length that a needle reaches in a given direction by counting the number
--   of holes punched through them.
type Needle' x = DualVector (Needle x)


-- | The word &#x201c;metric&#x201d; is used in the sense as in general relativity.
--   Actually this is just the type of scalar products on the tangent space.
--   The actual metric is the function @x -> x -> Scalar (Needle x)@ defined by
--
-- @
-- \\p q -> m '|$|' (p.-~!q)
-- @
type Metric x = Norm (Needle x)
type Metric' x = Variance (Needle x)

-- | A Riemannian metric assigns each point on a manifold a scalar product on the tangent space.
--   Note that this association is /not/ continuous, because the charts/tangent spaces in the bundle
--   are a priori disjoint. However, for a proper Riemannian metric, all arising expressions
--   of scalar products from needles between points on the manifold ought to be differentiable.
type RieMetric x = x -> Metric x
type RieMetric' x = x -> Metric' x


coerceMetric :: ∀ x ξ . (LocallyCoercible x ξ, LSpace (Needle ξ))
                             => RieMetric ξ -> RieMetric x
coerceMetric :: RieMetric ξ -> RieMetric x
coerceMetric = case ( DualSpaceWitness (Needle x)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualNeedleWitness x
                    , DualSpaceWitness (Needle ξ)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualNeedleWitness ξ ) of
   (DualSpaceWitness (Needle x)
DualSpaceWitness, DualSpaceWitness (Needle ξ)
DualSpaceWitness)
       -> \RieMetric ξ
m x
x -> case RieMetric ξ
m RieMetric ξ -> RieMetric ξ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> ξ
forall x ξ. LocallyCoercible x ξ => x -> ξ
locallyTrivialDiffeomorphism x
x of
              Norm Needle ξ -+> DualVector (Needle ξ)
sc -> LinearFunction
  (Scalar (DualVector (Needle x))) (Needle x) (DualVector (Needle x))
-> Metric x
forall v. (v -+> DualVector v) -> Norm v
Norm (LinearFunction
   (Scalar (DualVector (Needle x))) (Needle x) (DualVector (Needle x))
 -> Metric x)
-> LinearFunction
     (Scalar (DualVector (Needle x))) (Needle x) (DualVector (Needle x))
-> Metric x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearFunction
  (Scalar (DualVector (Needle x)))
  (DualVector (Needle ξ))
  (DualVector (Needle x))
bw LinearFunction
  (Scalar (DualVector (Needle x)))
  (DualVector (Needle ξ))
  (DualVector (Needle x))
-> LinearFunction
     (Scalar (DualVector (Needle x))) (Needle x) (DualVector (Needle ξ))
-> LinearFunction
     (Scalar (DualVector (Needle x))) (Needle x) (DualVector (Needle x))
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. LinearFunction
  (Scalar (DualVector (Needle x))) (Needle ξ) (DualVector (Needle ξ))
Needle ξ -+> DualVector (Needle ξ)
sc LinearFunction
  (Scalar (DualVector (Needle x))) (Needle ξ) (DualVector (Needle ξ))
-> LinearFunction
     (Scalar (DualVector (Needle x))) (Needle x) (Needle ξ)
-> LinearFunction
     (Scalar (DualVector (Needle x))) (Needle x) (DualVector (Needle ξ))
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. LinearFunction
  (Scalar (DualVector (Needle x))) (Needle x) (Needle ξ)
Needle x -+> Needle ξ
fw
 where fw :: Needle x -+> Needle ξ
fw = [(x, ξ)] -> Needle x -+> Needle ξ
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> Needle x -+> Needle ξ
coerceNeedle ([]::[(x,ξ)])
       bw :: LinearFunction
  (Scalar (DualVector (Needle x)))
  (DualVector (Needle ξ))
  (DualVector (Needle x))
bw = case CanonicalDiffeomorphism ξ x
forall x ξ. LocallyCoercible x ξ => CanonicalDiffeomorphism ξ x
oppositeLocalCoercion :: CanonicalDiffeomorphism ξ x of
              CanonicalDiffeomorphism ξ x
CanonicalDiffeomorphism -> [(ξ, x)]
-> LinearFunction
     (Scalar (DualVector (Needle x)))
     (DualVector (Needle ξ))
     (DualVector (Needle x))
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> DualVector (Needle x) -+> DualVector (Needle ξ)
coerceNeedle' ([]::[(ξ,x)])
coerceMetric' :: ∀ x ξ . (LocallyCoercible x ξ, LSpace (Needle ξ))
                             => RieMetric' ξ -> RieMetric' x
coerceMetric' :: RieMetric' ξ -> RieMetric' x
coerceMetric' = case ( DualSpaceWitness (Needle x)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualNeedleWitness x
                     , DualSpaceWitness (Needle ξ)
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualNeedleWitness ξ ) of
   (DualSpaceWitness (Needle x)
DualSpaceWitness, DualSpaceWitness (Needle ξ)
DualSpaceWitness)
       -> \RieMetric' ξ
m x
x -> case RieMetric' ξ
m RieMetric' ξ -> RieMetric' ξ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x -> ξ
forall x ξ. LocallyCoercible x ξ => x -> ξ
locallyTrivialDiffeomorphism x
x of
              Norm DualVector (Needle ξ) -+> DualVector (DualVector (Needle ξ))
sc -> LinearFunction
  (Scalar (Needle x)) (DualVector (Needle x)) (Needle x)
-> Metric' x
forall v. (v -+> DualVector v) -> Norm v
Norm (LinearFunction
   (Scalar (Needle x)) (DualVector (Needle x)) (Needle x)
 -> Metric' x)
-> LinearFunction
     (Scalar (Needle x)) (DualVector (Needle x)) (Needle x)
-> Metric' x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearFunction (Scalar (Needle x)) (Needle ξ) (Needle x)
LinearFunction (Scalar (Needle ξ)) (Needle ξ) (Needle x)
bw LinearFunction (Scalar (Needle x)) (Needle ξ) (Needle x)
-> LinearFunction
     (Scalar (Needle x)) (DualVector (Needle x)) (Needle ξ)
-> LinearFunction
     (Scalar (Needle x)) (DualVector (Needle x)) (Needle x)
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. DualVector (Needle ξ) -+> DualVector (DualVector (Needle ξ))
LinearFunction
  (Scalar (Needle x)) (DualVector (Needle ξ)) (Needle ξ)
sc LinearFunction
  (Scalar (Needle x)) (DualVector (Needle ξ)) (Needle ξ)
-> LinearFunction
     (Scalar (Needle x)) (DualVector (Needle x)) (DualVector (Needle ξ))
-> LinearFunction
     (Scalar (Needle x)) (DualVector (Needle x)) (Needle ξ)
forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. DualVector (Needle x) -+> DualVector (Needle ξ)
LinearFunction
  (Scalar (Needle x)) (DualVector (Needle x)) (DualVector (Needle ξ))
fw
 where fw :: DualVector (Needle x) -+> DualVector (Needle ξ)
fw = [(x, ξ)] -> DualVector (Needle x) -+> DualVector (Needle ξ)
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> DualVector (Needle x) -+> DualVector (Needle ξ)
coerceNeedle' ([]::[(x,ξ)])
       bw :: LinearFunction (Scalar (Needle ξ)) (Needle ξ) (Needle x)
bw = case CanonicalDiffeomorphism ξ x
forall x ξ. LocallyCoercible x ξ => CanonicalDiffeomorphism ξ x
oppositeLocalCoercion :: CanonicalDiffeomorphism ξ x of
              CanonicalDiffeomorphism ξ x
CanonicalDiffeomorphism -> [(ξ, x)]
-> LinearFunction (Scalar (Needle x)) (Needle ξ) (Needle x)
forall x ξ (p :: * -> *).
(LocallyCoercible x ξ, Functor p) =>
p (x, ξ) -> Needle x -+> Needle ξ
coerceNeedle ([]::[(ξ,x)])




hugeℝVal :: ℝ
hugeℝVal :: ℝ
hugeℝVal = ℝ
1e+100

#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 (NumPrime s) => LocallyCoercible (ZeroDim s) (V0 s) where
  locallyTrivialDiffeomorphism :: ZeroDim s -> V0 s
locallyTrivialDiffeomorphism ZeroDim s
Origin = V0 s
forall a. V0 a
V0
  coerceNeedle :: p (ZeroDim s, V0 s) -> Needle (ZeroDim s) -+> Needle (V0 s)
coerceNeedle p (ZeroDim s, V0 s)
_ = (ZeroDim s -> V0 s) -> LinearFunction s (ZeroDim s) (V0 s)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((ZeroDim s -> V0 s) -> LinearFunction s (ZeroDim s) (V0 s))
-> (ZeroDim s -> V0 s) -> LinearFunction s (ZeroDim s) (V0 s)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ZeroDim s
Origin -> V0 s
forall a. V0 a
V0
  coerceNeedle' :: p (ZeroDim s, V0 s) -> Needle' (ZeroDim s) -+> Needle' (V0 s)
coerceNeedle' p (ZeroDim s, V0 s)
_ = (ZeroDim s -> V0 s) -> LinearFunction s (ZeroDim s) (V0 s)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((ZeroDim s -> V0 s) -> LinearFunction s (ZeroDim s) (V0 s))
-> (ZeroDim s -> V0 s) -> LinearFunction s (ZeroDim s) (V0 s)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ZeroDim s
Origin -> V0 s
forall a. V0 a
V0
instance (NumPrime s) => LocallyCoercible (V0 s) (ZeroDim s) where
  locallyTrivialDiffeomorphism :: V0 s -> ZeroDim s
locallyTrivialDiffeomorphism V0 s
V0 = ZeroDim s
forall s. ZeroDim s
Origin
  coerceNeedle :: p (V0 s, ZeroDim s) -> Needle (V0 s) -+> Needle (ZeroDim s)
coerceNeedle p (V0 s, ZeroDim s)
_ = (V0 s -> ZeroDim s) -> LinearFunction s (V0 s) (ZeroDim s)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V0 s -> ZeroDim s) -> LinearFunction s (V0 s) (ZeroDim s))
-> (V0 s -> ZeroDim s) -> LinearFunction s (V0 s) (ZeroDim s)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \V0 s
V0 -> ZeroDim s
forall s. ZeroDim s
Origin
  coerceNeedle' :: p (V0 s, ZeroDim s) -> Needle' (V0 s) -+> Needle' (ZeroDim s)
coerceNeedle' p (V0 s, ZeroDim s)
_ = (V0 s -> ZeroDim s) -> LinearFunction s (V0 s) (ZeroDim s)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V0 s -> ZeroDim s) -> LinearFunction s (V0 s) (ZeroDim s))
-> (V0 s -> ZeroDim s) -> LinearFunction s (V0 s) (ZeroDim s)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \V0 s
V0 -> ZeroDim s
forall s. ZeroDim s
Origin
instance LocallyCoercible ℝ (V1 ℝ) where
  locallyTrivialDiffeomorphism :: ℝ -> V1 ℝ
locallyTrivialDiffeomorphism = ℝ -> V1 ℝ
forall a. a -> V1 a
V1
  coerceNeedle :: p (ℝ, V1 ℝ) -> Needle ℝ -+> Needle (V1 ℝ)
coerceNeedle p (ℝ, V1 ℝ)
_ = (ℝ -> V1 ℝ) -> LinearFunction ℝ ℝ (V1 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ℝ -> V1 ℝ
forall a. a -> V1 a
V1
  coerceNeedle' :: p (ℝ, V1 ℝ) -> Needle' ℝ -+> Needle' (V1 ℝ)
coerceNeedle' p (ℝ, V1 ℝ)
_ = (ℝ -> V1 ℝ) -> LinearFunction ℝ ℝ (V1 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ℝ -> V1 ℝ
forall a. a -> V1 a
V1
instance LocallyCoercible (V1 ℝ) ℝ where
  locallyTrivialDiffeomorphism :: V1 ℝ -> ℝ
locallyTrivialDiffeomorphism (V1 ℝ
n) = ℝ
n
  coerceNeedle :: p (V1 ℝ, ℝ) -> Needle (V1 ℝ) -+> Needle ℝ
coerceNeedle p (V1 ℝ, ℝ)
_ = (V1 ℝ -> ℝ) -> LinearFunction ℝ (V1 ℝ) ℝ
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V1 ℝ -> ℝ) -> LinearFunction ℝ (V1 ℝ) ℝ)
-> (V1 ℝ -> ℝ) -> LinearFunction ℝ (V1 ℝ) ℝ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V1 ℝ
n) -> ℝ
n
  coerceNeedle' :: p (V1 ℝ, ℝ) -> Needle' (V1 ℝ) -+> Needle' ℝ
coerceNeedle' p (V1 ℝ, ℝ)
_ = (V1 ℝ -> ℝ) -> LinearFunction ℝ (V1 ℝ) ℝ
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V1 ℝ -> ℝ) -> LinearFunction ℝ (V1 ℝ) ℝ)
-> (V1 ℝ -> ℝ) -> LinearFunction ℝ (V1 ℝ) ℝ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V1 ℝ
n) -> ℝ
n
instance LocallyCoercible (ℝ,ℝ) (V2 ℝ) where
  locallyTrivialDiffeomorphism :: (ℝ, ℝ) -> V2 ℝ
locallyTrivialDiffeomorphism = (ℝ -> ℝ -> V2 ℝ) -> (ℝ, ℝ) -> V2 ℝ
forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k a (k b c) -> k (a, b) c
uncurry ℝ -> ℝ -> V2 ℝ
forall a. a -> a -> V2 a
V2
  coerceNeedle :: p ((ℝ, ℝ), V2 ℝ) -> Needle (ℝ, ℝ) -+> Needle (V2 ℝ)
coerceNeedle p ((ℝ, ℝ), V2 ℝ)
_ = ((ℝ, ℝ) -> V2 ℝ) -> LinearFunction ℝ (ℝ, ℝ) (V2 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (((ℝ, ℝ) -> V2 ℝ) -> LinearFunction ℝ (ℝ, ℝ) (V2 ℝ))
-> ((ℝ, ℝ) -> V2 ℝ) -> LinearFunction ℝ (ℝ, ℝ) (V2 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (ℝ -> ℝ -> V2 ℝ) -> (ℝ, ℝ) -> V2 ℝ
forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k a (k b c) -> k (a, b) c
uncurry ℝ -> ℝ -> V2 ℝ
forall a. a -> a -> V2 a
V2
  coerceNeedle' :: p ((ℝ, ℝ), V2 ℝ) -> Needle' (ℝ, ℝ) -+> Needle' (V2 ℝ)
coerceNeedle' p ((ℝ, ℝ), V2 ℝ)
_ = ((ℝ, ℝ) -> V2 ℝ) -> LinearFunction ℝ (ℝ, ℝ) (V2 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (((ℝ, ℝ) -> V2 ℝ) -> LinearFunction ℝ (ℝ, ℝ) (V2 ℝ))
-> ((ℝ, ℝ) -> V2 ℝ) -> LinearFunction ℝ (ℝ, ℝ) (V2 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (ℝ -> ℝ -> V2 ℝ) -> (ℝ, ℝ) -> V2 ℝ
forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k a (k b c) -> k (a, b) c
uncurry ℝ -> ℝ -> V2 ℝ
forall a. a -> a -> V2 a
V2
instance LocallyCoercible (V2 ℝ) (ℝ,ℝ) where
  locallyTrivialDiffeomorphism :: V2 ℝ -> (ℝ, ℝ)
locallyTrivialDiffeomorphism (V2 ℝ
x ℝ
y) = (ℝ
x,ℝ
y)
  coerceNeedle :: p (V2 ℝ, (ℝ, ℝ)) -> Needle (V2 ℝ) -+> Needle (ℝ, ℝ)
coerceNeedle p (V2 ℝ, (ℝ, ℝ))
_ = (V2 ℝ -> (ℝ, ℝ)) -> LinearFunction ℝ (V2 ℝ) (ℝ, ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V2 ℝ -> (ℝ, ℝ)) -> LinearFunction ℝ (V2 ℝ) (ℝ, ℝ))
-> (V2 ℝ -> (ℝ, ℝ)) -> LinearFunction ℝ (V2 ℝ) (ℝ, ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V2 ℝ
x ℝ
y) -> (ℝ
x,ℝ
y)
  coerceNeedle' :: p (V2 ℝ, (ℝ, ℝ)) -> Needle' (V2 ℝ) -+> Needle' (ℝ, ℝ)
coerceNeedle' p (V2 ℝ, (ℝ, ℝ))
_ = (V2 ℝ -> (ℝ, ℝ)) -> LinearFunction ℝ (V2 ℝ) (ℝ, ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V2 ℝ -> (ℝ, ℝ)) -> LinearFunction ℝ (V2 ℝ) (ℝ, ℝ))
-> (V2 ℝ -> (ℝ, ℝ)) -> LinearFunction ℝ (V2 ℝ) (ℝ, ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V2 ℝ
x ℝ
y) -> (ℝ
x,ℝ
y)
instance LocallyCoercible ((ℝ,ℝ),ℝ) (V3 ℝ) where
  locallyTrivialDiffeomorphism :: ((ℝ, ℝ), ℝ) -> V3 ℝ
locallyTrivialDiffeomorphism ((ℝ
x,ℝ
y),ℝ
z) = ℝ -> ℝ -> ℝ -> V3 ℝ
forall a. a -> a -> a -> V3 a
V3 ℝ
x ℝ
y ℝ
z
  coerceNeedle :: p (((ℝ, ℝ), ℝ), V3 ℝ) -> Needle ((ℝ, ℝ), ℝ) -+> Needle (V3 ℝ)
coerceNeedle p (((ℝ, ℝ), ℝ), V3 ℝ)
_ = (((ℝ, ℝ), ℝ) -> V3 ℝ) -> LinearFunction ℝ ((ℝ, ℝ), ℝ) (V3 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((((ℝ, ℝ), ℝ) -> V3 ℝ) -> LinearFunction ℝ ((ℝ, ℝ), ℝ) (V3 ℝ))
-> (((ℝ, ℝ), ℝ) -> V3 ℝ) -> LinearFunction ℝ ((ℝ, ℝ), ℝ) (V3 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \((ℝ
x,ℝ
y),ℝ
z) -> ℝ -> ℝ -> ℝ -> V3 ℝ
forall a. a -> a -> a -> V3 a
V3 ℝ
x ℝ
y ℝ
z
  coerceNeedle' :: p (((ℝ, ℝ), ℝ), V3 ℝ) -> Needle' ((ℝ, ℝ), ℝ) -+> Needle' (V3 ℝ)
coerceNeedle' p (((ℝ, ℝ), ℝ), V3 ℝ)
_ = (((ℝ, ℝ), ℝ) -> V3 ℝ) -> LinearFunction ℝ ((ℝ, ℝ), ℝ) (V3 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((((ℝ, ℝ), ℝ) -> V3 ℝ) -> LinearFunction ℝ ((ℝ, ℝ), ℝ) (V3 ℝ))
-> (((ℝ, ℝ), ℝ) -> V3 ℝ) -> LinearFunction ℝ ((ℝ, ℝ), ℝ) (V3 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \((ℝ
x,ℝ
y),ℝ
z) -> ℝ -> ℝ -> ℝ -> V3 ℝ
forall a. a -> a -> a -> V3 a
V3 ℝ
x ℝ
y ℝ
z
instance LocallyCoercible (ℝ,(ℝ,ℝ)) (V3 ℝ) where
  locallyTrivialDiffeomorphism :: (ℝ, (ℝ, ℝ)) -> V3 ℝ
locallyTrivialDiffeomorphism (ℝ
x,(ℝ
y,ℝ
z)) = ℝ -> ℝ -> ℝ -> V3 ℝ
forall a. a -> a -> a -> V3 a
V3 ℝ
x ℝ
y ℝ
z
  coerceNeedle :: p ((ℝ, (ℝ, ℝ)), V3 ℝ) -> Needle (ℝ, (ℝ, ℝ)) -+> Needle (V3 ℝ)
coerceNeedle p ((ℝ, (ℝ, ℝ)), V3 ℝ)
_ = ((ℝ, (ℝ, ℝ)) -> V3 ℝ) -> LinearFunction ℝ (ℝ, (ℝ, ℝ)) (V3 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (((ℝ, (ℝ, ℝ)) -> V3 ℝ) -> LinearFunction ℝ (ℝ, (ℝ, ℝ)) (V3 ℝ))
-> ((ℝ, (ℝ, ℝ)) -> V3 ℝ) -> LinearFunction ℝ (ℝ, (ℝ, ℝ)) (V3 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(ℝ
x,(ℝ
y,ℝ
z)) -> ℝ -> ℝ -> ℝ -> V3 ℝ
forall a. a -> a -> a -> V3 a
V3 ℝ
x ℝ
y ℝ
z
  coerceNeedle' :: p ((ℝ, (ℝ, ℝ)), V3 ℝ) -> Needle' (ℝ, (ℝ, ℝ)) -+> Needle' (V3 ℝ)
coerceNeedle' p ((ℝ, (ℝ, ℝ)), V3 ℝ)
_ = ((ℝ, (ℝ, ℝ)) -> V3 ℝ) -> LinearFunction ℝ (ℝ, (ℝ, ℝ)) (V3 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (((ℝ, (ℝ, ℝ)) -> V3 ℝ) -> LinearFunction ℝ (ℝ, (ℝ, ℝ)) (V3 ℝ))
-> ((ℝ, (ℝ, ℝ)) -> V3 ℝ) -> LinearFunction ℝ (ℝ, (ℝ, ℝ)) (V3 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(ℝ
x,(ℝ
y,ℝ
z)) -> ℝ -> ℝ -> ℝ -> V3 ℝ
forall a. a -> a -> a -> V3 a
V3 ℝ
x ℝ
y ℝ
z
instance LocallyCoercible (V3 ℝ) ((ℝ,ℝ),ℝ) where
  locallyTrivialDiffeomorphism :: V3 ℝ -> ((ℝ, ℝ), ℝ)
locallyTrivialDiffeomorphism (V3 ℝ
x ℝ
y ℝ
z) = ((ℝ
x,ℝ
y),ℝ
z)
  coerceNeedle :: p (V3 ℝ, ((ℝ, ℝ), ℝ)) -> Needle (V3 ℝ) -+> Needle ((ℝ, ℝ), ℝ)
coerceNeedle p (V3 ℝ, ((ℝ, ℝ), ℝ))
_ = (V3 ℝ -> ((ℝ, ℝ), ℝ)) -> LinearFunction ℝ (V3 ℝ) ((ℝ, ℝ), ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V3 ℝ -> ((ℝ, ℝ), ℝ)) -> LinearFunction ℝ (V3 ℝ) ((ℝ, ℝ), ℝ))
-> (V3 ℝ -> ((ℝ, ℝ), ℝ)) -> LinearFunction ℝ (V3 ℝ) ((ℝ, ℝ), ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V3 ℝ
x ℝ
y ℝ
z) -> ((ℝ
x,ℝ
y),ℝ
z)
  coerceNeedle' :: p (V3 ℝ, ((ℝ, ℝ), ℝ)) -> Needle' (V3 ℝ) -+> Needle' ((ℝ, ℝ), ℝ)
coerceNeedle' p (V3 ℝ, ((ℝ, ℝ), ℝ))
_ = (V3 ℝ -> ((ℝ, ℝ), ℝ)) -> LinearFunction ℝ (V3 ℝ) ((ℝ, ℝ), ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V3 ℝ -> ((ℝ, ℝ), ℝ)) -> LinearFunction ℝ (V3 ℝ) ((ℝ, ℝ), ℝ))
-> (V3 ℝ -> ((ℝ, ℝ), ℝ)) -> LinearFunction ℝ (V3 ℝ) ((ℝ, ℝ), ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V3 ℝ
x ℝ
y ℝ
z) -> ((ℝ
x,ℝ
y),ℝ
z)
instance LocallyCoercible (V3 ℝ) (ℝ,(ℝ,ℝ)) where
  locallyTrivialDiffeomorphism :: V3 ℝ -> (ℝ, (ℝ, ℝ))
locallyTrivialDiffeomorphism (V3 ℝ
x ℝ
y ℝ
z) = (ℝ
x,(ℝ
y,ℝ
z))
  coerceNeedle :: p (V3 ℝ, (ℝ, (ℝ, ℝ))) -> Needle (V3 ℝ) -+> Needle (ℝ, (ℝ, ℝ))
coerceNeedle p (V3 ℝ, (ℝ, (ℝ, ℝ)))
_ = (V3 ℝ -> (ℝ, (ℝ, ℝ))) -> LinearFunction ℝ (V3 ℝ) (ℝ, (ℝ, ℝ))
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V3 ℝ -> (ℝ, (ℝ, ℝ))) -> LinearFunction ℝ (V3 ℝ) (ℝ, (ℝ, ℝ)))
-> (V3 ℝ -> (ℝ, (ℝ, ℝ))) -> LinearFunction ℝ (V3 ℝ) (ℝ, (ℝ, ℝ))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V3 ℝ
x ℝ
y ℝ
z) -> (ℝ
x,(ℝ
y,ℝ
z))
  coerceNeedle' :: p (V3 ℝ, (ℝ, (ℝ, ℝ))) -> Needle' (V3 ℝ) -+> Needle' (ℝ, (ℝ, ℝ))
coerceNeedle' p (V3 ℝ, (ℝ, (ℝ, ℝ)))
_ = (V3 ℝ -> (ℝ, (ℝ, ℝ))) -> LinearFunction ℝ (V3 ℝ) (ℝ, (ℝ, ℝ))
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V3 ℝ -> (ℝ, (ℝ, ℝ))) -> LinearFunction ℝ (V3 ℝ) (ℝ, (ℝ, ℝ)))
-> (V3 ℝ -> (ℝ, (ℝ, ℝ))) -> LinearFunction ℝ (V3 ℝ) (ℝ, (ℝ, ℝ))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V3 ℝ
x ℝ
y ℝ
z) -> (ℝ
x,(ℝ
y,ℝ
z))
instance LocallyCoercible ((ℝ,ℝ),(ℝ,ℝ)) (V4 ℝ) where
  locallyTrivialDiffeomorphism :: ((ℝ, ℝ), (ℝ, ℝ)) -> V4 ℝ
locallyTrivialDiffeomorphism ((ℝ
x,ℝ
y),(ℝ
z,ℝ
w)) = ℝ -> ℝ -> ℝ -> ℝ -> V4 ℝ
forall a. a -> a -> a -> a -> V4 a
V4 ℝ
x ℝ
y ℝ
z ℝ
w
  coerceNeedle :: p (((ℝ, ℝ), (ℝ, ℝ)), V4 ℝ)
-> Needle ((ℝ, ℝ), (ℝ, ℝ)) -+> Needle (V4 ℝ)
coerceNeedle p (((ℝ, ℝ), (ℝ, ℝ)), V4 ℝ)
_ = (((ℝ, ℝ), (ℝ, ℝ)) -> V4 ℝ)
-> LinearFunction ℝ ((ℝ, ℝ), (ℝ, ℝ)) (V4 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((((ℝ, ℝ), (ℝ, ℝ)) -> V4 ℝ)
 -> LinearFunction ℝ ((ℝ, ℝ), (ℝ, ℝ)) (V4 ℝ))
-> (((ℝ, ℝ), (ℝ, ℝ)) -> V4 ℝ)
-> LinearFunction ℝ ((ℝ, ℝ), (ℝ, ℝ)) (V4 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \((ℝ
x,ℝ
y),(ℝ
z,ℝ
w)) -> ℝ -> ℝ -> ℝ -> ℝ -> V4 ℝ
forall a. a -> a -> a -> a -> V4 a
V4 ℝ
x ℝ
y ℝ
z ℝ
w
  coerceNeedle' :: p (((ℝ, ℝ), (ℝ, ℝ)), V4 ℝ)
-> Needle' ((ℝ, ℝ), (ℝ, ℝ)) -+> Needle' (V4 ℝ)
coerceNeedle' p (((ℝ, ℝ), (ℝ, ℝ)), V4 ℝ)
_ = (((ℝ, ℝ), (ℝ, ℝ)) -> V4 ℝ)
-> LinearFunction ℝ ((ℝ, ℝ), (ℝ, ℝ)) (V4 ℝ)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((((ℝ, ℝ), (ℝ, ℝ)) -> V4 ℝ)
 -> LinearFunction ℝ ((ℝ, ℝ), (ℝ, ℝ)) (V4 ℝ))
-> (((ℝ, ℝ), (ℝ, ℝ)) -> V4 ℝ)
-> LinearFunction ℝ ((ℝ, ℝ), (ℝ, ℝ)) (V4 ℝ)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \((ℝ
x,ℝ
y),(ℝ
z,ℝ
w)) -> ℝ -> ℝ -> ℝ -> ℝ -> V4 ℝ
forall a. a -> a -> a -> a -> V4 a
V4 ℝ
x ℝ
y ℝ
z ℝ
w
instance LocallyCoercible (V4 ℝ) ((ℝ,ℝ),(ℝ,ℝ)) where
  locallyTrivialDiffeomorphism :: V4 ℝ -> ((ℝ, ℝ), (ℝ, ℝ))
locallyTrivialDiffeomorphism (V4 ℝ
x ℝ
y ℝ
z ℝ
w) = ((ℝ
x,ℝ
y),(ℝ
z,ℝ
w))
  coerceNeedle :: p (V4 ℝ, ((ℝ, ℝ), (ℝ, ℝ)))
-> Needle (V4 ℝ) -+> Needle ((ℝ, ℝ), (ℝ, ℝ))
coerceNeedle p (V4 ℝ, ((ℝ, ℝ), (ℝ, ℝ)))
_ = (V4 ℝ -> ((ℝ, ℝ), (ℝ, ℝ)))
-> LinearFunction ℝ (V4 ℝ) ((ℝ, ℝ), (ℝ, ℝ))
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V4 ℝ -> ((ℝ, ℝ), (ℝ, ℝ)))
 -> LinearFunction ℝ (V4 ℝ) ((ℝ, ℝ), (ℝ, ℝ)))
-> (V4 ℝ -> ((ℝ, ℝ), (ℝ, ℝ)))
-> LinearFunction ℝ (V4 ℝ) ((ℝ, ℝ), (ℝ, ℝ))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V4 ℝ
x ℝ
y ℝ
z ℝ
w) -> ((ℝ
x,ℝ
y),(ℝ
z,ℝ
w))
  coerceNeedle' :: p (V4 ℝ, ((ℝ, ℝ), (ℝ, ℝ)))
-> Needle' (V4 ℝ) -+> Needle' ((ℝ, ℝ), (ℝ, ℝ))
coerceNeedle' p (V4 ℝ, ((ℝ, ℝ), (ℝ, ℝ)))
_ = (V4 ℝ -> ((ℝ, ℝ), (ℝ, ℝ)))
-> LinearFunction ℝ (V4 ℝ) ((ℝ, ℝ), (ℝ, ℝ))
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((V4 ℝ -> ((ℝ, ℝ), (ℝ, ℝ)))
 -> LinearFunction ℝ (V4 ℝ) ((ℝ, ℝ), (ℝ, ℝ)))
-> (V4 ℝ -> ((ℝ, ℝ), (ℝ, ℝ)))
-> LinearFunction ℝ (V4 ℝ) ((ℝ, ℝ), (ℝ, ℝ))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(V4 ℝ
x ℝ
y ℝ
z ℝ
w) -> ((ℝ
x,ℝ
y),(ℝ
z,ℝ
w))


instance ( Semimanifold a, Semimanifold b, Semimanifold c
         , LSpace (Needle a), LSpace (Needle b), LSpace (Needle c)
         , Scalar (Needle a) ~ Scalar (Needle b), Scalar (Needle b) ~ Scalar (Needle c)
         , Scalar (Needle' a) ~ Scalar (Needle a), Scalar (Needle' b) ~ Scalar (Needle b)
         , Scalar (Needle' c) ~ Scalar (Needle c) )
     => LocallyCoercible (a,(b,c)) ((a,b),c) where
  locallyTrivialDiffeomorphism :: (a, (b, c)) -> ((a, b), c)
locallyTrivialDiffeomorphism = (a, (b, c)) -> ((a, b), c)
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup
  coerceNeedle :: p ((a, (b, c)), ((a, b), c))
-> Needle (a, (b, c)) -+> Needle ((a, b), c)
coerceNeedle p ((a, (b, c)), ((a, b), c))
_ = Needle (a, (b, c)) -+> Needle ((a, b), c)
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup
  coerceNeedle' :: p ((a, (b, c)), ((a, b), c))
-> Needle' (a, (b, c)) -+> Needle' ((a, b), c)
coerceNeedle' p ((a, (b, c)), ((a, b), c))
_ = Needle' (a, (b, c)) -+> Needle' ((a, b), c)
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k (a, (b, c)) ((a, b), c)
regroup
  oppositeLocalCoercion :: CanonicalDiffeomorphism ((a, b), c) (a, (b, c))
oppositeLocalCoercion = CanonicalDiffeomorphism ((a, b), c) (a, (b, c))
forall a b. LocallyCoercible a b => CanonicalDiffeomorphism a b
CanonicalDiffeomorphism
instance ∀ a b c .
         ( Semimanifold a, Semimanifold b, Semimanifold c
         , LSpace (Needle a), LSpace (Needle b), LSpace (Needle c)
         , Scalar (Needle a) ~ Scalar (Needle b), Scalar (Needle b) ~ Scalar (Needle c)
         , Scalar (Needle' a) ~ Scalar (Needle a), Scalar (Needle' b) ~ Scalar (Needle b)
         , Scalar (Needle' c) ~ Scalar (Needle c)  )
     => LocallyCoercible ((a,b),c) (a,(b,c)) where
  locallyTrivialDiffeomorphism :: ((a, b), c) -> (a, (b, c))
locallyTrivialDiffeomorphism = ((a, b), c) -> (a, (b, c))
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup'
  coerceNeedle :: p (((a, b), c), (a, (b, c)))
-> Needle ((a, b), c) -+> Needle (a, (b, c))
coerceNeedle p (((a, b), c), (a, (b, c)))
_ = Needle ((a, b), c) -+> Needle (a, (b, c))
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup'
  coerceNeedle' :: p (((a, b), c), (a, (b, c)))
-> Needle' ((a, b), c) -+> Needle' (a, (b, c))
coerceNeedle' p (((a, b), c), (a, (b, c)))
_ = Needle' ((a, b), c) -+> Needle' (a, (b, c))
forall (k :: * -> * -> *) a b c.
(Cartesian k, ObjectPair k a b, ObjectPair k b c,
 ObjectPair k a (b, c), ObjectPair k (a, b) c) =>
k ((a, b), c) (a, (b, c))
regroup'
  oppositeLocalCoercion :: CanonicalDiffeomorphism (a, (b, c)) ((a, b), c)
oppositeLocalCoercion = CanonicalDiffeomorphism (a, (b, c)) ((a, b), c)
forall a b. LocallyCoercible a b => CanonicalDiffeomorphism a b
CanonicalDiffeomorphism


instance (LinearSpace (a n), Needle (a n) ~ a n)
            => Semimanifold (LinAff.Point a n) where
  type Needle (LinAff.Point a n) = a n
  LinAff.P a n
v .+~^ :: Point a n -> Needle (Point a n) -> Point a n
.+~^ Needle (Point a n)
w = a n -> Point a n
forall (f :: * -> *) a. f a -> Point f a
LinAff.P (a n -> Point a n) -> a n -> Point a n
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a n
v a n -> a n -> a n
forall v. AdditiveGroup v => v -> v -> v
^+^ a n
Needle (Point a n)
w
instance (LinearSpace (a n), Needle (a n) ~ a n)
            => PseudoAffine (LinAff.Point a n) where
  LinAff.P a n
v .-~. :: Point a n -> Point a n -> Maybe (Needle (Point a n))
.-~. LinAff.P a n
w = a n -> Maybe (a n)
forall (m :: * -> *) a. Monad m (->) => a -> m a
return (a n -> Maybe (a n)) -> a n -> Maybe (a n)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ a n
v a n -> a n -> a n
forall v. AdditiveGroup v => v -> v -> v
^-^ a n
w
  LinAff.P a n
v .-~! :: Point a n -> Point a n -> Needle (Point a n)
.-~! LinAff.P a n
w = a n
v a n -> a n -> a n
forall v. AdditiveGroup v => v -> v -> v
^-^ a n
w


instance RealFloat' r => Semimanifold (S⁰_ r) where
  type Needle (S⁰_ r) = ZeroDim r
  S⁰_ r
p .+~^ :: S⁰_ r -> Needle (S⁰_ r) -> S⁰_ r
.+~^ Needle (S⁰_ r)
Origin = S⁰_ r
p
  S⁰_ r
p .-~^ :: S⁰_ r -> Needle (S⁰_ r) -> S⁰_ r
.-~^ Needle (S⁰_ r)
Origin = S⁰_ r
p
instance RealFloat' r => PseudoAffine (S⁰_ r) where
  S⁰_ r
PositiveHalfSphere .-~. :: S⁰_ r -> S⁰_ r -> Maybe (Needle (S⁰_ r))
.-~. S⁰_ r
PositiveHalfSphere = ZeroDim r -> Maybe (ZeroDim r)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure ZeroDim r
forall s. ZeroDim s
Origin
  S⁰_ r
NegativeHalfSphere .-~. S⁰_ r
NegativeHalfSphere = ZeroDim r -> Maybe (ZeroDim r)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure ZeroDim r
forall s. ZeroDim s
Origin
  S⁰_ r
_ .-~. S⁰_ r
_ = Maybe (Needle (S⁰_ r))
forall a. Maybe a
Nothing
  S⁰_ r
PositiveHalfSphere .-~! :: S⁰_ r -> S⁰_ r -> Needle (S⁰_ r)
.-~! S⁰_ r
PositiveHalfSphere = Needle (S⁰_ r)
forall s. ZeroDim s
Origin
  S⁰_ r
NegativeHalfSphere .-~! S⁰_ r
NegativeHalfSphere = Needle (S⁰_ r)
forall s. ZeroDim s
Origin
  S⁰_ r
_ .-~! S⁰_ r
_ = String -> ZeroDim r
forall a. HasCallStack => String -> a
error String
"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 r
φ₀ .+~^ :: S¹_ r -> Needle (S¹_ r) -> S¹_ r
.+~^ Needle (S¹_ r)
δφ  = r -> S¹_ r
forall r. r -> S¹_ r
S¹Polar (r -> S¹_ r) -> r -> S¹_ r
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ r
φ'
   where φ' :: r
φ' = r -> r
forall r. RealFloat r => r -> r
toS¹range (r -> r) -> r -> r
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ r
φ₀ r -> r -> r
forall a. Num a => a -> a -> a
+ r
Needle (S¹_ r)
δφ
  semimanifoldWitness :: SemimanifoldWitness (S¹_ r)
semimanifoldWitness = case TensorSpace r => LinearManifoldWitness r
forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @r of
    LinearManifoldWitness r
LinearManifoldWitness -> SemimanifoldWitness (S¹_ r)
forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness
instance RealFloat' r => PseudoAffine (S¹_ r) where
  S¹_ r
p .-~. :: S¹_ r -> S¹_ r -> Maybe (Needle (S¹_ r))
.-~. S¹_ r
q = r -> Maybe r
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (S¹_ r
pS¹_ r -> S¹_ r -> Needle (S¹_ r)
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!S¹_ r
q)
  S¹Polar r
φ₁ .-~! :: S¹_ r -> S¹_ r -> Needle (S¹_ r)
.-~! S¹Polar r
φ₀
     | r
δφ r -> r -> Bool
forall a. Ord a => a -> a -> Bool
> r
forall a. Floating a => a
pi     = r
δφ r -> r -> r
forall a. Num a => a -> a -> a
- r
forall r. RealFloat r => r
tau
     | r
δφ r -> r -> Bool
forall a. Ord a => a -> a -> Bool
< (-r
forall a. Floating a => a
pi)  = r
δφ r -> r -> r
forall a. Num a => a -> a -> a
+ r
forall r. RealFloat r => r
tau
     | Bool
otherwise   = r
Needle (S¹_ r)
δφ
   where δφ :: r
δφ = r
φ₁ r -> r -> r
forall a. Num a => a -> a -> a
- r
φ₀



instance RealFloat' s => Semimanifold (S²_ s) where
  type Needle (S²_ s) = V2 s
  .+~^ :: S²_ s -> Needle (S²_ s) -> S²_ s
(.+~^) = case TensorSpace s => LinearManifoldWitness s
forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s of
   LinearManifoldWitness s
LinearManifoldWitness ->
      let addS² :: S²_ (Scalar v) -> v -> S²_ (Scalar v)
addS² (S²Polar Scalar v
θ₀ Scalar v
φ₀) v
𝐯 = Scalar v -> Scalar v -> S²_ (Scalar v)
forall r. r -> r -> S²_ r
S²Polar Scalar v
θ₁ Scalar v
φ₁
           where -- See images/constructions/sphericoords-needles.svg.
                 S¹Polar Scalar v
γc = v -> S¹_ (Scalar v)
forall m v. NaturallyEmbedded m v => v -> m
coEmbed v
𝐯
                 γ :: Scalar v
γ | Scalar v
θ₀ Scalar v -> Scalar v -> Bool
forall a. Ord a => a -> a -> Bool
< Scalar v
forall a. Floating a => a
piScalar v -> Scalar v -> Scalar v
forall a. Fractional a => a -> a -> a
/Scalar v
2   = Scalar v
γc Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
- Scalar v
φ₀
                   | Bool
otherwise   = Scalar v
γc Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
+ Scalar v
φ₀
                 d :: Scalar v
d = v -> Scalar v
forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude v
𝐯
                 S¹Polar Scalar v
φ₁ = Scalar v -> S¹_ (Scalar v)
forall r. r -> S¹_ r
S¹Polar Scalar v
φ₀ S¹_ (Scalar v) -> Needle (S¹_ (Scalar v)) -> S¹_ (Scalar v)
forall x. Semimanifold x => x -> Needle x -> x
.+~^ Scalar v
Needle (S¹_ (Scalar v))
δφ
                 
                 -- Cartesian coordinates of p₁ in the system whose north pole is p₀
                 -- with φ₀ as the zero meridian
                 V3 Scalar v
bx Scalar v
by Scalar v
bz = S²_ (Scalar v) -> V3 (Scalar v)
forall m v. NaturallyEmbedded m v => m -> v
embed (S²_ (Scalar v) -> V3 (Scalar v))
-> S²_ (Scalar v) -> V3 (Scalar v)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Scalar v -> Scalar v -> S²_ (Scalar v)
forall r. r -> r -> S²_ r
S²Polar Scalar v
d Scalar v
γ
                 
                 sθ₀ :: Scalar v
sθ₀ = Scalar v -> Scalar v
forall a. Floating a => a -> a
sin Scalar v
θ₀; cθ₀ :: Scalar v
cθ₀ = Scalar v -> Scalar v
forall a. Floating a => a -> a
cos Scalar v
θ₀
                 -- Cartesian coordinates of p₁ in the system with the standard north pole,
                 -- but still φ₀ as the zero meridian
                 (Scalar v
qx,Scalar v
qz) = ( Scalar v
cθ₀ Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
* Scalar v
bx Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
+ Scalar v
sθ₀ Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
* Scalar v
bz
                           ,-Scalar v
sθ₀ Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
* Scalar v
bx Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
+ Scalar v
cθ₀ Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
* Scalar v
bz )
                 qy :: Scalar v
qy      = Scalar v
by
                 
                 S²Polar Scalar v
θ₁ Scalar v
δφ = V3 (Scalar v) -> S²_ (Scalar v)
forall m v. NaturallyEmbedded m v => v -> m
coEmbed (V3 (Scalar v) -> S²_ (Scalar v))
-> V3 (Scalar v) -> S²_ (Scalar v)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Scalar v -> Scalar v -> Scalar v -> V3 (Scalar v)
forall a. a -> a -> a -> V3 a
V3 Scalar v
qx Scalar v
qy Scalar v
qz
      in S²_ s -> Needle (S²_ s) -> S²_ s
forall v.
(NaturallyEmbedded (S¹_ (Scalar v)) v, Num' (Scalar v),
 IEEE (Scalar v), InnerSpace v, InnerSpace (Scalar v)) =>
S²_ (Scalar v) -> v -> S²_ (Scalar v)
addS²

instance RealFloat' s => PseudoAffine (S²_ s) where
  S²_ s
p.-~. :: S²_ s -> S²_ s -> Maybe (Needle (S²_ s))
.-~.S²_ s
q = V2 s -> Maybe (V2 s)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (S²_ s
pS²_ s -> S²_ s -> Needle (S²_ s)
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!S²_ s
q)
  S²Polar s
θ₁ s
φ₁ .-~! :: S²_ s -> S²_ s -> Needle (S²_ s)
.-~! S²Polar s
θ₀ s
φ₀ = s
Scalar (V2 s)
d Scalar (V2 s) -> V2 s -> V2 s
forall v. VectorSpace v => Scalar v -> v -> v
*^ S¹_ s -> V2 s
forall m v. NaturallyEmbedded m v => m -> v
embed(s -> S¹_ s
forall r. r -> S¹_ r
S¹Polar s
γc)
   where -- See images/constructions/sphericoords-needles.svg.
         V3 s
qx s
qy s
qz = S²_ s -> V3 s
forall m v. NaturallyEmbedded m v => m -> v
embed (S²_ s -> V3 s) -> S²_ s -> V3 s
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s -> s -> S²_ s
forall r. r -> r -> S²_ r
S²Polar s
θ₁ (s
φ₁s -> s -> s
forall a. Num a => a -> a -> a
-s
φ₀)

         sθ₀ :: s
sθ₀ = s -> s
forall a. Floating a => a -> a
sin s
θ₀; cθ₀ :: s
cθ₀ = s -> s
forall a. Floating a => a -> a
cos s
θ₀
         (s
bx,s
bz) = ( s
cθ₀ s -> s -> s
forall a. Num a => a -> a -> a
* s
qx s -> s -> s
forall a. Num a => a -> a -> a
- s
sθ₀ s -> s -> s
forall a. Num a => a -> a -> a
* s
qz
                   , s
sθ₀ s -> s -> s
forall a. Num a => a -> a -> a
* s
qx s -> s -> s
forall a. Num a => a -> a -> a
+ s
cθ₀ s -> s -> s
forall a. Num a => a -> a -> a
* s
qz )
         by :: s
by      = s
qy

         S²Polar s
d s
γ = V3 s -> S²_ s
forall m v. NaturallyEmbedded m v => v -> m
coEmbed (V3 s -> S²_ s) -> V3 s -> S²_ s
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s -> s -> s -> V3 s
forall a. a -> a -> a -> V3 a
V3 s
bx s
by s
bz
         
         γc :: s
γc | s
θ₀ s -> s -> Bool
forall a. Ord a => a -> a -> Bool
< s
forall a. Floating a => a
pis -> s -> s
forall a. Fractional a => a -> a -> a
/s
2   = s
γ s -> s -> s
forall a. Num a => a -> a -> a
+ s
φ₀
            | Bool
otherwise   = s
γ s -> s -> s
forall a. Num a => a -> a -> a
- s
φ₀




instance Semimanifold ℝP² where
  type Needle ℝP² = ℝ²
  HemisphereℝP²Polar ℝ
θ₀ ℝ
φ₀ .+~^ :: ℝP² -> Needle ℝP² -> ℝP²
.+~^ Needle ℝP²
v
      = case ℝ -> ℝ -> S²_ ℝ
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀ S²_ ℝ -> Needle (S²_ ℝ) -> S²_ ℝ
forall x. Semimanifold x => x -> Needle x -> x
.+~^ Needle (S²_ ℝ)
Needle ℝP²
v of
          S²Polar ℝ
θ₁ ℝ
φ₁
           | ℝ
θ₁ ℝ -> ℝ -> Bool
forall a. Ord a => a -> a -> Bool
> ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Fractional a => a -> a -> a
/ℝ
2   -> ℝ -> ℝ -> ℝP²
forall r. r -> r -> ℝP²_ r
HemisphereℝP²Polar (ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
-ℝ
θ₁) (-ℝ
φ₁)
           | Bool
otherwise   -> ℝ -> ℝ -> ℝP²
forall r. r -> r -> ℝP²_ r
HemisphereℝP²Polar ℝ
θ₁        ℝ
φ₁
instance PseudoAffine ℝP² where
  ℝP²
p.-~. :: ℝP² -> ℝP² -> Maybe (Needle ℝP²)
.-~.ℝP²
q = V2 ℝ -> Maybe (V2 ℝ)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (ℝP²
pℝP² -> ℝP² -> Needle ℝP²
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!ℝP²
q)
  HemisphereℝP²Polar ℝ
θ₁ ℝ
φ₁ .-~! :: ℝP² -> ℝP² -> Needle ℝP²
.-~! HemisphereℝP²Polar ℝ
θ₀ ℝ
φ₀
      = case ℝ -> ℝ -> S²_ ℝ
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₁ ℝ
φ₁ S²_ ℝ -> S²_ ℝ -> Needle (S²_ ℝ)
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~! ℝ -> ℝ -> S²_ ℝ
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀ of
          Needle (S²_ ℝ)
v -> let r² :: ℝ
r² = V2 ℝ -> ℝ
forall v s. (InnerSpace v, s ~ Scalar v) => v -> s
magnitudeSq V2 ℝ
Needle (S²_ ℝ)
v
               in if ℝ
r²ℝ -> ℝ -> Bool
forall a. Ord a => a -> a -> Bool
>ℝ
forall a. Floating a => a
piℝ -> Int -> ℝ
forall a. Num a => a -> Int -> a
^Int
2ℝ -> ℝ -> ℝ
forall a. Fractional a => a -> a -> a
/ℝ
4
                   then ℝ -> ℝ -> S²_ ℝ
forall r. r -> r -> S²_ r
S²Polar (ℝ
forall a. Floating a => a
piℝ -> ℝ -> ℝ
forall a. Num a => a -> a -> a
-ℝ
θ₁) (-ℝ
φ₁) S²_ ℝ -> S²_ ℝ -> Needle (S²_ ℝ)
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~! ℝ -> ℝ -> S²_ ℝ
forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀
                   else Needle (S²_ ℝ)
Needle ℝP²
v


-- instance (PseudoAffine m, VectorSpace (Needle m), Scalar (Needle m) ~ ℝ)
--              => Semimanifold (CD¹ m) where
--   type Needle (CD¹ m) = (Needle m, ℝ)
--   CD¹ h₀ m₀ .+~^ (h₁δm, δh)
--       = let h₁ = min 1 . max 1e-300 $ h₀+δh; δm = h₁δm^/h₁
--         in CD¹ h₁ (m₀.+~^δm)
-- instance (PseudoAffine m, VectorSpace (Needle m), Scalar (Needle m) ~ ℝ)
--              => PseudoAffine (CD¹ m) where
--   CD¹ h₁ m₁ .-~. CD¹ h₀ m₀
--      = fmap ( \δm -> (h₁*^δm, h₁-h₀) ) $ m₁.-~.m₀
                               





class ImpliesMetric s where
  type MetricRequirement s x :: Constraint
  type MetricRequirement s x = Semimanifold x
  inferMetric :: (MetricRequirement s x, LSpace (Needle x))
                     => s x -> Metric x
  inferMetric' :: (MetricRequirement s x, LSpace (Needle x))
                     => s x -> Metric' x

instance ImpliesMetric Norm where
  type MetricRequirement Norm x = (SimpleSpace x, x ~ Needle x)
  inferMetric :: Norm x -> Metric x
inferMetric = Norm x -> Metric x
forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  inferMetric' :: Norm x -> Metric' x
inferMetric' = Norm x -> Metric' x
forall v. SimpleSpace v => Norm v -> Variance v
dualNorm



type DualNeedleWitness x = DualSpaceWitness (Needle x)



#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 .−.
-- | A connected manifold is one where any point can be reached by translation from
--   any other point.
class (PseudoAffine m) => Connected m where
  {-# MINIMAL #-}
  -- | Safe version of '(.-~.)'.
  (.−.) :: m -> m -> Needle m
  (.−.) = m -> m -> Needle m
forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
(.-~!)

instance Connected ℝ⁰
instance Connected ℝ
instance Connected ℝ¹
instance Connected ℝ²
instance Connected ℝ³
instance Connected ℝ⁴
instance Connected S¹
instance Connected S²
instance Connected ℝP⁰
instance Connected ℝP¹
instance Connected ℝP²
instance (Connected x, Connected y) => Connected (x,y)
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)