diff --git a/CartesianCategories/PackageInfo.g b/CartesianCategories/PackageInfo.g
index b8b886cfa4..ba5605c106 100644
--- a/CartesianCategories/PackageInfo.g
+++ b/CartesianCategories/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "CartesianCategories",
 Subtitle := "Cartesian and cocartesian categories and various subdoctrines",
-Version := "2023.08-02",
+Version := "2023.08-03",
 Date := ~.Version{[ 1 .. 10 ]},
 Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
 License := "GPL-2.0-or-later",
diff --git a/CartesianCategories/gap/AUTOGENERATED_FROM.md b/CartesianCategories/gap/AUTOGENERATED_FROM.md
index 759056a2d8..c33d703aae 100644
--- a/CartesianCategories/gap/AUTOGENERATED_FROM.md
+++ b/CartesianCategories/gap/AUTOGENERATED_FROM.md
@@ -1,3 +1,3 @@
 The files of this package which include the line `THIS FILE WAS AUTOMATICALLY GENERATED` in their header have been autogenerated
 
-* from MonoidalCategories v2023.05-02
+* from MonoidalCategories v2023.08-01
diff --git a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
index 248388a2d0..ef795323f4 100644
--- a/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
+++ b/CartesianCategories/gap/SymmetricCartesianClosedCategoriesDerivedMethods.gi
@@ -158,7 +158,7 @@ AddDerivationToCAP( MorphismToCartesianBidualWithGivenCartesianBidual,
                     
   function( cat, a, avv )
     local morphism, av, tensor_unit;
-
+    
     #        a
     #        |
     #        | coev_(a,a^v)
@@ -230,7 +230,7 @@ AddDerivationToCAP( CartesianDualOnMorphismsWithGivenCartesianDuals,
                       [ IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject, 1 ] ],
                     
   function( cat, s, alpha, r )
-
+    
     # alpha: a → b
     #
     #   b^v
@@ -383,7 +383,7 @@ AddDerivationToCAP( DirectProductExponentialCompatibilityMorphismWithGivenObject
     #
     #
     # Adjoint[ (Exp(a1,b1) × Exp(a2,b2)) × (a1 × a2) → b1 × b2 ] = [ Exp(a1,b1) × Exp(a2,b2) → Exp(a1 × a2, b1 × b2) ]
-
+    
     a1 := list[1];
     b1 := list[2];
     a2 := list[3];
@@ -453,7 +453,7 @@ AddDerivationToCAP( DirectProductCartesianDualityCompatibilityMorphismWithGivenO
                     
   function( cat, s, a, b, r )
     local morphism, unit, direct_product_on_a_and_b;
-
+    
     #      a^v × b^v
     #          |
     #          v
@@ -535,7 +535,7 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,
                     
   function( cat, a, internal_hom )
     local unit;
-
+    
     # ρ_a: a × 1 → a
     #
     # Adjoint( ρ_a ) = ( a → Exp(1,a) )
@@ -572,7 +572,7 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,
                     
   function( cat, a, internal_hom )
     local unit;
-
+    
     #  Exp(1,a)
     #      |
     #      | ( ρ_Exp(1,a) )^-1
@@ -618,7 +618,7 @@ AddDerivationToCAP( MorphismFromDirectProductToExponentialWithGivenObjects,
                     
   function( cat, direct_product_object, a, b, internal_hom )
     local unit;
-
+    
     #      a^v × b
     #          |
     #          v
@@ -631,7 +631,7 @@ AddDerivationToCAP( MorphismFromDirectProductToExponentialWithGivenObjects,
     #          | Exp((ρ_a)^-1, λ_b)
     #          v
     #       Exp(a,b)
-
+    
     unit := TerminalObject( cat );
     
     return PreComposeList( cat, [
@@ -699,7 +699,7 @@ AddDerivationToCAP( CartesianPreComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local exp_a_b, exp_b_c, morphism;
-
+    
     # (Exp(a,b) × Exp(b,c)) × a
     #           |
     #           | α_( ( Exp(a,b), Exp(b,c) ), a)
@@ -772,7 +772,7 @@ AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local exp_a_b, exp_b_c, morphism;
-
+    
     # (Exp(b,c) × Exp(a,b)) × a
     #            |
     #            | α_( ( Exp(b,c), Exp(a,b) ), c )
@@ -879,7 +879,7 @@ AddDerivationToCAP( DirectProductExponentialCompatibilityMorphismWithGivenObject
                     
   function( cat, source, list, range )
     local a1, b1, a2, b2, morphism, exp_a1_b1, exp_a2_b2, id_a2, direct_product_on_objects_exp_a1_b1_exp_a2_b2;
-
+    
     # Exp(a1,b1) × Exp(a2,b2) × a1 × a2
     #                 |
     #                 | id_Exp(a1,b1) × B_( Exp(a2,b2), a1 ) × id_a2
@@ -949,7 +949,7 @@ AddDerivationToCAP( DirectProductCartesianDualityCompatibilityMorphismWithGivenO
                     
   function( cat, source, a, b, range )
     local morphism, unit, direct_product_on_a_and_b;
-
+    
     #      a^v × b^v
     #          |
     #          v
@@ -1054,7 +1054,7 @@ AddDerivationToCAP( CartesianPostComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local exp_a_b, exp_b_c, morphism;
-
+    
     # Exp(b,c) × Exp(a,b) × a
     #            |
     #            | id_Exp(b,c) × ev_ab
diff --git a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
index 15f32a5ead..f4a81102ad 100644
--- a/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
+++ b/CartesianCategories/gap/SymmetricCocartesianCoclosedCategoriesDerivedMethods.gi
@@ -75,7 +75,7 @@ AddDerivationToCAP( CoexponentialToCoproductAdjunctionMap,
                       [ IdentityMorphism, 1 ] ],
                     
   function( cat, a, b, f )
-
+    
     # f: Coexp(a,b) → c
     #
     #        a
@@ -102,7 +102,7 @@ AddDerivationToCAP( UniversalPropertyOfCocartesianDual,
                       [ CoproductToCoexponentialAdjunctionMap, 1 ] ],
                     
   function( cat, t, a, alpha )
-
+    
     # alpha: 1 → t ⊔ a
     #
     # a_v → ( Coexp(1,a) → t ) = Adjoint( alpha )
@@ -124,7 +124,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,
                     
   function( cat, a, avv )
     local alpha;
-
+    
     #    1
     #    |
     #    | cocaev_a
@@ -160,7 +160,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,
                     
   function( cat, a, avv )
     local morphism, av, tensor_unit;
-
+    
     #     Coexp(1, a_v)
     #          |
     #          | Coexp( cocaev_(1,a), id_(a_v) )
@@ -192,7 +192,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,
                 ] );
     
     return morphism;
-
+    
 end : CategoryFilter := IsCocartesianCoclosedCategory );
 
 ##
@@ -201,7 +201,7 @@ AddDerivationToCAP( CocartesianDualOnObjects,
                     [ [ IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject, 1 ] ],
                     
   function( cat, a )
-
+    
     # Source( a_v → Coexp(1,a) )
     
     return Source( IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject( cat, a ) );
@@ -214,7 +214,7 @@ AddDerivationToCAP( CocartesianDualOnObjects,
                     [ [ IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject, 1 ] ],
                     
   function( cat, a )
-
+    
     # Range( Coexp(1,a) → a_v )
     
     return Range( IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( cat, a ) );
@@ -233,7 +233,7 @@ AddDerivationToCAP( CocartesianDualOnMorphismsWithGivenCocartesianDuals,
                     
   function( cat, s, alpha, r )
     local result_morphism;
-
+    
     # alpha: a → b
     #
     #    b_v
@@ -269,9 +269,9 @@ AddDerivationToCAP( CocartesianEvaluationForCocartesianDualWithGivenCoproduct,
                       [ IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject, 1 ] ],
                     
   function( cat, s, a, r )
-
+    
     # s := 1
-
+    
     # Adjoint( Coexp(1,a) → a_v ) = ( 1 → a_v ⊔ a )
 
     return CoexponentialToCoproductAdjunctionMap( cat,
@@ -291,7 +291,7 @@ AddDerivationToCAP( CocartesianLambdaIntroduction,
                     
   function( cat, alpha )
     local result_morphism, range;
-
+    
     #   a
     #   |
     #   | alpha
@@ -324,7 +324,7 @@ AddDerivationToCAP( CocartesianLambdaElimination,
                     
   function( cat, a, b, alpha )
     local result_morphism;
-
+    
     # alpha: Coexp(a,b) → 1
     # Adjoint( alpha ) = ( a → 1 ⊔ b )
     #
@@ -360,7 +360,7 @@ AddDerivationToCAP( CoexponentialCoproductCompatibilityMorphismWithGivenObjects,
                     
   function( cat, source, list, range )
     local a1, a2, b1, b2, morphism, coexp_a1_b1, coexp_a2_b2, id_b2, coproduct_on_objects_coexp_a1_b1_coexp_a2_b2;
-
+    
     #                   a1 ⊔ a2
     #                      |
     #                      | id_a1 ⊔ cocaev_(a2,b2)
@@ -402,7 +402,7 @@ AddDerivationToCAP( CoexponentialCoproductCompatibilityMorphismWithGivenObjects,
     coexp_a1_b1 := CoexponentialOnObjects( cat, a1, b1 );
     
     coexp_a2_b2 := CoexponentialOnObjects( cat, a2, b2 );
-
+    
     id_b2 := IdentityMorphism( cat, b2 );
     
     coproduct_on_objects_coexp_a1_b1_coexp_a2_b2 :=
@@ -463,7 +463,7 @@ AddDerivationToCAP( CocartesianDualityCoproductCompatibilityMorphismWithGivenObj
                     
   function( cat, s, a, b, r )
     local morphism, unit, coproduct_on_a_and_b;
-
+    
     #         (a ⊔ b)_v
     #            |
     #            V
@@ -499,7 +499,7 @@ AddDerivationToCAP( CocartesianDualityCoproductCompatibilityMorphismWithGivenObj
                 ] );
 
     return morphism;
-
+    
 end : CategoryFilter := IsCocartesianCoclosedCategory );
 
 ##
@@ -514,7 +514,7 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
                     
   function( cat, a, internal_cohom )
     local unit;
-
+    
     #     Coexp(a, 1)
     #         |
     #         | Coexp((ρ_a)^-1, id_1)
@@ -545,7 +545,7 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,
                     
   function( cat, a, internal_cohom )
     local unit;
-
+    
     # (ρ_a)^-1: a → a ⊔ 1
     #
     # Adjoint( (ρ_a)^-1 ) = ( Coexp(a,1) → a )
@@ -582,7 +582,7 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,
                     
   function( cat, a, internal_cohom )
     local unit;
-
+    
     #       a
     #       |
     #       | cocaev_(a,1)
@@ -628,7 +628,7 @@ AddDerivationToCAP( MorphismFromCoexponentialToCoproductWithGivenObjects,
                     
   function( cat, internal_cohom, a, b, coproduct_object )
     local unit;
-
+    
     #       Coexp(a,b)
     #            |
     #            | Coexp((λ_a)^-1, ρ_b)
@@ -667,7 +667,7 @@ AddDerivationToCAP( CocartesianEvaluationMorphismWithGivenRange,
                       [ CoexponentialOnObjects, 1 ] ],
                     
   function( cat, a, b, coproduct_object )
-
+    
     # Adjoint( id_Coexp(a,b): Coexp(a,b) → Coexp(a,b) ) = ( a → Coexp(a,b) ⊔ b )
     
     return CoexponentialToCoproductAdjunctionMap( cat,
@@ -684,7 +684,7 @@ AddDerivationToCAP( CocartesianCoevaluationMorphismWithGivenSource,
                       [ Coproduct, 1 ] ],
                     
   function( cat, a, b, internal_cohom )
-
+    
     # Adjoint( id_(a ⊔ b): a ⊔ b → a ⊔ b ) = ( Coexp(a ⊔ b, b) → a )
     
     return CoproductToCoexponentialAdjunctionMap( cat,
@@ -710,7 +710,7 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local coexp_a_b, coexp_b_c, morphism;
-
+    
     #           a
     #           |
     #           | cocaev_ab
@@ -783,7 +783,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local coexp_a_b, coexp_b_c, morphism;
-
+    
     #             a
     #             |
     #             | cocaev_ab
@@ -833,7 +833,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local braiding;
-
+    
     #       Coexp(a,c)
     #            |
     #            | PreCoCompose
@@ -891,7 +891,7 @@ AddDerivationToCAP( CoexponentialCoproductCompatibilityMorphismWithGivenObjects,
                     
   function( cat, source, list, range )
     local a1, a2, b1, b2, morphism, coexp_a1_b1, coexp_a2_b2, id_b2, coproduct_on_objects_coexp_a1_b1_coexp_a2_b2;
-
+    
     #           a1 ⊔ a2
     #              |
     #              | id_a1 ⊔ cocaev_(a2,b2)
@@ -961,7 +961,7 @@ AddDerivationToCAP( CocartesianDualityCoproductCompatibilityMorphismWithGivenObj
                     
   function( cat, source, a, b, range )
     local morphism, unit, coproduct_on_a_and_b;
-
+    
     #         (a ⊔ b)_v
     #            |
     #            V
@@ -1006,7 +1006,7 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local coexp_a_b, coexp_b_c, morphism;
-
+    
     #            a
     #            |
     #            | cocaev_ab
@@ -1066,7 +1066,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local coexp_a_b, coexp_b_c, morphism;
-
+    
     #             a
     #             |
     #             | cocaev_ab
diff --git a/MonoidalCategories/PackageInfo.g b/MonoidalCategories/PackageInfo.g
index d6a30c178e..1866f3a010 100644
--- a/MonoidalCategories/PackageInfo.g
+++ b/MonoidalCategories/PackageInfo.g
@@ -10,7 +10,7 @@ SetPackageInfo( rec(
 
 PackageName := "MonoidalCategories",
 Subtitle := "Monoidal and monoidal (co)closed categories",
-Version := "2023.07-01",
+Version := "2023.08-01",
 Date := (function ( ) if IsBound( GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE ) then return GAPInfo.SystemEnvironment.GAP_PKG_RELEASE_DATE; else return Concatenation( ~.Version{[ 1 .. 4 ]}, "-", ~.Version{[ 6, 7 ]}, "-01" ); fi; end)( ),
 License := "GPL-2.0-or-later",
 
diff --git a/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi
index e1a9201461..799d36e670 100644
--- a/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi
+++ b/MonoidalCategories/gap/RigidSymmetricClosedMonoidalCategoriesDerivedMethods.gi
@@ -23,7 +23,7 @@ AddDerivationToCAP( InternalHomOnObjects,
                     [ [ IsomorphismFromTensorProductWithDualObjectToInternalHom, 1 ] ],
                     
   function( cat, a, b )
-
+    
     # Range( a^v ⊗ b → Hom(a,b) )
     
     return Range( IsomorphismFromTensorProductWithDualObjectToInternalHom( cat, a, b ) );
@@ -41,7 +41,7 @@ AddDerivationToCAP( InternalHomOnMorphismsWithGivenInternalHoms,
                     
   function( cat, internal_hom_source, alpha, beta, internal_hom_range )
     local dual_alpha;
-
+    
     # alpha: a → a'
     # beta: b → b'
     #
@@ -76,7 +76,7 @@ AddDerivationToCAP( MorphismFromBidualWithGivenBidual,
                       [ MorphismToBidualWithGivenBidual, 1 ] ],
                     
   function( cat, a, bidual )
-
+    
     # Inverse( a → (a^v)^v )
     
     return InverseForMorphisms( cat, MorphismToBidualWithGivenBidual( cat, a, bidual ) );
@@ -90,7 +90,7 @@ AddDerivationToCAP( MorphismToBidualWithGivenBidual,
                       [ MorphismFromBidualWithGivenBidual, 1 ] ],
                     
   function( cat, a, bidual )
-
+    
     # Inverse( (a^v)^v → a )
     
     return InverseForMorphisms( cat, MorphismFromBidualWithGivenBidual( cat, a, bidual ) );
@@ -112,7 +112,7 @@ AddDerivationToCAP( EvaluationMorphismWithGivenSource,
                     
   function( cat, a, b, internal_hom_tensored_a )
     local morphism;
-
+    
     # Hom(a,b) ⊗ a
     #      |
     #      | Isomorphism ⊗ id_a
@@ -170,7 +170,7 @@ AddDerivationToCAP( EvaluationMorphismWithGivenSource,
                     
   function( cat, a, b, internal_hom_tensored_a )
     local morphism;
-
+    
     # Hom(a,b) ⊗ a
     #      |
     #      | Isomorphism ⊗ id_a
@@ -200,7 +200,7 @@ AddDerivationToCAP( EvaluationMorphismWithGivenSource,
                 ] );
                     
     return morphism;
-      
+    
 end : CategoryFilter := cat -> HasIsRigidSymmetricClosedMonoidalCategory( cat ) and IsRigidSymmetricClosedMonoidalCategory( cat ) and HasIsStrictMonoidalCategory( cat ) and IsStrictMonoidalCategory( cat ) );
 
 ##
@@ -219,7 +219,7 @@ AddDerivationToCAP( CoevaluationMorphismWithGivenRange,
                     
   function( cat, a, b, internal_hom )
     local morphism, dual_b, id_a;
-
+    
     #      a
     #      |
     #      | (λ_a)^-1
@@ -290,7 +290,7 @@ AddDerivationToCAP( CoevaluationMorphismWithGivenRange,
                     
   function( cat, a, b, internal_hom )
     local morphism, dual_b, id_a;
-
+    
     # 1 ⊗ a
     #   |
     #   | coev_b ⊗ id_a
@@ -439,7 +439,7 @@ AddDerivationToCAP( CoevaluationForDualWithGivenTensorProduct,
                     
   function( cat, unit, a, tensor_object )
     local morphism;
-
+    
     #    1
     #    |
     #    | LambdaIntro( id_a )
@@ -476,7 +476,7 @@ AddDerivationToCAP( TraceMap,
                     
   function( cat, alpha )
     local result_morphism, a;
-
+    
     # alpha: a → a
     #
     #    1
@@ -524,7 +524,7 @@ AddDerivationToCAP( TensorProductInternalHomCompatibilityMorphismInverseWithGive
                       [ TensorProductInternalHomCompatibilityMorphismWithGivenObjects, 1 ] ],
                     
   function( cat, source, list, range )
-
+    
     # Inverse( Hom(a,a') ⊗ Hom(b,b') → Hom(a ⊗ b, a' ⊗ b') )
     
     return InverseForMorphisms( cat, TensorProductInternalHomCompatibilityMorphismWithGivenObjects( cat, range, list, source ) );
diff --git a/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
index d73e2bdcdb..28b0cb5fcd 100644
--- a/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
+++ b/MonoidalCategories/gap/RigidSymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
@@ -10,7 +10,7 @@ AddDerivationToCAP( InternalCoHomOnObjects,
                     [ [ IsomorphismFromInternalCoHomToTensorProductWithCoDualObject, 1 ] ],
                     
   function( cat, a, b )
-
+    
     # Source( Cohom(a,b) → b_v ⊗ a )
     
     return Source( IsomorphismFromInternalCoHomToTensorProductWithCoDualObject( cat, a, b ) );
@@ -23,7 +23,7 @@ AddDerivationToCAP( InternalCoHomOnObjects,
                     [ [ IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom, 1 ] ],
                     
   function( cat, a, b )
-
+    
     # Range( b_v ⊗ a → Cohom(a,b) )
     
     return Range( IsomorphismFromTensorProductWithCoDualObjectToInternalCoHom( cat, b, a ) );
@@ -41,7 +41,7 @@ AddDerivationToCAP( InternalCoHomOnMorphismsWithGivenInternalCoHoms,
                     
   function( cat, internal_cohom_source, alpha, beta, internal_cohom_range )
     local codual_beta;
-
+    
     # alpha: a → a'
     # beta: b → b'
     #
@@ -76,7 +76,7 @@ AddDerivationToCAP( MorphismToCoBidualWithGivenCoBidual,
                       [ MorphismFromCoBidualWithGivenCoBidual, 1 ] ],
                     
   function( cat, a, cobidual )
-
+    
     # Inverse( (a_v)_v → a )
     
     return InverseForMorphisms( cat, MorphismFromCoBidualWithGivenCoBidual( cat, a, cobidual ) );
@@ -90,7 +90,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                       [ MorphismToCoBidualWithGivenCoBidual, 1 ] ],
                     
   function( cat, a, cobidual )
-
+    
     # Inverse( a → (a_v)_v )
     
     return InverseForMorphisms( cat, MorphismToCoBidualWithGivenCoBidual( cat, a, cobidual ) );
@@ -112,7 +112,7 @@ AddDerivationToCAP( CoclosedEvaluationMorphismWithGivenRange,
                     
   function( cat, a, b, internal_cohom_tensored_b )
     local morphism;
-
+    
     #      a
     #      |
     #      | (ρ_a)^-1
@@ -170,7 +170,7 @@ AddDerivationToCAP( CoclosedEvaluationMorphismWithGivenRange,
                     
   function( cat, a, b, internal_cohom_tensored_b )
     local morphism;
-
+    
     #    a ⊗ 1
     #      |
     #      | id_a ⊗ coclev_b
@@ -200,7 +200,7 @@ AddDerivationToCAP( CoclosedEvaluationMorphismWithGivenRange,
                 ] );
                     
     return morphism;
-      
+    
 end : CategoryFilter := cat -> HasIsRigidSymmetricCoclosedMonoidalCategory( cat ) and IsRigidSymmetricCoclosedMonoidalCategory( cat ) and HasIsStrictMonoidalCategory( cat ) and IsStrictMonoidalCategory( cat ) );
 
 ##
@@ -219,7 +219,7 @@ AddDerivationToCAP( CoclosedCoevaluationMorphismWithGivenSource,
                     
   function( cat, a, b, internal_cohom )
     local morphism, codual_b, id_a;
-
+    
     # Cohom(a ⊗ b, b)
     #       |
     #       | Isomorphism
@@ -290,7 +290,7 @@ AddDerivationToCAP( CoclosedCoevaluationMorphismWithGivenSource,
                     
   function( cat, a, b, internal_cohom )
     local morphism, codual_b, id_a;
-
+    
     # Cohom(a ⊗ b, b)
     #       |
     #       | Isomorphism
@@ -391,7 +391,7 @@ AddDerivationToCAP( CoclosedCoevaluationForCoDualWithGivenTensorProduct,
                     
   function( cat, tensor_object, a, unit )
     local morphism;
-
+    
     # a ⊗ a_v
     #    |
     #    | B_( a, a_v )
@@ -428,7 +428,7 @@ AddDerivationToCAP( CoTraceMap,
                     
   function( cat, alpha )
     local a;
-
+    
     # alpha: a → a
     #
     #    1
@@ -474,7 +474,7 @@ AddDerivationToCAP( InternalCoHomTensorProductCompatibilityMorphismInverseWithGi
                       [ InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects, 1 ] ],
                     
   function( cat, source, list, range )
-
+    
     # Inverse( Cohom( a ⊗ a', b ⊗ b') → Cohom(a,b) ⊗ Cohom(a',b') )
     
     return InverseForMorphisms( cat, InternalCoHomTensorProductCompatibilityMorphismWithGivenObjects( cat, range, list, source ) );
diff --git a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi
index c435994f9d..e3e4920dd8 100644
--- a/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi
+++ b/MonoidalCategories/gap/SymmetricClosedMonoidalCategoriesDerivedMethods.gi
@@ -155,7 +155,7 @@ AddDerivationToCAP( MorphismToBidualWithGivenBidual,
                     
   function( cat, a, avv )
     local morphism, av, tensor_unit;
-
+    
     #        a
     #        |
     #        | coev_(a,a^v)
@@ -227,7 +227,7 @@ AddDerivationToCAP( DualOnMorphismsWithGivenDuals,
                       [ IsomorphismFromInternalHomIntoTensorUnitToDualObject, 1 ] ],
                     
   function( cat, s, alpha, r )
-
+    
     # alpha: a → b
     #
     #   b^v
@@ -380,7 +380,7 @@ AddDerivationToCAP( TensorProductInternalHomCompatibilityMorphismWithGivenObject
     #
     #
     # Adjoint[ (Hom(a1,b1) ⊗ Hom(a2,b2)) ⊗ (a1 ⊗ a2) → b1 ⊗ b2 ] = [ Hom(a1,b1) ⊗ Hom(a2,b2) → Hom(a1 ⊗ a2, b1 ⊗ b2) ]
-
+    
     a1 := list[1];
     b1 := list[2];
     a2 := list[3];
@@ -450,7 +450,7 @@ AddDerivationToCAP( TensorProductDualityCompatibilityMorphismWithGivenObjects,
                     
   function( cat, s, a, b, r )
     local morphism, unit, tensor_product_on_a_and_b;
-
+    
     #      a^v ⊗ b^v
     #          |
     #          v
@@ -532,7 +532,7 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalHomWithGivenInternalHom,
                     
   function( cat, a, internal_hom )
     local unit;
-
+    
     # ρ_a: a ⊗ 1 → a
     #
     # Adjoint( ρ_a ) = ( a → Hom(1,a) )
@@ -569,7 +569,7 @@ AddDerivationToCAP( IsomorphismFromInternalHomToObjectWithGivenInternalHom,
                     
   function( cat, a, internal_hom )
     local unit;
-
+    
     #  Hom(1,a)
     #      |
     #      | ( ρ_Hom(1,a) )^-1
@@ -615,7 +615,7 @@ AddDerivationToCAP( MorphismFromTensorProductToInternalHomWithGivenObjects,
                     
   function( cat, tensor_object, a, b, internal_hom )
     local unit;
-
+    
     #      a^v ⊗ b
     #          |
     #          v
@@ -628,7 +628,7 @@ AddDerivationToCAP( MorphismFromTensorProductToInternalHomWithGivenObjects,
     #          | Hom((ρ_a)^-1, λ_b)
     #          v
     #       Hom(a,b)
-
+    
     unit := TensorUnit( cat );
     
     return PreComposeList( cat, [
@@ -696,7 +696,7 @@ AddDerivationToCAP( MonoidalPreComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local hom_a_b, hom_b_c, morphism;
-
+    
     # (Hom(a,b) ⊗ Hom(b,c)) ⊗ a
     #           |
     #           | α_( ( Hom(a,b), Hom(b,c) ), a)
@@ -769,7 +769,7 @@ AddDerivationToCAP( MonoidalPostComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local hom_a_b, hom_b_c, morphism;
-
+    
     # (Hom(b,c) ⊗ Hom(a,b)) ⊗ a
     #            |
     #            | α_( ( Hom(b,c), Hom(a,b) ), c )
@@ -876,7 +876,7 @@ AddDerivationToCAP( TensorProductInternalHomCompatibilityMorphismWithGivenObject
                     
   function( cat, source, list, range )
     local a1, b1, a2, b2, morphism, int_hom_a1_b1, int_hom_a2_b2, id_a2, tensor_product_on_objects_int_hom_a1_b1_int_hom_a2_b2;
-
+    
     # Hom(a1,b1) ⊗ Hom(a2,b2) ⊗ a1 ⊗ a2
     #                 |
     #                 | id_Hom(a1,b1) ⊗ B_( Hom(a2,b2), a1 ) ⊗ id_a2
@@ -946,7 +946,7 @@ AddDerivationToCAP( TensorProductDualityCompatibilityMorphismWithGivenObjects,
                     
   function( cat, source, a, b, range )
     local morphism, unit, tensor_product_on_a_and_b;
-
+    
     #      a^v ⊗ b^v
     #          |
     #          v
@@ -1051,7 +1051,7 @@ AddDerivationToCAP( MonoidalPostComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local hom_a_b, hom_b_c, morphism;
-
+    
     # Hom(b,c) ⊗ Hom(a,b) ⊗ a
     #            |
     #            | id_Hom(b,c) ⊗ ev_ab
diff --git a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
index e50d82c4ac..7759daae18 100644
--- a/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
+++ b/MonoidalCategories/gap/SymmetricCoclosedMonoidalCategoriesDerivedMethods.gi
@@ -72,7 +72,7 @@ AddDerivationToCAP( InternalCoHomToTensorProductAdjunctionMap,
                       [ IdentityMorphism, 1 ] ],
                     
   function( cat, a, b, f )
-
+    
     # f: Cohom(a,b) → c
     #
     #        a
@@ -99,7 +99,7 @@ AddDerivationToCAP( UniversalPropertyOfCoDual,
                       [ TensorProductToInternalCoHomAdjunctionMap, 1 ] ],
                     
   function( cat, t, a, alpha )
-
+    
     # alpha: 1 → t ⊗ a
     #
     # a_v → ( Cohom(1,a) → t ) = Adjoint( alpha )
@@ -121,7 +121,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                     
   function( cat, a, avv )
     local alpha;
-
+    
     #    1
     #    |
     #    | coclev_a
@@ -157,7 +157,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                     
   function( cat, a, avv )
     local morphism, av, tensor_unit;
-
+    
     #     Cohom(1, a_v)
     #          |
     #          | Cohom( coclev_(1,a), id_(a_v) )
@@ -189,7 +189,7 @@ AddDerivationToCAP( MorphismFromCoBidualWithGivenCoBidual,
                 ] );
     
     return morphism;
-
+    
 end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );
 
 ##
@@ -198,7 +198,7 @@ AddDerivationToCAP( CoDualOnObjects,
                     [ [ IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit, 1 ] ],
                     
   function( cat, a )
-
+    
     # Source( a_v → Cohom(1,a) )
     
     return Source( IsomorphismFromCoDualObjectToInternalCoHomFromTensorUnit( cat, a ) );
@@ -211,7 +211,7 @@ AddDerivationToCAP( CoDualOnObjects,
                     [ [ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject, 1 ] ],
                     
   function( cat, a )
-
+    
     # Range( Cohom(1,a) → a_v )
     
     return Range( IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject( cat, a ) );
@@ -230,7 +230,7 @@ AddDerivationToCAP( CoDualOnMorphismsWithGivenCoDuals,
                     
   function( cat, s, alpha, r )
     local result_morphism;
-
+    
     # alpha: a → b
     #
     #    b_v
@@ -266,9 +266,9 @@ AddDerivationToCAP( CoclosedEvaluationForCoDualWithGivenTensorProduct,
                       [ IsomorphismFromInternalCoHomFromTensorUnitToCoDualObject, 1 ] ],
                     
   function( cat, s, a, r )
-
+    
     # s := 1
-
+    
     # Adjoint( Cohom(1,a) → a_v ) = ( 1 → a_v ⊗ a )
 
     return InternalCoHomToTensorProductAdjunctionMap( cat,
@@ -288,7 +288,7 @@ AddDerivationToCAP( CoLambdaIntroduction,
                     
   function( cat, alpha )
     local result_morphism, range;
-
+    
     #   a
     #   |
     #   | alpha
@@ -321,7 +321,7 @@ AddDerivationToCAP( CoLambdaElimination,
                     
   function( cat, a, b, alpha )
     local result_morphism;
-
+    
     # alpha: Cohom(a,b) → 1
     # Adjoint( alpha ) = ( a → 1 ⊗ b )
     #
@@ -357,7 +357,7 @@ AddDerivationToCAP( InternalCoHomTensorProductCompatibilityMorphismWithGivenObje
                     
   function( cat, source, list, range )
     local a1, a2, b1, b2, morphism, int_cohom_a1_b1, int_cohom_a2_b2, id_b2, tensor_product_on_objects_int_cohom_a1_b1_int_cohom_a2_b2;
-
+    
     #                   a1 ⊗ a2
     #                      |
     #                      | id_a1 ⊗ coclev_(a2,b2)
@@ -399,7 +399,7 @@ AddDerivationToCAP( InternalCoHomTensorProductCompatibilityMorphismWithGivenObje
     int_cohom_a1_b1 := InternalCoHomOnObjects( cat, a1, b1 );
     
     int_cohom_a2_b2 := InternalCoHomOnObjects( cat, a2, b2 );
-
+    
     id_b2 := IdentityMorphism( cat, b2 );
     
     tensor_product_on_objects_int_cohom_a1_b1_int_cohom_a2_b2 :=
@@ -460,7 +460,7 @@ AddDerivationToCAP( CoDualityTensorProductCompatibilityMorphismWithGivenObjects,
                     
   function( cat, s, a, b, r )
     local morphism, unit, tensor_product_on_a_and_b;
-
+    
     #         (a ⊗ b)_v
     #            |
     #            V
@@ -496,7 +496,7 @@ AddDerivationToCAP( CoDualityTensorProductCompatibilityMorphismWithGivenObjects,
                 ] );
 
     return morphism;
-
+    
 end : CategoryFilter := IsSymmetricCoclosedMonoidalCategory );
 
 ##
@@ -511,7 +511,7 @@ AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom,
                     
   function( cat, a, internal_cohom )
     local unit;
-
+    
     #     Cohom(a, 1)
     #         |
     #         | Cohom((ρ_a)^-1, id_1)
@@ -542,7 +542,7 @@ AddDerivationToCAP( IsomorphismFromInternalCoHomToObjectWithGivenInternalCoHom,
                     
   function( cat, a, internal_cohom )
     local unit;
-
+    
     # (ρ_a)^-1: a → a ⊗ 1
     #
     # Adjoint( (ρ_a)^-1 ) = ( Cohom(a,1) → a )
@@ -579,7 +579,7 @@ AddDerivationToCAP( IsomorphismFromObjectToInternalCoHomWithGivenInternalCoHom,
                     
   function( cat, a, internal_cohom )
     local unit;
-
+    
     #       a
     #       |
     #       | coclev_(a,1)
@@ -625,7 +625,7 @@ AddDerivationToCAP( MorphismFromInternalCoHomToTensorProductWithGivenObjects,
                     
   function( cat, internal_cohom, a, b, tensor_object )
     local unit;
-
+    
     #       Cohom(a,b)
     #            |
     #            | Cohom((λ_a)^-1, ρ_b)
@@ -664,7 +664,7 @@ AddDerivationToCAP( CoclosedEvaluationMorphismWithGivenRange,
                       [ InternalCoHomOnObjects, 1 ] ],
                     
   function( cat, a, b, tensor_object )
-
+    
     # Adjoint( id_Cohom(a,b): Cohom(a,b) → Cohom(a,b) ) = ( a → Cohom(a,b) ⊗ b )
     
     return InternalCoHomToTensorProductAdjunctionMap( cat,
@@ -681,7 +681,7 @@ AddDerivationToCAP( CoclosedCoevaluationMorphismWithGivenSource,
                       [ TensorProductOnObjects, 1 ] ],
                     
   function( cat, a, b, internal_cohom )
-
+    
     # Adjoint( id_(a ⊗ b): a ⊗ b → a ⊗ b ) = ( Cohom(a ⊗ b, b) → a )
     
     return TensorProductToInternalCoHomAdjunctionMap( cat,
@@ -707,7 +707,7 @@ AddDerivationToCAP( MonoidalPreCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local cohom_a_b, cohom_b_c, morphism;
-
+    
     #           a
     #           |
     #           | coclev_ab
@@ -780,7 +780,7 @@ AddDerivationToCAP( MonoidalPostCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local cohom_a_b, cohom_b_c, morphism;
-
+    
     #             a
     #             |
     #             | coclev_ab
@@ -830,7 +830,7 @@ AddDerivationToCAP( MonoidalPostCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local braiding;
-
+    
     #       Cohom(a,c)
     #            |
     #            | PreCoCompose
@@ -888,7 +888,7 @@ AddDerivationToCAP( InternalCoHomTensorProductCompatibilityMorphismWithGivenObje
                     
   function( cat, source, list, range )
     local a1, a2, b1, b2, morphism, int_cohom_a1_b1, int_cohom_a2_b2, id_b2, tensor_product_on_objects_int_cohom_a1_b1_int_cohom_a2_b2;
-
+    
     #           a1 ⊗ a2
     #              |
     #              | id_a1 ⊗ coclev_(a2,b2)
@@ -958,7 +958,7 @@ AddDerivationToCAP( CoDualityTensorProductCompatibilityMorphismWithGivenObjects,
                     
   function( cat, source, a, b, range )
     local morphism, unit, tensor_product_on_a_and_b;
-
+    
     #         (a ⊗ b)_v
     #            |
     #            V
@@ -1003,7 +1003,7 @@ AddDerivationToCAP( MonoidalPreCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local cohom_a_b, cohom_b_c, morphism;
-
+    
     #            a
     #            |
     #            | coclev_ab
@@ -1063,7 +1063,7 @@ AddDerivationToCAP( MonoidalPostCoComposeMorphismWithGivenObjects,
                     
   function( cat, source, a, b, c, range )
     local cohom_a_b, cohom_b_c, morphism;
-
+    
     #             a
     #             |
     #             | coclev_ab