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

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


module Data.Function.Affine (
              Affine(..)
            , evalAffine
            , fromOffsetSlope
            -- * Misc
            , lensEmbedding, correspondingDirections
            ) where
    


import Data.Semigroup

import Data.MemoTrie
import Data.VectorSpace
import Data.AffineSpace
import Data.Tagged
import Data.Manifold.Types.Primitive
import Data.Manifold.PseudoAffine
import Data.Manifold.WithBoundary
import Data.Manifold.Atlas
import Data.Embedding

import qualified Prelude
import qualified Control.Applicative as Hask
import Data.Functor (($>))

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

import Math.LinearMap.Category

import Control.Lens



data Affine s d c where
    Affine :: (ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
               -> Affine s d c

instance Category (Affine s) where
  type Object (Affine s) x = ( Manifold x
                             , Atlas' x
                             , Scalar (Needle x) ~ s )
  id :: forall a. Object (Affine s) a => Affine s a a
id = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id 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 :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
  Affine ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f . :: forall a b c.
(Object (Affine s) a, Object (Affine s) b, Object (Affine s) c) =>
Affine s b c -> Affine s a b -> Affine s a c
. Affine ChartIndex a :->: (b, LinearMap s (Needle a) (Needle b))
g = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie
      forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex a
ixa -> case forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex a :->: (b, LinearMap s (Needle a) (Needle b))
g ChartIndex a
ixa of
           (b
b, LinearMap s (Needle a) (Needle b)
ða'b) -> case forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => m -> ChartIndex m
lookupAtlas b
b of
            (c
c, LinearMap s (Needle b) (Needle c)
ðb'c) -> (c
c, LinearMap s (Needle b) (Needle c)
ðb'c 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
. LinearMap s (Needle a) (Needle b)
ða'b)

instance ∀ s . (ScalarManifold s, Eq s) => Cartesian (Affine s) where
  type UnitObject (Affine s) = ZeroDim s
  swap :: forall a b.
(ObjectPair (Affine s) a b, ObjectPair (Affine s) b a) =>
Affine s (a, b) (b, a)
swap = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap 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 :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall (k :: * -> * -> *) a b.
(Cartesian k, ObjectPair k a b, ObjectPair k b a) =>
k (a, b) (b, a)
swap
  attachUnit :: forall unit a.
(unit ~ UnitObject (Affine s), ObjectPair (Affine s) a unit) =>
Affine s a (a, unit)
attachUnit = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \a
a -> ((a
a,forall s. ZeroDim s
Origin), forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k a (a, unit)
attachUnit)
  detachUnit :: forall unit a.
(unit ~ UnitObject (Affine s), ObjectPair (Affine s) a unit) =>
Affine s (a, unit) a
detachUnit = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint
                 forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \(a
a,ZeroDim s
Origin::ZeroDim s) -> (a
a, forall (k :: * -> * -> *) unit a.
(Cartesian k, unit ~ UnitObject k, ObjectPair k a unit) =>
k (a, unit) a
detachUnit)
  regroup :: forall a b c.
(ObjectPair (Affine s) a b, ObjectPair (Affine s) b c,
 ObjectPair (Affine s) a (b, c), ObjectPair (Affine s) (a, b) c) =>
Affine s (a, (b, c)) ((a, b), c)
regroup = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a 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 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 :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const 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
  regroup' :: forall a b c.
(ObjectPair (Affine s) a b, ObjectPair (Affine s) b c,
 ObjectPair (Affine s) a (b, c), ObjectPair (Affine s) (a, b) c) =>
Affine s ((a, b), c) (a, (b, c))
regroup' = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a 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' 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 :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const 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'

instance ∀ s . (ScalarManifold s, Eq s) => Morphism (Affine s) where
  Affine ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f *** :: forall b b' c c'.
(ObjectPair (Affine s) b b', ObjectPair (Affine s) c c') =>
Affine s b c -> Affine s b' c' -> Affine s (b, b') (c, c')
*** Affine ChartIndex b' :->: (c', LinearMap s (Needle b') (Needle c'))
g = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie
      forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(ChartIndex b
ixα,ChartIndex b'
ixβ) -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f ChartIndex b
ixα, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b' :->: (c', LinearMap s (Needle b') (Needle c'))
g ChartIndex b'
ixβ) of
            ((c
fα, LinearMap s (Needle b) (Needle c)
ðα'f), (c'
gβ,LinearMap s (Needle b') (Needle c')
ðβ'g)) -> ((c
fα,c'
gβ), LinearMap s (Needle b) (Needle c)
ðα'fforall (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')
***LinearMap s (Needle b') (Needle c')
ðβ'g)
  
