Skip to content

Commit

Permalink
whitespaces
Browse files Browse the repository at this point in the history
  • Loading branch information
mohamed-barakat committed Aug 14, 2023
1 parent f580a68 commit b60f736
Show file tree
Hide file tree
Showing 9 changed files with 112 additions and 112 deletions.
2 changes: 1 addition & 1 deletion CartesianCategories/PackageInfo.g
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
2 changes: 1 addition & 1 deletion CartesianCategories/gap/AUTOGENERATED_FROM.md
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,7 @@ AddDerivationToCAP( MorphismToCartesianBidualWithGivenCartesianBidual,

function( cat, a, avv )
local morphism, av, tensor_unit;

# a
# |
# | coev_(a,a^v)
Expand Down Expand Up @@ -230,7 +230,7 @@ AddDerivationToCAP( CartesianDualOnMorphismsWithGivenCartesianDuals,
[ IsomorphismFromExponentialIntoTerminalObjectToCartesianDualObject, 1 ] ],

function( cat, s, alpha, r )

# alpha: a → b
#
# b^v
Expand Down Expand Up @@ -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];
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -535,7 +535,7 @@ AddDerivationToCAP( IsomorphismFromObjectToExponentialWithGivenExponential,

function( cat, a, internal_hom )
local unit;

# ρ_a: a × 1 → a
#
# Adjoint( ρ_a ) = ( a → Exp(1,a) )
Expand Down Expand Up @@ -572,7 +572,7 @@ AddDerivationToCAP( IsomorphismFromExponentialToObjectWithGivenExponential,

function( cat, a, internal_hom )
local unit;

# Exp(1,a)
# |
# | ( ρ_Exp(1,a) )^-1
Expand Down Expand Up @@ -618,7 +618,7 @@ AddDerivationToCAP( MorphismFromDirectProductToExponentialWithGivenObjects,

function( cat, direct_product_object, a, b, internal_hom )
local unit;

# a^v × b
# |
# v
Expand All @@ -631,7 +631,7 @@ AddDerivationToCAP( MorphismFromDirectProductToExponentialWithGivenObjects,
# | Exp((ρ_a)^-1, λ_b)
# v
# Exp(a,b)

unit := TerminalObject( cat );

return PreComposeList( cat, [
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 )
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ AddDerivationToCAP( CoexponentialToCoproductAdjunctionMap,
[ IdentityMorphism, 1 ] ],

function( cat, a, b, f )

# f: Coexp(a,b) → c
#
# a
Expand All @@ -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 )
Expand All @@ -124,7 +124,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,

function( cat, a, avv )
local alpha;

# 1
# |
# | cocaev_a
Expand Down Expand Up @@ -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) )
Expand Down Expand Up @@ -192,7 +192,7 @@ AddDerivationToCAP( MorphismFromCocartesianBidualWithGivenCocartesianBidual,
] );

return morphism;

end : CategoryFilter := IsCocartesianCoclosedCategory );

##
Expand All @@ -201,7 +201,7 @@ AddDerivationToCAP( CocartesianDualOnObjects,
[ [ IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject, 1 ] ],

function( cat, a )

# Source( a_v → Coexp(1,a) )

return Source( IsomorphismFromCocartesianDualObjectToCoexponentialFromInitialObject( cat, a ) );
Expand All @@ -214,7 +214,7 @@ AddDerivationToCAP( CocartesianDualOnObjects,
[ [ IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject, 1 ] ],

function( cat, a )

# Range( Coexp(1,a) → a_v )

return Range( IsomorphismFromCoexponentialFromInitialObjectToCocartesianDualObject( cat, a ) );
Expand All @@ -233,7 +233,7 @@ AddDerivationToCAP( CocartesianDualOnMorphismsWithGivenCocartesianDuals,

function( cat, s, alpha, r )
local result_morphism;

# alpha: a → b
#
# b_v
Expand Down Expand Up @@ -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,
Expand All @@ -291,7 +291,7 @@ AddDerivationToCAP( CocartesianLambdaIntroduction,

function( cat, alpha )
local result_morphism, range;

# a
# |
# | alpha
Expand Down Expand Up @@ -324,7 +324,7 @@ AddDerivationToCAP( CocartesianLambdaElimination,

function( cat, a, b, alpha )
local result_morphism;

# alpha: Coexp(a,b) → 1
# Adjoint( alpha ) = ( a → 1 ⊔ b )
#
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 :=
Expand Down Expand Up @@ -463,7 +463,7 @@ AddDerivationToCAP( CocartesianDualityCoproductCompatibilityMorphismWithGivenObj

function( cat, s, a, b, r )
local morphism, unit, coproduct_on_a_and_b;

# (a ⊔ b)_v
# |
# V
Expand Down Expand Up @@ -499,7 +499,7 @@ AddDerivationToCAP( CocartesianDualityCoproductCompatibilityMorphismWithGivenObj
] );

return morphism;

end : CategoryFilter := IsCocartesianCoclosedCategory );

##
Expand All @@ -514,7 +514,7 @@ AddDerivationToCAP( IsomorphismFromCoexponentialToObjectWithGivenCoexponential,

function( cat, a, internal_cohom )
local unit;

# Coexp(a, 1)
# |
# | Coexp((ρ_a)^-1, id_1)
Expand Down Expand Up @@ -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 )
Expand Down Expand Up @@ -582,7 +582,7 @@ AddDerivationToCAP( IsomorphismFromObjectToCoexponentialWithGivenCoexponential,

function( cat, a, internal_cohom )
local unit;

# a
# |
# | cocaev_(a,1)
Expand Down Expand Up @@ -628,7 +628,7 @@ AddDerivationToCAP( MorphismFromCoexponentialToCoproductWithGivenObjects,

function( cat, internal_cohom, a, b, coproduct_object )
local unit;

# Coexp(a,b)
# |
# | Coexp((λ_a)^-1, ρ_b)
Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand All @@ -710,7 +710,7 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,

function( cat, source, a, b, c, range )
local coexp_a_b, coexp_b_c, morphism;

# a
# |
# | cocaev_ab
Expand Down Expand Up @@ -783,7 +783,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,

function( cat, source, a, b, c, range )
local coexp_a_b, coexp_b_c, morphism;

# a
# |
# | cocaev_ab
Expand Down Expand Up @@ -833,7 +833,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,

function( cat, source, a, b, c, range )
local braiding;

# Coexp(a,c)
# |
# | PreCoCompose
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -961,7 +961,7 @@ AddDerivationToCAP( CocartesianDualityCoproductCompatibilityMorphismWithGivenObj

function( cat, source, a, b, range )
local morphism, unit, coproduct_on_a_and_b;

# (a ⊔ b)_v
# |
# V
Expand Down Expand Up @@ -1006,7 +1006,7 @@ AddDerivationToCAP( CocartesianPreCoComposeMorphismWithGivenObjects,

function( cat, source, a, b, c, range )
local coexp_a_b, coexp_b_c, morphism;

# a
# |
# | cocaev_ab
Expand Down Expand Up @@ -1066,7 +1066,7 @@ AddDerivationToCAP( CocartesianPostCoComposeMorphismWithGivenObjects,

function( cat, source, a, b, c, range )
local coexp_a_b, coexp_b_c, morphism;

# a
# |
# | cocaev_ab
Expand Down
2 changes: 1 addition & 1 deletion MonoidalCategories/PackageInfo.g
Original file line number Diff line number Diff line change
Expand Up @@ -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",

Expand Down
Loading

0 comments on commit b60f736

Please sign in to comment.