Autoformat everything

examples/KZmod3_2.hs

@@ -3,9 +3,9 @@ module KZmod3_2 where
 import System.IO
 
 import Math.Algebra.Group
+import Math.Topology.SGrp.KGn
 import Math.Topology.SGrp.Wbar
 import Math.Topology.SGrp.WbarDiscrete
-import Math.Topology.SGrp.KGn
 import Math.Topology.SSet.Effective
 
 main :: IO ()

examples/Pi4S3.hs

@@ -2,25 +2,28 @@ module Pi4S3 where
 
 import System.IO
 
+import Math.Topology.SGrp.KGn
+import Math.Topology.SGrp.Wbar
 import Math.Topology.SSet
 import Math.Topology.SSet.Effective
 import Math.Topology.SSet.Sphere
 import Math.Topology.SSet.TwistedProduct
-import Math.Topology.SGrp.Wbar
-import Math.Topology.SGrp.KGn
 
 s3 = Sphere 3
 kz2 = Wbar kz1
 kz3 = Wbar (Wbar kz1)
 
 classifying :: Morphism Sphere (Wbar (Wbar KZ1))
 classifying = Morphism m
-  where m Cell = NonDegen $ WbarSimplex [
-              NonDegen (WbarSimplex [NonDegen [1], NonDegen []]),
-              Degen 0 (NonDegen (WbarSimplex [])),
-              NonDegen (WbarSimplex [])
-            ]
-        m Basepoint = NonDegen $ WbarSimplex []
+  where
+    m Cell =
+      NonDegen $
+        WbarSimplex
+          [ NonDegen (WbarSimplex [NonDegen [1], NonDegen []]),
+            Degen 0 (NonDegen (WbarSimplex [])),
+            NonDegen (WbarSimplex [])
+          ]
+    m Basepoint = NonDegen $ WbarSimplex []
 
 fibration :: Twist Sphere (Wbar KZ1)
 fibration = pullback kz3 kz2 (canonicalTwist kz2) classifying

src/Control/Category/Constrained.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE RebindableSyntax #-}
+
 -- I don't want to import a whole package just for this.
 
 -- Tried to keep it minimal, no crazy tricks
@@ -7,7 +8,7 @@ module Control.Category.Constrained where
 import qualified Control.Monad (join)
 import Data.Kind (Type)
 import GHC.Exts (Constraint)
-import Prelude hiding (Functor, Monad, Traversable, fmap, id, (.), (<$>), (>>=), (>>), return)
+import Prelude hiding (Functor, Monad, Traversable, fmap, id, return, (.), (<$>), (>>), (>>=))
 import qualified Prelude
 
 infixr 9 .
@@ -47,7 +48,7 @@ class Functor (dom :: i -> i -> Type) (cod :: j -> j -> Type) (f :: i -> j) wher
 (<$>) = fmap
 infixl 4 <$>
 
-newtype Wrapped (f :: Type -> Type) a = Wrapped { unwrap :: f a }
+newtype Wrapped (f :: Type -> Type) a = Wrapped {unwrap :: f a}
 
 instance (Prelude.Functor f) => Functor (->) (->) (Wrapped f) where
   fmap f (Wrapped a) = Wrapped (Prelude.fmap f a)

src/Math/Algebra/AbGroupPres.hs

@@ -28,7 +28,7 @@ instance Eq AbGroupPres where
   a == b = reduced a == reduced b
 
 -- Cokernel of the reduced matrix
-newtype AbGroupPresElt = AbGroupPresElt { eltVector :: (Matrix Integer) }
+newtype AbGroupPresElt = AbGroupPresElt {eltVector :: (Matrix Integer)}
 
 normaliseElt :: AbGroupPres -> Matrix Integer -> AbGroupPresElt
 normaliseElt (AbGroupPres _ d _ _) c = AbGroupPresElt $ M.fromList (M.nrows d) 1 $ fmap (uncurry doMod) pairs

src/Math/Algebra/ChainComplex.hs