instance ∀ s . (ScalarManifold s, Eq s) => PreArrow (Affine s) where
  Affine ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f &&& :: forall b c c'.
(Object (Affine s) b, ObjectPair (Affine s) c c') =>
Affine s b c -> Affine s b c' -> Affine s b (c, c')
&&& Affine ChartIndex b :->: (c', LinearMap s (Needle b) (Needle c'))
g = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie
      forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex b
ix -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c, LinearMap s (Needle b) (Needle c))
f ChartIndex b
ix, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex b :->: (c', LinearMap s (Needle b) (Needle c'))
g ChartIndex b
ix) of
            ((c
fα, LinearMap s (Needle b) (Needle c)
ðα'f), (c'
gβ,LinearMap s (Needle b) (Needle c')
ðβ'g)) -> ((c
fα,c'
gβ), LinearMap s (Needle b) (Needle c)
ðα'fforall (a :: * -> * -> *) b c c'.
(PreArrow a, Object a b, ObjectPair a c c') =>
a b c -> a b c' -> a b (c, c')
&&&LinearMap s (Needle b) (Needle c')
ðβ'g)
  terminal :: forall b. Object (Affine s) b => Affine s b (UnitObject (Affine s))
terminal = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex b
_ -> (forall s. ZeroDim s
Origin, forall v. AdditiveGroup v => v
zeroV)
  fst :: forall x y. ObjectPair (Affine s) x y => Affine s (x, y) x
fst = forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
 LinearSpace (Needle y), Scalar (Needle x) ~ s,
 Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
 HasTrie (ChartIndex y)) =>
Affine s (x, y) x
afst
   where afst :: ∀ x y . ( Manifold (x, y), Atlas (x, y)
                         , LinearSpace (Needle x), LinearSpace (Needle y)
                         , Scalar (Needle x) ~ s, Scalar (Needle y) ~ s
                         , HasTrie (ChartIndex x), HasTrie (ChartIndex y) )
                   => Affine s (x,y) x
         afst :: forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
 LinearSpace (Needle y), Scalar (Needle x) ~ s,
 Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
 HasTrie (ChartIndex y)) =>
Affine s (x, y) x
afst = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint @(x,y) forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \(x
x,y
_::y) -> (x
x, forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst)
  snd :: forall x y. ObjectPair (Affine s) x y => Affine s (x, y) y
snd = forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
 LinearSpace (Needle y), Scalar (Needle x) ~ s,
 Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
 HasTrie (ChartIndex y)) =>
Affine s (x, y) y
asnd
   where asnd :: ∀ x y . ( Manifold (x, y), Atlas (x, y)
                         , LinearSpace (Needle x), LinearSpace (Needle y)
                         , Scalar (Needle x) ~ s, Scalar (Needle y) ~ s
                         , HasTrie (ChartIndex x), HasTrie (ChartIndex y) )
                   => Affine s (x,y) y
         asnd :: forall x y.
(Manifold (x, y), Atlas (x, y), LinearSpace (Needle x),
 LinearSpace (Needle y), Scalar (Needle x) ~ s,
 Scalar (Needle y) ~ s, HasTrie (ChartIndex x),
 HasTrie (ChartIndex y)) =>
Affine s (x, y) y
asnd = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \(x
_::x,y
y) -> (y
y, forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd)
  
instance ∀ s . (ScalarManifold s, Eq s) => WellPointed (Affine s) where
  const :: forall b x.
(Object (Affine s) b, ObjectPoint (Affine s) x) =>
x -> Affine s b x
const x
x = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (x
x, forall v. AdditiveGroup v => v
zeroV)
  unit :: CatTagged (Affine s) (UnitObject (Affine s))
