-- |
-- Module      : Data.Manifold.FibreBundle
-- Copyright   : (c) Justus Sagemüller 2018
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 

{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE UnicodeSyntax              #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE PatternSynonyms            #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses    #-}
#endif


module Data.Manifold.FibreBundle where


import Data.AdditiveGroup
import Data.VectorSpace
import Math.LinearMap.Category

import Data.Manifold.Types.Primitive
import Data.Manifold.PseudoAffine

import Math.Rotations.Class
    
import qualified Prelude as Hask

import Control.Category.Constrained.Prelude hiding ((^))
import Control.Category.Discrete
import Control.Arrow.Constrained

import Linear (V2(V2), V3(V3), V4(V4))

import Data.Tagged


pattern TangentBundle :: m -> Needle m -> FibreBundle m (Needle m)
pattern $bTangentBundle :: forall m. m -> Needle m -> FibreBundle m (Needle m)
$mTangentBundle :: forall {r} {m}.
FibreBundle m (Needle m)
-> (m -> Needle m -> r) -> ((# #) -> r) -> r
TangentBundle p v = FibreBundle p v

infixr 5 :@.
-- | Provided for convenience. Flipped synonym of 'FibreBundle', restricted to manifolds
--   without boundary (so the type of the whole can be inferred from its interior).
pattern (:@.) :: f -> m -> FibreBundle m f
pattern f $b:@. :: forall f m. f -> m -> FibreBundle m f
$m:@. :: forall {r} {f} {m}.
FibreBundle m f -> (f -> m -> r) -> ((# #) -> r) -> r
:@. p = FibreBundle p f

-- | 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 -> TangentBundle m
tangentAt :: forall m. AdditiveGroup (Needle m) => m -> TangentBundle m
tangentAt m
p = forall v. AdditiveGroup v => v
zeroV forall f m. f -> m -> FibreBundle m f
:@. m
p

data TransportOnNeedleWitness k m f where
  TransportOnNeedle :: (ParallelTransporting (LinearFunction (Scalar (Needle m)))
                                             (Needle m) (Needle f))
                     => TransportOnNeedleWitness k m f

data ForgetTransportProperties k m f where
  ForgetTransportProperties :: ParallelTransporting (->) m f
                     => ForgetTransportProperties k m f

class (PseudoAffine m, Category k, Object k f)
           => ParallelTransporting k m f where
  transportOnNeedleWitness :: TransportOnNeedleWitness k m f
  default transportOnNeedleWitness
      :: ParallelTransporting (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f)
           => TransportOnNeedleWitness k m f
  transportOnNeedleWitness = forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties k m f
  default forgetTransportProperties :: ParallelTransporting (->) m f
           => ForgetTransportProperties k m f
  forgetTransportProperties = forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  
  parallelTransport :: m -> Needle m -> k f f
  translateAndInvblyParTransport
        :: m -> Needle m -> (m, (k f f, k f f))
  translateAndInvblyParTransport m
p Needle m
v
              = (m
q, ( forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v
                    , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
q forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ m
pforall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!m
q ))
   where q :: m
q = m
pforall x. Semimanifold x => x -> Needle x -> x
.+~^Needle m
v

instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
      => ParallelTransporting Discrete m (ZeroDim s) where
  transportOnNeedleWitness :: TransportOnNeedleWitness Discrete m (ZeroDim s)
transportOnNeedleWitness = case (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties Discrete m (ZeroDim s)
forgetTransportProperties = case (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
        -> forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: m -> Needle m -> Discrete (ZeroDim s) (ZeroDim s)
parallelTransport m
_ Needle m
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
      => ParallelTransporting (LinearFunction s) m (ZeroDim s) where
  transportOnNeedleWitness :: TransportOnNeedleWitness (LinearFunction s) m (ZeroDim s)
transportOnNeedleWitness = case (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties (LinearFunction s) m (ZeroDim s)
forgetTransportProperties = case (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
        -> forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: m -> Needle m -> LinearFunction s (ZeroDim s) (ZeroDim s)
parallelTransport m
_ Needle m
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance ∀ m s . (PseudoAffine m, s ~ (Scalar (Needle m)), Num' s)
      => ParallelTransporting (->) m (ZeroDim s) where
  transportOnNeedleWitness :: TransportOnNeedleWitness (->) m (ZeroDim s)
transportOnNeedleWitness = case (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)) -> forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties (->) m (ZeroDim s)
forgetTransportProperties = case (forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m) of
    (PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness))
        -> forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: m -> Needle m -> ZeroDim s -> ZeroDim s
parallelTransport m
_ Needle m
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

instance (Category k, Object k ℝ) => ParallelTransporting k ℝ ℝ where
  parallelTransport :: ℝ -> Needle ℝ -> k ℝ ℝ
parallelTransport ℝ
_ Needle ℝ
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance (Category k, Object k ℝ²) => ParallelTransporting k ℝ² ℝ² where
  parallelTransport :: ℝ² -> Needle ℝ² -> k ℝ² ℝ²
parallelTransport ℝ²
_ Needle ℝ²
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance (Category k, Object k ℝ³) => ParallelTransporting k ℝ³ ℝ³ where
  parallelTransport :: ℝ³ -> Needle ℝ³ -> k ℝ³ ℝ³
parallelTransport ℝ³
_ Needle ℝ³
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
instance (Category k, Object k ℝ⁴) => ParallelTransporting k ℝ⁴ ℝ⁴ where
  parallelTransport :: ℝ⁴ -> Needle ℝ⁴ -> k ℝ⁴ ℝ⁴
parallelTransport ℝ⁴
_ Needle ℝ⁴
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

instance (Category k, Object k ℝ) => ParallelTransporting k S¹ ℝ where
  parallelTransport :: S¹ -> Needle S¹ -> k ℝ ℝ
parallelTransport S¹
_ Needle S¹
_ = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id

instance (EnhancedCat k (LinearMap ℝ), Object k ℝ²)
             => ParallelTransporting k S² ℝ² where
  parallelTransport :: S² -> Needle S² -> k ℝ² ℝ²
parallelTransport S²
p Needle S²
v = (forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst 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
. forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd) (forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport S²
p Needle S²
v)
  translateAndInvblyParTransport :: S² -> Needle S² -> (S², (k ℝ² ℝ², k ℝ² ℝ²))
translateAndInvblyParTransport (S²Polar ℝ
θ₀ ℝ
φ₀) Needle S²
𝐯
     | ℝ
d forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
pi     = (forall r. r -> r -> S²_ r
S²Polar ℝ
θ₁ ℝ
φ₁, (forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr LinearMap ℝ ℝ² ℝ²
fwd, forall (a :: * -> * -> *) (k :: * -> * -> *) b c.
(EnhancedCat a k, Object k b, Object k c, Object a b,
 Object a c) =>
k b c -> a b c
arr LinearMap ℝ ℝ² ℝ²
bwd))
     | ℝ
d forall a. Ord a => a -> a -> Bool
< ℝ
2forall a. Num a => a -> a -> a
*forall a. Floating a => a
pi   = forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport (forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀)
                      forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Needle S²
𝐯forall v s. (VectorSpace v, s ~ Scalar v) => v -> s -> v
^*(-(ℝ
2forall a. Num a => a -> a -> a
*forall a. Floating a => a
piforall a. Num a => a -> a -> a
-ℝ
d)forall a. Fractional a => a -> a -> a
/ℝ
d)
     | Bool
otherwise  = forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> (m, (k f f, k f f))
translateAndInvblyParTransport (forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ ℝ
φ₀)
                      forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ let revolutions :: Integer
revolutions = forall a b. (RealFrac a, Integral b) => a -> b
floor forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ
dforall a. Fractional a => a -> a -> a
/(ℝ
2forall a. Num a => a -> a -> a
*forall a. Floating a => a
pi)
                        in Needle S²
𝐯forall v s. (VectorSpace v, s ~ Scalar v) => v -> s -> v
^*((ℝ
d forall a. Num a => a -> a -> a
- ℝ
2forall a. Num a => a -> a -> a
*forall a. Floating a => a
piforall a. Num a => a -> a -> a
*forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
revolutions)forall a. Fractional a => a -> a -> a
/ℝ
d)
   where -- See images/constructions/sphericoords-needles.svg. Translation as in
         -- "Data.Manifold.PseudoAffine" instance.
         S¹Polar ℝ
γc₀ = forall m v. NaturallyEmbedded m v => v -> m
coEmbed Needle S²
𝐯
         γ₀ :: ℝ
γ₀ | ℝ
θ₀ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall a. Fractional a => a -> a -> a
/ℝ
2   = ℝ
γc₀ forall a. Num a => a -> a -> a
- ℝ
φ₀
            | Bool
otherwise   = ℝ
γc₀ forall a. Num a => a -> a -> a
+ ℝ
φ₀
         d :: ℝ
d = forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude Needle S²
𝐯
         S¹Polar ℝ
φ₁ = forall r. r -> S¹_ r
S¹Polar ℝ
φ₀ forall x. Semimanifold x => x -> Needle x -> x
.+~^ ℝ
δφ
         
         -- Cartesian coordinates of p₁ in the system whose north pole is p₀
         -- with φ₀ as the zero meridian
         V3 ℝ
bx ℝ
by ℝ
bz = forall m v. NaturallyEmbedded m v => m -> v
embed forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall r. r -> r -> S²_ r
S²Polar ℝ
d ℝ
γ₀
         
         sθ₀ :: ℝ
sθ₀ = forall a. Floating a => a -> a
sin ℝ
θ₀; cθ₀ :: ℝ
cθ₀ = forall a. Floating a => a -> a
cos ℝ
θ₀
         -- Cartesian coordinates of p₁ in the system with the standard north pole,
         -- but still φ₀ as the zero meridian
         (ℝ
qx,ℝ
qz) = ( ℝ
cθ₀ forall a. Num a => a -> a -> a
* ℝ
bx forall a. Num a => a -> a -> a
+ ℝ
sθ₀ forall a. Num a => a -> a -> a
* ℝ
bz
                   ,-ℝ
sθ₀ forall a. Num a => a -> a -> a
* ℝ
bx forall a. Num a => a -> a -> a
+ ℝ
cθ₀ forall a. Num a => a -> a -> a
* ℝ
bz )
         qy :: ℝ
qy      = ℝ
by
         
         S²Polar ℝ
θ₁ ℝ
δφ = forall m v. NaturallyEmbedded m v => v -> m
coEmbed forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a. a -> a -> a -> V3 a
V3 ℝ
qx ℝ
qy ℝ
qz
         
         sθ₁ :: ℝ
sθ₁ = forall a. Floating a => a -> a
sin ℝ
θ₁; cθ₁ :: ℝ
cθ₁ = forall a. Floating a => a -> a
cos ℝ
θ₁
         
         γ₁ :: ℝ
γ₁
          | ℝ
sθ₀forall a. Ord a => a -> a -> Bool
<=ℝ
sθ₁  = let
              -- Cartesian coordinates of the standard north pole in the system whose north
              -- pole is p₀ with 𝐯 along the zero meridian
              V3 ℝ
nbx ℝ
nby ℝ
nbz = forall m v. NaturallyEmbedded m v => m -> v
embed forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ (forall a. Floating a => a
piforall a. Num a => a -> a -> a
-ℝ
γ₀)
              
              sd :: ℝ
sd = forall a. Floating a => a -> a
sin ℝ
d; cd :: ℝ
cd = forall a. Floating a => a -> a
cos ℝ
d
              -- Cartesian coordinates of the standard north pole in the system whose north
              -- pole is p₁ with 𝐯 along the zero meridian
              (ℝ
ox,ℝ
oz) = ( ℝ
cd forall a. Num a => a -> a -> a
* ℝ
nbx forall a. Num a => a -> a -> a
- ℝ
sd forall a. Num a => a -> a -> a
* ℝ
nbz
                        , ℝ
sd forall a. Num a => a -> a -> a
* ℝ
nbx forall a. Num a => a -> a -> a
+ ℝ
cd forall a. Num a => a -> a -> a
* ℝ
nbz )
              oy :: ℝ
oy      = ℝ
nby

           in forall a. RealFloat a => a -> a -> a
atan2 ℝ
oy (-ℝ
ox)

          | Bool
otherwise = let
              -- Cartesian coordinates of p₀ in the system with the standard north pole,
              -- with p₁ on the zero meridian
              V3 ℝ
gx ℝ
gy ℝ
gz = forall m v. NaturallyEmbedded m v => m -> v
embed forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall r. r -> r -> S²_ r
S²Polar ℝ
θ₀ (-ℝ
δφ)
              
              -- Cartesian coordinates of p₀ in the system whose north
              -- pole is p₁ and the standard north pole on the zero meridian
              (ℝ
ux,ℝ
uz) = ( ℝ
cθ₁ forall a. Num a => a -> a -> a
* ℝ
gx forall a. Num a => a -> a -> a
- ℝ
sθ₁ forall a. Num a => a -> a -> a
* ℝ
gz
                        , ℝ
sθ₁ forall a. Num a => a -> a -> a
* ℝ
gx forall a. Num a => a -> a -> a
+ ℝ
cθ₁ forall a. Num a => a -> a -> a
* ℝ
gz )
              uy :: ℝ
uy      = ℝ
gy

           in forall a. RealFloat a => a -> a -> a
atan2 (-ℝ
uy) (-ℝ
ux)

         γc₁ :: ℝ
γc₁ | ℝ
θ₁ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall a. Fractional a => a -> a -> a
/ℝ
2  = ℝ
γ₁ forall a. Num a => a -> a -> a
+ ℝ
φ₁
             | Bool
otherwise  = ℝ
γ₁ forall a. Num a => a -> a -> a
- ℝ
φ₁

         (ℝ
sδγc, ℝ
cδγc) = forall a. Floating a => a -> a
sin forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall a. Floating a => a -> a
cos forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝ
γc₁ forall a. Num a => a -> a -> a
- ℝ
γc₀

         fwd :: LinearMap ℝ ℝ² ℝ²
fwd = forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap (forall a. a -> a -> V2 a
V2 (forall a. a -> a -> V2 a
V2   ℝ
cδγc  ℝ
sδγc)
                             (forall a. a -> a -> V2 a
V2 (-ℝ
sδγc) ℝ
cδγc)) :: LinearMap ℝ ℝ² ℝ²
         bwd :: LinearMap ℝ ℝ² ℝ²
bwd = forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap (forall a. a -> a -> V2 a
V2 (forall a. a -> a -> V2 a
V2 ℝ
cδγc (-ℝ
sδγc))
                             (forall a. a -> a -> V2 a
V2 ℝ
sδγc   ℝ
cδγc )) :: LinearMap ℝ ℝ² ℝ²


instance {-# OVERLAPS #-} ∀ k a b fa fb s .
         ( ParallelTransporting k a fa, ParallelTransporting k b fb
         , PseudoAffine fa, PseudoAffine fb
         , Scalar (Needle a) ~ s, Scalar (Needle b) ~ s
         , Scalar (Needle fa) ~ s, Scalar (Needle fb) ~ s
         , Num' s
         , Morphism k, ObjectPair k fa fb )
              => ParallelTransporting k (a,b) (fa,fb) where
  transportOnNeedleWitness :: TransportOnNeedleWitness k (a, b) (fa, fb)
transportOnNeedleWitness = case
         ( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness a
         , forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness b
         , forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness fa
         , forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness fb
         , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a fa
         , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k b fb ) of
     ( PseudoAffineWitness (SemimanifoldWitness a
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness b
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness fa
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness fb
SemimanifoldWitness)
      ,TransportOnNeedleWitness k a fa
TransportOnNeedle, TransportOnNeedleWitness k b fb
TransportOnNeedle)
         -> forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties k (a, b) (fa, fb)
forgetTransportProperties = case
    ( forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a fa
    , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k b fb ) of
     (ForgetTransportProperties k a fa
ForgetTransportProperties, ForgetTransportProperties k b fb
ForgetTransportProperties) -> forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: (a, b) -> Needle (a, b) -> k (fa, fb) (fa, fb)
parallelTransport (a
pa,b
pb) (Needle a
va,Needle b
vb)
       = forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
pa Needle a
va  forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport b
pb Needle b
vb

instance ∀ k a f g s .
         ( ParallelTransporting k a f, ParallelTransporting k a g
         , ParallelTransporting (LinearFunction s) (Needle a) (Needle f, Needle g)
         , PseudoAffine f, PseudoAffine g
         , Morphism k, ObjectPair k f g )
              => ParallelTransporting k a (f,g) where
  transportOnNeedleWitness :: TransportOnNeedleWitness k a (f, g)
transportOnNeedleWitness = case
         ( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness a
         , forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness f
         , forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness g
         , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a f
         , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
TransportOnNeedleWitness k m f
transportOnNeedleWitness :: TransportOnNeedleWitness k a g ) of
     ( PseudoAffineWitness (SemimanifoldWitness a
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness f
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness g
SemimanifoldWitness)
      ,TransportOnNeedleWitness k a f
TransportOnNeedle, TransportOnNeedleWitness k a g
TransportOnNeedle)
         -> forall m f (k :: * -> * -> *).
ParallelTransporting
  (LinearFunction (Scalar (Needle m))) (Needle m) (Needle f) =>
TransportOnNeedleWitness k m f
TransportOnNeedle
  forgetTransportProperties :: ForgetTransportProperties k a (f, g)
forgetTransportProperties = case
    ( forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a f
    , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties :: ForgetTransportProperties k a g ) of
     (ForgetTransportProperties k a f
ForgetTransportProperties, ForgetTransportProperties k a g
ForgetTransportProperties) -> forall m f (k :: * -> * -> *).
ParallelTransporting (->) m f =>
ForgetTransportProperties k m f
ForgetTransportProperties
  parallelTransport :: a -> Needle a -> k (f, g) (f, g)
parallelTransport a
p Needle a
v
       = forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
p Needle a
v forall (a :: * -> * -> *) b b' c c'.
(Morphism a, ObjectPair a b b', ObjectPair a c c') =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport a
p Needle a
v


instance ( ParallelTransporting (LinearFunction (Scalar f)) m f, AdditiveGroup m
         , VectorSpace f )
                => AdditiveGroup (FibreBundle m f) where
  zeroV :: FibreBundle m f
zeroV = forall b f. b -> f -> FibreBundle b f
FibreBundle forall v. AdditiveGroup v => v
zeroV forall v. AdditiveGroup v => v
zeroV
  FibreBundle m
p f
v ^+^ :: FibreBundle m f -> FibreBundle m f -> FibreBundle m f
^+^ FibreBundle m
q f
w = forall b f. b -> f -> FibreBundle b f
FibreBundle (m
pforall v. AdditiveGroup v => v -> v -> v
^+^m
q) (f
vforall v. AdditiveGroup v => v -> v -> v
^+^f
w)
  negateV :: FibreBundle m f -> FibreBundle m f
negateV (FibreBundle m
p f
v) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall v. AdditiveGroup v => v -> v
negateV m
p) (forall v. AdditiveGroup v => v -> v
negateV f
v)

instance ∀ m f s .
         ( ParallelTransporting (->) m f, Semimanifold f
         , ParallelTransporting (LinearFunction s) (Needle m) (Needle f)
         , s ~ Scalar (Needle m) )
                => Semimanifold (FibreBundle m f) where
  type Needle (FibreBundle m f) = FibreBundle (Needle m) (Needle f)
  semimanifoldWitness :: SemimanifoldWitness (FibreBundle m f)
semimanifoldWitness = case ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness m
                             , forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness f
                             , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties
                               :: ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
                             ) of
         (SemimanifoldWitness m
SemimanifoldWitness, SemimanifoldWitness f
SemimanifoldWitness
          ,ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
ForgetTransportProperties)
           -> forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness
  FibreBundle m
p f
f .+~^ :: FibreBundle m f -> Needle (FibreBundle m f) -> FibreBundle m f
.+~^ FibreBundle Needle m
v Needle f
δf
      = forall b f. b -> f -> FibreBundle b f
FibreBundle (m
pforall x. Semimanifold x => x -> Needle x -> x
.+~^Needle m
v) (forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v f
fforall x. Semimanifold x => x -> Needle x -> x
.+~^Needle f
δf)

instance ∀ m f s .
         ( ParallelTransporting (->) m f
         , PseudoAffine f
         , ParallelTransporting (LinearFunction s) (Needle m) (Needle f)
         , s ~ Scalar (Needle m) )
                => PseudoAffine (FibreBundle m f) where
  pseudoAffineWitness :: PseudoAffineWitness (FibreBundle m f)
pseudoAffineWitness = case ( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness m
                             , forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness :: PseudoAffineWitness f
                             , forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
ForgetTransportProperties k m f
forgetTransportProperties
                               :: ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
                             ) of
     ( PseudoAffineWitness (SemimanifoldWitness m
SemimanifoldWitness)
      ,PseudoAffineWitness (SemimanifoldWitness f
SemimanifoldWitness)
      ,ForgetTransportProperties (LinearFunction s) (Needle m) (Needle f)
ForgetTransportProperties)
         -> forall x.
PseudoAffine (Needle x) =>
SemimanifoldWitness x -> PseudoAffineWitness x
PseudoAffineWitness (forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness)
  FibreBundle m
p f
f .-~! :: HasCallStack =>
FibreBundle m f -> FibreBundle m f -> Needle (FibreBundle m f)
.-~! FibreBundle m
q f
g = case m
pforall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!m
q of
      Needle m
v  -> forall b f. b -> f -> FibreBundle b f
FibreBundle Needle m
v forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ f
f forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~! forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v f
g
  FibreBundle m
p f
f .-~. :: FibreBundle m f
-> FibreBundle m f -> Maybe (Needle (FibreBundle m f))
.-~. FibreBundle m
q f
g = case m
pforall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~.m
q of
      Maybe (Needle m)
Nothing -> forall a. Maybe a
Nothing
      Just Needle m
v  -> forall b f. b -> f -> FibreBundle b f
FibreBundle Needle m
v forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> f
f forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. forall (k :: * -> * -> *) m f.
ParallelTransporting k m f =>
m -> Needle m -> k f f
parallelTransport m
p Needle m
v f
g


instance (AdditiveGroup f) => NaturallyEmbedded x (FibreBundle x f) where
  embed :: x -> FibreBundle x f
embed x
x = forall b f. b -> f -> FibreBundle b f
FibreBundle x
x forall v. AdditiveGroup v => v
zeroV
  coEmbed :: FibreBundle x f -> x
coEmbed (FibreBundle x
x f
_) = x
x

instance (NaturallyEmbedded m v, VectorSpace f)
    => NaturallyEmbedded (FibreBundle m (ZeroDim s)) (FibreBundle v f) where
  embed :: FibreBundle m (ZeroDim s) -> FibreBundle v f
embed (FibreBundle m
x ZeroDim s
Origin) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall m v. NaturallyEmbedded m v => m -> v
embed m
x) forall v. AdditiveGroup v => v
zeroV
  coEmbed :: FibreBundle v f -> FibreBundle m (ZeroDim s)
coEmbed (FibreBundle v
u f
_) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall m v. NaturallyEmbedded m v => v -> m
coEmbed v
u) forall s. ZeroDim s
Origin

instance (AdditiveGroup y, AdditiveGroup g)
           => NaturallyEmbedded (FibreBundle x f) (FibreBundle (x,y) (f,g)) where
  embed :: FibreBundle x f -> FibreBundle (x, y) (f, g)
embed (FibreBundle x
x f
δx) = forall b f. b -> f -> FibreBundle b f
FibreBundle (x
x,forall v. AdditiveGroup v => v
zeroV) (f
δx,forall v. AdditiveGroup v => v
zeroV)
  coEmbed :: FibreBundle (x, y) (f, g) -> FibreBundle x f
coEmbed (FibreBundle (x
x,y
_) (f
δx,g
_)) = forall b f. b -> f -> FibreBundle b f
FibreBundle x
x f
δx

instance NaturallyEmbedded v w
      => NaturallyEmbedded (FibreBundle ℝ v) (FibreBundle ℝ w) where
  embed :: FibreBundle ℝ v -> FibreBundle ℝ w
embed (FibreBundle ℝ
p v
v) = forall b f. b -> f -> FibreBundle b f
FibreBundle ℝ
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle ℝ w -> FibreBundle ℝ v
coEmbed (FibreBundle ℝ
p w
w) = forall b f. b -> f -> FibreBundle b f
FibreBundle ℝ
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w
instance (NaturallyEmbedded v w, s'~s)
      => NaturallyEmbedded (FibreBundle (V2 s) v) (FibreBundle (V2 s') w) where
  embed :: FibreBundle (V2 s) v -> FibreBundle (V2 s') w
embed (FibreBundle V2 s
p v
v) = forall b f. b -> f -> FibreBundle b f
FibreBundle V2 s
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle (V2 s') w -> FibreBundle (V2 s) v
coEmbed (FibreBundle V2 s'
p w
w) = forall b f. b -> f -> FibreBundle b f
FibreBundle V2 s'
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w
instance (NaturallyEmbedded v w, s'~s)
      => NaturallyEmbedded (FibreBundle (V3 s) v) (FibreBundle (V3 s') w) where
  embed :: FibreBundle (V3 s) v -> FibreBundle (V3 s') w
embed (FibreBundle V3 s
p v
v) = forall b f. b -> f -> FibreBundle b f
FibreBundle V3 s
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle (V3 s') w -> FibreBundle (V3 s) v
coEmbed (FibreBundle V3 s'
p w
w) = forall b f. b -> f -> FibreBundle b f
FibreBundle V3 s'
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w
instance (NaturallyEmbedded v w, s'~s)
      => NaturallyEmbedded (FibreBundle (V4 s) v) (FibreBundle (V4 s') w) where
  embed :: FibreBundle (V4 s) v -> FibreBundle (V4 s') w
embed (FibreBundle V4 s
p v
v) = forall b f. b -> f -> FibreBundle b f
FibreBundle V4 s
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => m -> v
embed v
v
  coEmbed :: FibreBundle (V4 s') w -> FibreBundle (V4 s) v
coEmbed (FibreBundle V4 s'
p w
w) = forall b f. b -> f -> FibreBundle b f
FibreBundle V4 s'
p forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m v. NaturallyEmbedded m v => v -> m
coEmbed w
w

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¹_ s) s' -> FibreBundle (V2 s'') (V2 s''')
embed (FibreBundle (S¹Polar s
φ) s'
l) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall a. a -> a -> V2 a
V2 s'''
cφ s'''
sφ) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s'
lforall v. VectorSpace v => Scalar v -> v -> v
*^(forall a. a -> a -> V2 a
V2 (-s'''
sφ) s'''
cφ)
   where (s'''
cφ, s'''
sφ) = (forall a. Floating a => a -> a
cos forall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&& forall a. Floating a => a -> a
sin) s
φ
  coEmbed :: FibreBundle (V2 s'') (V2 s''') -> FibreBundle (S¹_ s) s'
coEmbed (FibreBundle (V2 s''
0 s''
0) (V2 s'''
_ s'''
δy)) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall r. r -> S¹_ r
S¹Polar s
0) s'''
δy
  coEmbed (FibreBundle V2 s''
p (V2 s'''
δx s'''
δy)) = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall r. r -> S¹_ r
S¹Polar forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a. RealFloat a => a -> a -> a
atan2 s''
sφ s''
cφ) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
cφforall a. Num a => a -> a -> a
*s'''
δy forall a. Num a => a -> a -> a
- s''
sφforall a. Num a => a -> a -> a
*s'''
δx
   where V2 s''
cφ s''
sφ = V2 s''
pforall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/s'''
r
         r :: s'''
r = forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude V2 s''
p

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²_ s) (V2 s') -> FibreBundle (V3 s'') (V3 s''')
embed (FibreBundle (S²Polar s
θ s
φ) v :: V2 s'
v@(V2 s'
δξ s'
δυ))
       = forall b f. b -> f -> FibreBundle b f
FibreBundle (forall a. a -> a -> a -> V3 a
V3 (s''
sθforall a. Num a => a -> a -> a
*s''
cφ) (s''
sθforall a. Num a => a -> a -> a
*s''
sφ) s''
cθ) V3 s''
𝐯r
   where [V2 s''
cθ s''
sθ, V2 s''
cφ s''
sφ] = forall m v. NaturallyEmbedded m v => m -> v
embed 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
. forall r. r -> S¹_ r
S¹Polar forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> [s
θ,s
φ]
         S¹Polar s
γc = forall m v. NaturallyEmbedded m v => v -> m
coEmbed V2 s'
v
         γ :: s
γ | s
θ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall a. Fractional a => a -> a -> a
/s
2   = s
γc forall a. Num a => a -> a -> a
- s
φ
           | Bool
otherwise  = s
γc forall a. Num a => a -> a -> a
+ s
φ
         d :: s'''
d = forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude V2 s'
v

         V2 s'''
δθ s'''
δφ = s'''
d forall v. VectorSpace v => Scalar v -> v -> v
*^ forall m v. NaturallyEmbedded m v => m -> v
embed (forall r. r -> S¹_ r
S¹Polar s
γ)
         
         𝐞φ :: V3 s''
𝐞φ = forall a. a -> a -> a -> V3 a
V3 (-s''
sφ) s''
cφ s''
0
         𝐞θ :: V3 s''
𝐞θ = forall a. a -> a -> a -> V3 a
V3 (s''
cθforall a. Num a => a -> a -> a
*s''
cφ) (s''
cθforall a. Num a => a -> a -> a
*s''
sφ) (-s''
sθ)
         𝐯r :: V3 s''
𝐯r = s'''
δθforall v. VectorSpace v => Scalar v -> v -> v
*^V3 s''
𝐞θ forall v. AdditiveGroup v => v -> v -> v
^+^ s'''
δφforall v. VectorSpace v => Scalar v -> v -> v
*^V3 s''
𝐞φ
  
  coEmbed :: FibreBundle (V3 s'') (V3 s''') -> FibreBundle (S²_ s) (V2 s')
coEmbed (FibreBundle (V3 s''
x s''
y s''
z) V3 s'''
𝐯r) = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of
   ClosedScalarWitness s
ClosedScalarWitness -> forall b f. b -> f -> FibreBundle b f
FibreBundle (forall r. r -> r -> S²_ r
S²Polar s''
θ s''
φ) (forall v s. (InnerSpace v, s ~ Scalar v, Floating s) => v -> s
magnitude (Scalar (V3 s'')
δθ,Scalar (V3 s'')
δφ) forall v. VectorSpace v => Scalar v -> v -> v
*^ forall m v. NaturallyEmbedded m v => m -> v
embed (forall r. r -> S¹_ r
S¹Polar s''
γc))
     where r :: s''
r = forall a. Floating a => a -> a
sqrt forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
xforall a. Num a => a -> Int -> a
^Int
2 forall a. Num a => a -> a -> a
+ s''
yforall a. Num a => a -> Int -> a
^Int
2 forall a. Num a => a -> a -> a
+ s''
zforall a. Num a => a -> Int -> a
^Int
2
           rxy :: s''
rxy = forall a. Floating a => a -> a
sqrt forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ s''
xforall a. Num a => a -> Int -> a
^Int
2 forall a. Num a => a -> a -> a
+ s''
yforall a. Num a => a -> Int -> a
^Int
2
           θ :: s''
θ = forall a. RealFloat a => a -> a -> a
atan2 s''
rxy s''
z
           φ :: s''
φ = forall a. RealFloat a => a -> a -> a
atan2 s''
y s''
x
           cθ :: s''
cθ = s''
z forall a. Fractional a => a -> a -> a
/ s''
r
           sθ :: s''
sθ = s''
rxy forall a. Fractional a => a -> a -> a
/ s''
r
           (s''
cφ,s''
sφ) | s''
rxyforall a. Ord a => a -> a -> Bool
>s''
0      = (s''
x,s''
y)forall v s.
(VectorSpace v, s ~ Scalar v, Fractional s) =>
v -> s -> v
^/s''
rxy
                   | Bool
otherwise  = (s''
1,s''
0)
           𝐞φ :: V3 s''
𝐞φ = forall a. a -> a -> a -> V3 a
V3 (-s''
sφ) s''
cφ s''
0
           𝐞θ :: V3 s''
𝐞θ = forall a. a -> a -> a -> V3 a
V3 (s''
cθforall a. Num a => a -> a -> a
*s''
cφ) (s''
cθforall a. Num a => a -> a -> a
*s''
sφ) (-s''
sθ)
           δθ :: Scalar (V3 s'')
δθ = V3 s''
𝐞θ forall v. InnerSpace v => v -> v -> Scalar v
<.> V3 s'''
𝐯r
           δφ :: Scalar (V3 s'')
δφ = V3 s''
𝐞φ forall v. InnerSpace v => v -> v -> Scalar v
<.> V3 s'''
𝐯r
           γ :: s''
γ = forall a. RealFloat a => a -> a -> a
atan2 Scalar (V3 s'')
δφ Scalar (V3 s'')
δθ
           γc :: s''
γc | s''
θ forall a. Ord a => a -> a -> Bool
< forall a. Floating a => a
piforall a. Fractional a => a -> a -> a
/s''
2   = s''
γ forall a. Num a => a -> a -> a
+ s''
φ
              | Bool
otherwise  = s''
γ forall a. Num a => a -> a -> a
- s''
φ


-- | @ex -> ey@, @ey -> ez@, @ez -> ex@
transformEmbeddedTangents
    :: ∀ x f v . ( NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) )
           => (v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents :: forall x f v.
NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) =>
(v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents v -> v
f FibreBundle x f
p = case forall m v. NaturallyEmbedded m v => m -> v
embed FibreBundle x f
p :: FibreBundle v v of
    FibreBundle v
v v
δv -> forall m v. NaturallyEmbedded m v => v -> m
coEmbed (forall b f. b -> f -> FibreBundle b f
FibreBundle (v -> v
f v
v) (v -> v
f v
δv) :: FibreBundle v v)


instance (s~ℝ, s'~ℝ) => Rotatable (FibreBundle (S²_ s) (V2 s')) where
  type AxisSpace (FibreBundle (S²_ s) (V2 s')) = ℝP²_ s
  rotateAbout :: AxisSpace (FibreBundle (S²_ s) (V2 s'))
-> S¹ -> FibreBundle (S²_ s) (V2 s') -> FibreBundle (S²_ s) (V2 s')
rotateAbout AxisSpace (FibreBundle (S²_ s) (V2 s'))
axis S¹
angle = forall x f v.
NaturallyEmbedded (FibreBundle x f) (FibreBundle v v) =>
(v -> v) -> FibreBundle x f -> FibreBundle x f
transformEmbeddedTangents
        forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ℝP² -> S¹ -> ℝ³ -> ℝ³
rotateℝ³AboutCenteredAxis AxisSpace (FibreBundle (S²_ s) (V2 s'))
axis S¹
angle