@@ -190,7 +190,8 @@ instance Constrained.Functor (UMorphism d) (->) UHomologyClass where
 
 homologyGenerators :: FiniteType a => HomologyGroup a -> [HomologyClass a]
 homologyGenerators (HomologyGroup n p a) = fmap HomologyClass chains
-  where chains = fmap (fromChainGrpElt a n . AbGroupPresElt . (fromReduced p *) . eltVector) (indGenerators p)
+  where
+    chains = fmap (fromChainGrpElt a n . AbGroupPresElt . (fromReduced p *) . eltVector) (indGenerators p)
 
 homologies :: FiniteType a => a -> [AbGroupPres]
 homologies a = fmap (uncurry homology) pairs
@@ -199,7 +200,7 @@ homologies a = fmap (uncurry homology) pairs
     pairs = zip (tail diffs) diffs
 
 homologyGroups :: FiniteType a => a -> [HomologyGroup a]
-homologyGroups a = fmap (\(n, f,g) -> HomologyGroup n (homology f g) a) pairs
+homologyGroups a = fmap (\(n, f, g) -> HomologyGroup n (homology f g) a) pairs
   where
     diffs = fmap (chainDiff a) [0 ..]
     pairs = zip3 [0 ..] (tail diffs) diffs

src/Math/Algebra/ChainComplex/Algebra/Bar.hs

@@ -32,17 +32,17 @@ module Math.Algebra.ChainComplex.Algebra.Bar where
 -- case, the bar construction of a differential graded algebra with
 -- coefficients in a pair of differential graded modules. "
 
-import Data.Coerce ( coerce )
-import Control.Applicative ( Applicative(liftA2) )
+import Control.Applicative (Applicative (liftA2))
 import Control.Category.Constrained ((.))
+import Data.Coerce (coerce)
 import Prelude hiding ((.))
 
 import Math.Algebra.Bicomplex hiding (FiniteType)
 import qualified Math.Algebra.Bicomplex as Bi (FiniteType)
 import Math.Algebra.ChainComplex
 import Math.Algebra.ChainComplex.Algebra
-import Math.Algebra.ChainComplex.Reduction
 import Math.Algebra.ChainComplex.Equivalence
+import Math.Algebra.ChainComplex.Reduction
 import Math.Algebra.Combination
 
 -- To implement the action of `Bar` on reductions, we need a
@@ -51,7 +51,7 @@ import Math.Algebra.Combination
 -- of the suspension of the original `a`.
 -- TODO: this could be moved to its own file
 
-newtype TensorSusp a = TensorSusp { unTensorSusp :: a }
+newtype TensorSusp a = TensorSusp {unTensorSusp :: a}
 
 newtype TensorSuspBibasis a = TensorSuspBibasis a
   deriving (Eq)
@@ -103,8 +103,9 @@ instance (Algebra a, FiniteType a) => FiniteType (TensorSusp a) where
 
 verth :: (ChainComplex a) => Morphism a a -> Morphism a a -> [Basis a] -> Combination [Basis a]
 verth h gf [] = 0
-verth h gf (b:bs) = liftA2 (:) (h `onBasis` b) (coerce (tensorAlgFunc gf `onBasis` TensorSuspBasis (TotBasis (TensorSuspBibasis bs))))
-                    + fmap (b:) (verth h gf bs)
+verth h gf (b : bs) =
+  liftA2 (:) (h `onBasis` b) (coerce (tensorAlgFunc gf `onBasis` TensorSuspBasis (TotBasis (TensorSuspBibasis bs))))
+    + fmap (b :) (verth h gf bs)
 
 tensorAlgReduction ::
   (ChainComplex a, ChainComplex b) =>
@@ -128,8 +129,8 @@ instance Algebra a => Bicomplex (Bar a) where
   type Bibasis (Bar a) = BarBibasis [Basis a]
 
   isBibasis (Bar a) = coerce (isBibasis (TensorSusp a))