unit = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall s. ZeroDim s
Origin
  
instance EnhancedCat (->) (Affine s) where
  arr :: forall b c.
(Object (Affine s) b, Object (Affine s) c, Object (->) b,
 Object (->) c) =>
Affine s b c -> b -> c
arr Affine s b c
f = 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 x y s.
(Manifold x, Atlas x, HasTrie (ChartIndex x), Manifold y,
 s ~ Scalar (Needle x), s ~ Scalar (Needle y)) =>
Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
evalAffine Affine s b c
f
  
instance EnhancedCat (Affine s) (LinearMap s) where
  arr :: forall b c.
(Object (LinearMap s) b, Object (LinearMap s) c,
 Object (Affine s) b, Object (Affine s) c) =>
LinearMap s b c -> Affine s b c
arr = forall x y.
(LinearSpace x, Atlas x, HasTrie (ChartIndex x), LinearSpace y,
 Scalar x ~ s, Scalar y ~ s) =>
(LinearManifoldWitness x, LinearManifoldWitness y)
-> LinearMap s x y -> Affine s x y
alarr (forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness, forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness)
   where alarr :: ∀ x y . ( LinearSpace x, Atlas x, HasTrie (ChartIndex x)
                          , LinearSpace y
                          , Scalar x ~ s, Scalar y ~ s )
             => (LinearManifoldWitness x, LinearManifoldWitness y)
                  -> LinearMap s x y -> Affine s x y
         alarr :: forall x y.
(LinearSpace x, Atlas x, HasTrie (ChartIndex x), LinearSpace y,
 Scalar x ~ s, Scalar y ~ s) =>
(LinearManifoldWitness x, LinearManifoldWitness y)
-> LinearMap s x y -> Affine s x y
alarr (LinearManifoldWitness x
LinearManifoldWitness, LinearManifoldWitness y
LinearManifoldWitness) LinearMap s x y
f
             = forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint
                   forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \x
x₀ -> let y₀ :: y
y₀ = LinearMap s x y
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x
x₀
                              in (forall v. AdditiveGroup v => v -> v
negateV y
y₀, LinearMap s x y
f)

instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
         , LinearManifold (Needle x), Scalar (Needle x) ~ s
         , LinearManifold (Needle y), Scalar (Needle y) ~ s
         ) => Semimanifold (Affine s x y) where
  type Needle (Affine s x y) = Affine s x (Needle y)
  .+~^ :: Affine s x y -> Needle (Affine s x y) -> Affine s x y
(.+~^) = case ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness y ) of
    (SemimanifoldWitness y
SemimanifoldWitness) -> \(Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) (Affine ChartIndex x
:->: (Needle y, LinearMap s (Needle x) (Needle (Needle y)))
g)
      -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex x