-  bidegree  (Bar a) = coerce (bidegree (TensorSusp a))
-  vdiff     (Bar a) = coerce (vdiff (TensorSusp a))
+  bidegree (Bar a) = coerce (bidegree (TensorSusp a))
+  vdiff (Bar a) = coerce (vdiff (TensorSusp a))
 
   hdiff (Bar a) = Morphism (Bidegree (-1, 0)) (coerce go)
     where
@@ -180,7 +181,8 @@ barEquiv ::
   Equivalence a b ->
   Equivalence (Bar a) (Perturbed (TensorSusp b))
 barEquiv (Equivalence a l x r b) = Equivalence (Bar (unTensorSusp (perturbedOrig newa))) (coerce newl) newx newr newb
-  where (newx, newa, newl) = perturbBottom (TensorSusp x) (TensorSusp a) (tensorAlgReduction x a l) (horizPerturbation a)
-        (_, newb, newr) = perturb (TensorSusp x) (TensorSusp b) (tensorAlgReduction x b r) (perturbedDiff newx)
+  where
+    (newx, newa, newl) = perturbBottom (TensorSusp x) (TensorSusp a) (tensorAlgReduction x a l) (horizPerturbation a)
+    (_, newb, newr) = perturb (TensorSusp x) (TensorSusp b) (tensorAlgReduction x b r) (perturbedDiff newx)
 
 -- TODO: universal twisting cochain a -> Bar a (should be same as the one induced by the twist on Wbar)

src/Math/Algebra/ChainComplex/Reduction.hs

@@ -10,7 +10,7 @@ import Data.Coerce
 import Math.Algebra.ChainComplex
 import Math.Algebra.Combination (singleComb)
 
-import Prelude hiding (id, (.), fmap)
+import Prelude hiding (fmap, id, (.))
 
 data UReduction a b = Reduction
   { reductionF :: UMorphism Int a b, -- degree 0
@@ -30,8 +30,10 @@ instance Category UReduction where
 isoToReduction :: (Eq a) => UMorphism Int a b -> UMorphism Int b a -> UReduction a b
 isoToReduction f g = Reduction f g 0
 
-data Perturbed a = Perturbed { perturbedOrig :: a,
-                               perturbedDiff :: Morphism a a }
+data Perturbed a = Perturbed
+  { perturbedOrig :: a,
+    perturbedDiff :: Morphism a a
+  }
 
 newtype PerturbedBasis a = PerturbedBasis a
   deriving (Eq, Show)
@@ -58,7 +60,7 @@ perturb ::
 perturb a b (Reduction f g h) deltahat =
   (Perturbed a deltahat, Perturbed b delta, Reduction (coerce f') (coerce g') (coerce h'))
   where
-    sigmaimp d = singleComb d - fmap sigma ( (h . deltahat) `onBasis` d)
+    sigmaimp d = singleComb d - fmap sigma ((h . deltahat) `onBasis` d)
     sigma = Morphism 0 sigmaimp
     f' = f . (id - (deltahat . sigma . h))
     g' = sigma . g

src/Math/Algebra/Combination.hs

@@ -28,7 +28,7 @@ showAddTerm (0, b) = error "showTerm: 0 coefficient"
 showAddTerm (1, b) = show b
 showAddTerm (-1, b) = " - " ++ show b
 showAddTerm (c, b)
-  | c < 0 = " - " ++ show (-c) ++ "·" ++ show b
+  | c < 0 = " - " ++ show (- c) ++ "·" ++ show b
   | otherwise = " + " ++ show c ++ "·" ++ show b
 
 showSoloTerm :: Show b => (Int, b) -> String

src/Math/Topology/SGrp/KGn.hs

@@ -12,7 +12,6 @@ module Math.Topology.SGrp.KGn where
 
 import Control.Category.Constrained ((.))
 import Data.Coerce
-import Math.Algebra.Combination
 import Math.Algebra.ChainComplex as CC hiding (FiniteType, Morphism)
 import qualified Math.Algebra.ChainComplex as CC
 import Math.Algebra.ChainComplex.Algebra
@@ -21,6 +20,7 @@ import Math.Algebra.ChainComplex.Equivalence
 import Math.Algebra.ChainComplex.Reduction
 import Math.Algebra.ChainComplex.Shift
 import Math.Algebra.ChainComplex.Sum
+import Math.Algebra.Combination
 import Math.Algebra.Group
 import Math.Topology.SGrp
 import Math.Topology.SGrp.WbarDiscrete
@@ -40,10 +40,11 @@ type CircleComplex = () `Sum` Shift ()
 instance Algebra CircleComplex where
   unitMor _ = CC.Morphism 0 (const (singleComb (Left ())))
   muMor _ = CC.Morphism 0 go
-    where go (Left _, Left _) = singleComb (Left ())
-          go (Left _, Right _) = singleComb (Right (ShiftBasis ()))
-          go (Right _, Left _) = singleComb (Right (ShiftBasis ()))
-          go (Right _, Right _) = 2 .* singleComb (Right (ShiftBasis ()))
+    where
+      go (Left _, Left _) = singleComb (Left ())
+      go (Left _, Right _) = singleComb (Right (ShiftBasis ()))
+      go (Right _, Left _) = singleComb (Right (ShiftBasis ()))
+      go (Right _, Right _) = 2 .* singleComb (Right (ShiftBasis ()))
 
 instance DVF KZ1 where
   vf _ [] = Critical
@@ -94,10 +95,11 @@ instance Effective (WbarDiscrete Zmod) where
   eff w = dvfEquivalence (NChains w)
 
 -- | An efficient version of \(K(\mathbb{Z}/2, 1)\)
--- Ugly name, but what can you do?
 data KZmod2_1 = KZmod2_1
   deriving (Show)
 
+-- Ugly name, but what can you do?
+
 instance SSet KZmod2_1 where
   type GeomSimplex KZmod2_1 = Int
 

src/Math/Topology/SGrp/Wbar.hs

@@ -64,9 +64,9 @@ instance (SGrp g) => SSet (Wbar g) where
   type GeomSimplex (Wbar g) = WbarSimplex [Simplex g]
 
   isGeomSimplex (Wbar g) (WbarSimplex ss) =
-    all (\(i, s) -> simplexDim g s == i) (zip (reverse [0..length ss-1]) ss)
-    && normalise g ss == NonDegen (WbarSimplex ss)
-    && all (isSimplex g) ss
+    all (\(i, s) -> simplexDim g s == i) (zip (reverse [0 .. length ss -1]) ss)
+      && normalise g ss == NonDegen (WbarSimplex ss)
+      && all (isSimplex g) ss
 
   geomSimplexDim _ (WbarSimplex ss) = length ss
 
@@ -140,10 +140,11 @@ stripBar g (WbarSimplex as) = filter (/= basepoint g) $ fmap underlyingGeom as
 
 reconstructBar :: SGrp g => g -> [GeomSimplex g] -> GeomSimplex (Wbar g)
 reconstructBar _ [] = WbarSimplex []
-reconstructBar g (a:as) = WbarSimplex (a':nb')
-  where rest = reconstructBar g as
-        (b', a') = reconstructProduct (Wbar g) g (rest, a)
-        nb' = unnormalise g b'
+reconstructBar g (a : as) = WbarSimplex (a' : nb')
+  where
+    rest = reconstructBar g as
+    (b', a') = reconstructProduct (Wbar g) g (rest, a)
+    nb' = unnormalise g b'
 
 criticalIso ::
   forall g.
@@ -180,7 +181,6 @@ instance (SAb g, Effective g, ZeroReduced g, Algebra (Model g)) => Effective (Wb
 -- corresponding to the fibre sequence \( G \hookrightarrow W G
 -- \twoheadrightarrow \bar W G\). The total space \(W G\) is
 -- contractible.
-
 canonicalTwist :: (SGrp g) => g -> Twist (Wbar g) g
 canonicalTwist g = Twist $ \(WbarSimplex s) -> case length s of
   0 -> basepointSimplex g

src/Math/Topology/SSet.hs

@@ -151,7 +151,7 @@ someSimplices a n f | n < 0 = []
 someSimplices a n f = fmap NonDegen (f n) ++ (degensOf =<< someSimplices a (n - 1) f)
   where
     degensOf s@(NonDegen g) = fmap (\i -> Degen i s) [0 .. simplexDim a s]
-    degensOf s@(Degen j _)  = fmap (\i -> Degen i s) [(j + 1) .. simplexDim a s]
+    degensOf s@(Degen j _) = fmap (\i -> Degen i s) [(j + 1) .. simplexDim a s]
 
 allSimplices :: (FiniteType a) => a -> Int -> [Simplex a]
 allSimplices a n = someSimplices a n (geomBasis a)

src/Math/Topology/SSet/Product.hs

@@ -152,7 +152,7 @@ reconstructProduct :: (SSet a, SSet b) => a -> b -> (GeomSimplex a, GeomSimplex
 reconstructProduct a b (s, t) =
   let n = geomSimplexDim a s
       m = geomSimplexDim b t
-  in (downshiftN n (constantAt s m), constantAt t n)
+   in (downshiftN n (constantAt s m), constantAt t n)
 
 criticalIso ::
   forall a b.

src/Math/Topology/SSet/TwistedProduct.hs

@@ -1,5 +1,5 @@
-{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 -- | A principle \(G\)-bundle over \(A\), represented as a degree (-1) map of
 -- simplicial sets \(τ : A \to G\).
@@ -29,7 +29,7 @@ module Math.Topology.SSet.TwistedProduct where
 --
 
 import Data.Coerce
-import Math.Algebra.ChainComplex hiding (Morphism, FiniteType)
+import Math.Algebra.ChainComplex hiding (FiniteType, Morphism)
 import qualified Math.Algebra.ChainComplex as CC
 import Math.Algebra.ChainComplex.Equivalence
 import Math.Algebra.ChainComplex.Reduction
@@ -44,7 +44,7 @@ import Prelude hiding (id, return, (.))
 
 type Action g f = Morphism (Product f g) f
 
-newtype Twist b g = Twist { twistOnGeom :: GeomSimplex b -> Simplex g }
+newtype Twist b g = Twist {twistOnGeom :: GeomSimplex b -> Simplex g}
 
 twistOnFor :: (SSet b, Pointed g) => b -> g -> Twist b g -> Simplex b -> Simplex g
 twistOnFor a g f (NonDegen s) = f `twistOnGeom` s
@@ -85,7 +85,7 @@ instance (SSet f, SSet b, SGrp g) => SSet (TwistedProduct f b g) where
     | otherwise = TwistedProductSimplex <$> prodNormalise (face f s i, face b t i)
 
 instance (FiniteType b, FiniteType f, SGrp g) => FiniteType (TwistedProduct f b g) where
-  geomBasis (TwistedProduct f b _ _ _) n = [ TwistedProductSimplex (s, t) | s <- allSimplices f n, t <- allSimplices b n, isGeomSimplex (Product f b) (s, t)]
+  geomBasis (TwistedProduct f b _ _ _) n = [TwistedProductSimplex (s, t) | s <- allSimplices f n, t <- allSimplices b n, isGeomSimplex (Product f b) (s, t)]
 
 instance (SSet f, SSet b, SGrp g) => DVF (TwistedProduct f b g) where
   vf (TwistedProduct f b g _ _) (TwistedProductSimplex s) = coerce $ status (Product f b) s
@@ -114,6 +114,6 @@ instance
   -- TODO: compute the difference directly, likely much faster
   eff t@(TwistedProduct f b g act tau) =
     composeLeft (NChains t) (isoToReduction totalSpaceChainsIso totalSpaceChainsIsoInv) $
-    perturbLeft
+      perturbLeft
         (eff (Product f b))
         (coerce (diff (NChains (TwistedProduct f b g act tau))) - diff (NChains (Product f b)))