ix -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f ChartIndex x
ix, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x
:->: (Needle y, LinearMap s (Needle x) (Needle (Needle y)))
g ChartIndex x
ix) of
          ((y
fx₀,LinearMap s (Needle x) (Needle y)
f'), (Needle y
gx₀,LinearMap s (Needle x) (Needle y)
g')) -> (y
fx₀forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle y
gx₀, LinearMap s (Needle x) (Needle y)
f'forall v. AdditiveGroup v => v -> v -> v
^+^LinearMap s (Needle x) (Needle y)
g')
  semimanifoldWitness :: SemimanifoldWitness (Affine s x y)
semimanifoldWitness = case forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @y of
    SmfdWBoundWitness y
OpenManifoldWitness -> case forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @y of
        SemimanifoldWitness y
SemimanifoldWitness -> forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @y forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness
instance ( Atlas x, HasTrie (ChartIndex x), Manifold y
         , LinearManifold (Needle x), Scalar (Needle x) ~ s
         , LinearManifold (Needle y), Scalar (Needle y) ~ s
         ) => PseudoAffine (Affine s x y) where
  Affine s x y
p.-~. :: Affine s x y -> Affine s x y -> Maybe (Needle (Affine s x y))
.-~.Affine s x y
q = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (Affine s x y
pforall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!Affine s x y
q)
  .-~! :: HasCallStack =>
Affine s x y -> Affine s x y -> Needle (Affine s x y)
(.-~!) = case ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness y ) of
    (SemimanifoldWitness y
SemimanifoldWitness) -> \(Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) (Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
g)
      -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \ChartIndex x
ix -> case (forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f ChartIndex x
ix, forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
g ChartIndex x
ix) of
          ((y
fx₀,LinearMap s (Needle x) (Needle y)
f'), (y
gx₀,LinearMap s (Needle x) (Needle y)
g')) -> (y
fx₀forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
.-~!y
gx₀, LinearMap s (Needle x) (Needle y)
f'forall v. AdditiveGroup v => v -> v -> v
^-^LinearMap s (Needle x) (Needle y)
g')
  pseudoAffineWitness :: PseudoAffineWitness (Affine s x y)
pseudoAffineWitness = case forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness :: SemimanifoldWitness y of
    SemimanifoldWitness y
SemimanifoldWitness -> forall x.
PseudoAffine (Needle x) =>
SemimanifoldWitness x -> PseudoAffineWitness x
PseudoAffineWitness (forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness)
instance ( Atlas x, HasTrie (ChartIndex x)
         , LinearManifold (Needle x), Scalar (Needle x) ~ s
         , LinearManifold (Needle y), Scalar (Needle y) ~ s
         , Manifold y, Scalar (Needle y) ~ s )
              => AffineSpace (Affine s x y) where
  type Diff (Affine s x y) = Affine s x (Needle y)
  .+^ :: Affine s x y -> Diff (Affine s x y) -> Affine s x y
(.+^) = forall x. Semimanifold x => x -> Needle x -> x
(.+~^); .-. :: Affine s x y -> Affine s x y -> Diff (Affine s x y)
(.-.) = forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
(.-~!)
instance ( Atlas x, HasTrie (ChartIndex x)
         , LinearManifold (Needle x), Scalar (Needle x) ~ s
         , LinearManifold y, Scalar y ~ s, Num' s )
            => AdditiveGroup (Affine s x y) where
  zeroV :: Affine s x y
zeroV = case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y of
       LinearManifoldWitness y
LinearManifoldWitness -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (forall v. AdditiveGroup v => v
zeroV, forall v. AdditiveGroup v => v
zeroV)
  ^+^ :: Affine s x y -> Affine s x y -> Affine s x y
(^+^) = case ( forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y
               , forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness :: DualSpaceWitness y ) of
      (LinearManifoldWitness y
LinearManifoldWitness, DualSpaceWitness y
DualSpaceWitness) -> forall x. Semimanifold x => x -> Needle x -> x
(.+~^)
  negateV :: Affine s x y -> Affine s x y
negateV = case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y of
       LinearManifoldWitness y
LinearManifoldWitness -> \(Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$
             forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> forall v. AdditiveGroup v => v -> v
negateVforall (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 v. AdditiveGroup v => v -> v
negateV
instance ( Atlas x, HasTrie (ChartIndex x)
         , LinearManifold (Needle x), Scalar (Needle x) ~ s
         , LinearManifold y, Scalar y ~ s, Num' s )
            => VectorSpace (Affine s x y) where
  type Scalar (Affine s x y) = s
  *^ :: Scalar (Affine s x y) -> Affine s x y -> Affine s x y
(*^) = case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness y of
       LinearManifoldWitness y
LinearManifoldWitness -> \Scalar (Affine s x y)
μ (Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$
             forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> (Scalar (Affine s x y)
μforall v. VectorSpace v => Scalar v -> v -> 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')
***(Scalar (Affine s x y)
μforall v. VectorSpace v => Scalar v -> v -> v
*^)

evalAffine :: ∀ x y s . ( Manifold x, Atlas x, HasTrie (ChartIndex x)
                        , Manifold y
                        , s ~ Scalar (Needle x), s ~ Scalar (Needle y) )
               => Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
evalAffine :: forall x y s.
(Manifold x, Atlas x, HasTrie (ChartIndex x), Manifold y,
 s ~ Scalar (Needle x), s ~ Scalar (Needle y)) =>
Affine s x y -> x -> (y, LinearMap s (Needle x) (Needle y))
evalAffine (Affine ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f) x
x = (y
fx₀forall x. Semimanifold x => x -> Needle x -> x
.+~^(LinearMap s (Needle x) (Needle y)
ðx'f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Needle x
v), LinearMap s (Needle x) (Needle y)
ðx'f)
 where Just Needle x
v = x
x forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. forall m. Atlas m => ChartIndex m -> m
chartReferencePoint ChartIndex x
chIx
       chIx :: ChartIndex x
chIx = forall m. Atlas m => m -> ChartIndex m
lookupAtlas x
x
       (y
fx₀, LinearMap s (Needle x) (Needle y)
ðx'f) = forall a b. HasTrie a => (a :->: b) -> a -> b
untrie ChartIndex x :->: (y, LinearMap s (Needle x) (Needle y))
f ChartIndex x
chIx

fromOffsetSlope :: ∀ x y s . ( LinearSpace x, Atlas x, HasTrie (ChartIndex x)
                             , Manifold y
                             , s ~ Scalar x, s ~ Scalar (Needle y) )
               => y -> LinearMap s x (Needle y) -> Affine s x y
fromOffsetSlope :: forall x y s.
(LinearSpace x, Atlas x, HasTrie (ChartIndex x), Manifold y,
 s ~ Scalar x, s ~ Scalar (Needle y)) =>
y -> LinearMap s x (Needle y) -> Affine s x y
fromOffsetSlope = case ( forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness :: LinearManifoldWitness x ) of
   (LinearManifoldWitness x
LinearManifoldWitness)
       -> \y
y0 LinearMap s x (Needle y)
ðx'y -> forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall m. Atlas m => ChartIndex m -> m
chartReferencePoint
                    forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \x
x₀ -> let δy :: Needle y
δy = LinearMap s x (Needle y)
ðx'y forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ x
x₀
                               in (y
y0forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle y
δy, LinearMap s x (Needle y)
ðx'y)


instance EnhancedCat (Embedding (Affine s)) (Embedding (LinearMap s)) where
  arr :: forall b c.
(Object (Embedding (LinearMap s)) b,
 Object (Embedding (LinearMap s)) c,
 Object (Embedding (Affine s)) b,
 Object (Embedding (Affine s)) c) =>
Embedding (LinearMap s) b c -> Embedding (Affine s) b c
arr (Embedding LinearMap s b c
e LinearMap s c b
p) = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (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 s b c
e) (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 s c b
p)


lensEmbedding :: ∀ k x c s .
                 ( Num' s
                 , LinearSpace x, LinearSpace c, Object k x, Object k c
                 , Scalar x ~ s, Scalar c ~ s
                 , EnhancedCat k (LinearMap s) )
                  => Lens' x c -> Embedding k c x
lensEmbedding :: forall (k :: * -> * -> *) x c s.
(Num' s, LinearSpace x, LinearSpace c, Object k x, Object k c,
 Scalar x ~ s, Scalar c ~ s, EnhancedCat k (LinearMap s)) =>
Lens' x c -> Embedding k c x
lensEmbedding Lens' x c
l = forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (\c
c -> forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' x c
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ c
c)
                                     :: LinearMap s c x) )
                            (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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (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 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall s a. s -> Getting a s a -> a
^.Lens' x c
l)
                                     :: LinearMap s x c) )


correspondingDirections :: ∀ x c t s
                        . ( WithField s AffineManifold c
                          , WithField s AffineManifold x
                          , SemiInner (Needle c), SemiInner (Needle x)
                          , RealFrac' s
                          , Traversable t )
         => (c, x) -> t (Needle c, Needle x) -> Maybe (Embedding (Affine s) c x)
correspondingDirections :: forall x c (t :: * -> *) s.
(WithField s AffineManifold c, WithField s AffineManifold x,
 SemiInner (Needle c), SemiInner (Needle x), RealFrac' s,
 Traversable t) =>
(c, x)
-> t (Needle c, Needle x) -> Maybe (Embedding (Affine s) c x)
correspondingDirections (c
c₀, x
x₀) t (Needle c, Needle x)
dirMap
   = Maybe
  (ReifiedLens' (Diff c) (t (Scalar (Diff c))),
   ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall (c :: * -> * -> *) a b. c a b -> c b a -> Embedding c a b
Embedding (forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ChartIndex c -> (x, LinearMap s (Needle c) (Needle x))
c2x)
                                 (forall d c s.
(ChartIndex d :->: (c, LinearMap s (Needle d) (Needle c)))
-> Affine s d c
Affine 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 b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ChartIndex x -> (c, LinearMap s (Needle x) (Needle c))
x2c)
 where freeEmbeddings :: Maybe
  (ReifiedLens' (Diff c) (t (Scalar (Diff c))),
   ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Monoidal f r t, ObjectPair r a b, ObjectPair t (f a) (f b),
 Object t (f (a, b))) =>
t (f a, f b) (f (a, b))
fzip ( forall v (t :: * -> *) r.
(HasCallStack, SemiInner v, RealFrac' (Scalar v), Traversable t) =>
t v -> Maybe (ReifiedLens' v (t (Scalar v)))
embedFreeSubspace forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fstforall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$>t (Needle c, Needle x)
dirMap
                             , forall v (t :: * -> *) r.
(HasCallStack, SemiInner v, RealFrac' (Scalar v), Traversable t) =>
t v -> Maybe (ReifiedLens' v (t (Scalar v)))
embedFreeSubspace forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
sndforall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$>t (Needle c, Needle x)
dirMap )
       c2t :: Lens' (Needle c) (t s)
       c2t :: Lens' (Needle c) (t s)
c2t = case Maybe
  (ReifiedLens' (Diff c) (t (Scalar (Diff c))),
   ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings of Just (Lens Lens (Diff c) (Diff c) (t s) (t s)
ct, ReifiedLens' (Diff x) (t s)
_) -> Lens (Diff c) (Diff c) (t s) (t s)
ct
       x2t :: Lens' (Needle x) (t s)
       x2t :: Lens' (Needle x) (t s)
x2t = case Maybe
  (ReifiedLens' (Diff c) (t (Scalar (Diff c))),
   ReifiedLens' (Diff x) (t (Scalar (Diff x))))
freeEmbeddings of Just (ReifiedLens' (Diff c) (t s)
_, Lens Lens (Diff x) (Diff x) (t s) (t s)
xt) -> Lens (Diff x) (Diff x) (t s) (t s)
xt
       c2x :: ChartIndex c -> (x, LinearMap s (Needle c) (Needle x))
       c2x :: ChartIndex c -> (x, LinearMap s (Needle c) (Needle x))
c2x ChartIndex c
ιc
              = ( x
x₀ forall x. Semimanifold x => x -> Needle x -> x
.+~^ (forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle x) (t s)
x2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Needle c
δcforall s a. s -> Getting a s a -> a
^.Lens' (Needle c) (t s)
c2t)
                , 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 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 s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Diff c
dc -> forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle x) (t s)
x2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Diff c
dcforall s a. s -> Getting a s a -> a
^.Lens' (Needle c) (t s)
c2t )
        where Just Needle c
δc = forall m. Atlas m => ChartIndex m -> m
chartReferencePoint ChartIndex c
ιc forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. c
c₀
       x2c :: ChartIndex x
                            -> (c, LinearMap s (Needle x) (Needle c))
       x2c :: ChartIndex x -> (c, LinearMap s (Needle x) (Needle c))
x2c ChartIndex x
ιx
              = ( c
c₀ forall x. Semimanifold x => x -> Needle x -> x
.+~^ (forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle c) (t s)
c2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Needle x
δxforall s a. s -> Getting a s a -> a
^.Lens' (Needle x) (t s)
x2t)
                , 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 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 s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Diff x
dx -> forall v. AdditiveGroup v => v
zeroV forall a b. a -> (a -> b) -> b
& Lens' (Needle c) (t s)
c2t forall s t a b. ASetter s t a b -> b -> s -> t
.~ Diff x
dxforall s a. s -> Getting a s a -> a
^.Lens' (Needle x) (t s)
x2t )
        where Just Needle x
δx = forall m. Atlas m => ChartIndex m -> m
chartReferencePoint ChartIndex x
ιx forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~. x
x₀