[MathJax off]

1 Toposes

An elementary topos is a finite complete, cartesian closed category with a subobject classifier. It follows that an elementary topos is also a finitely cocomplete Heyting category.

The doctrines of (co)cartesian (co)closed categories and their variations are implemented in the CAP-based package CartesianCategories.

1.1 Exact cover with global elements

1.1-1 ExactCoverWithGlobalElements

Returns: a list of morphisms in \(\mathrm{Hom}( t, a )\)

The argument is an object a of a category \(\mathbf{C}\) which is enriched over itself, i.e., \(\mathbf{C}\) = RangeCategoryOfHomomorphismStructure( \(\mathbf{C}\) ). The output is a list \(D\) of global elements of a (i.e., morphisms from the distinguished object \(t :=\)DistinguishedObjectOfHomomorphismStructure( \(\mathbf{C}\) ) to a), such that UniversalMorphismFromCoproduct(a, \(D\)) is an isomorphism.

1.1-2 IndexOfNonliftableMorphismFromDistinguishedObject

Returns: a morphism in \(\mathrm{Hom}( t, \mathrm{Target}( \iota ) )\)

The argument is a nonepimorphic monomorphism iota of a category \(\mathbf{C}\) which is enriched over itself, i.e., \(\mathbf{C}\) = RangeCategoryOfHomomorphismStructure( \(\mathbf{C}\) ). The output is a positive integer, namely the position of a morphism \(\tau\) in the list ExactCoverWithGlobalElements( Range( iota ) ) of morphisms from the distinguished object \(t :=\)DistinguishedObjectOfHomomorphismStructure( \(\mathbf{C}\) ) to Range( iota ), such that IsLiftableAlongMonomorphism( iota, \(\tau\) ) = false.

1.1-3 NonliftableMorphismFromDistinguishedObject

Returns: a morphism in \(\mathrm{Hom}( t, \mathrm{Target}( \iota ) )\)

The argument is a nonepimorphic monomorphism iota of a category \(\mathbf{C}\) which is enriched over itself, i.e., \(\mathbf{C}\) = RangeCategoryOfHomomorphismStructure( \(\mathbf{C}\) ). The output is a morphism \(\tau\) from the distinguished object \(t :=\)DistinguishedObjectOfHomomorphismStructure( \(\mathbf{C}\) ) to Range( iota ), such that IsLiftableAlongMonomorphism( iota, \(\tau\) ) = false.

1.2 Subobject classifier

1.2-1 IsElementaryTopos

Returns: true or false

The property of the category C being an elementary topos.

A subobject classifier consists of three parts:

• an object \(\Omega\),

• a function \(\mathrm{true}\) providing a morphism \(\mathrm{true}: 1 \rightarrow \Omega\),

• a function \(\chi\) mapping each monomorphism \(i : A \rightarrow S\) to a morphism \(\chi_i : S \to \Omega\).

The triple \((\Omega,\mathrm{true},\chi)\) is called a subobject classifier if for each monomorphism \(i : A \to S\), the morphism \(\chi_i : S \to \Omega\) is the unique morphism such that \(\chi_i \circ i = \mathrm{true} \circ \ast\) determine a pullback diagram.

1.2-2 SubobjectClassifier

Returns: an object

The argument is a category \(C\). The output is the subobject classifier object \(\Omega\) of \(C\).

1.2-3 CartesianSquareOfSubobjectClassifier

Returns: an object

The argument is a category \(C\). The output is the cartesian square of the subobject classifier object \Omega of \(C\).

1.2-4 ClassifyingMorphismOfSubobject

Returns: a morphism in \(\mathrm{Hom}( \mathrm{Target}(m), \mathrm{SubobjectClassifier} )\)

The argument is a monomorphism \(m : A \rightarrow S\). The output is its classifying morphism \(\chi_m : S \rightarrow \mathrm{SubobjectClassifier}\).

1.2-5 ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier

Returns: a morphism in \(\mathrm{Hom}( \mathrm{Target}(m), \mathrm{SubobjectClassifier} )\)

The arguments are a monomorphism \(m : A \rightarrow S\) and the subobject classifier \(\Omega\). The output is the classifying morphism of the monomorphism \(\chi_m : S \rightarrow \mathrm{SubobjectClassifier}\).

1.2-6 SubobjectOfClassifyingMorphism

Returns: a monomorphism in \(\mathrm{Hom}( A, S )\)

The argument is a classifying morphism \(\chi : S \rightarrow \Omega\). The output is the subobject monomorphism of the classifying morphism, \(m : A \rightarrow S\).

1.2-7 ListOfSubobjects

Returns: a list of monomorphisms into \(A\).

The argument is an object A. The output is a list of all subobjects of A.

1.3 Truth morphisms

1.3-1 TruthMorphismOfTrue

Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{SubobjectClassifier} )\)

The argument is a category \(C\). The output is the truth morphism \(\mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}\).

1.3-2 TruthMorphismOfTrueWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( T, \Omega )\)

The arguments are the terminal object of the category and the subobject classifier. The output is the truth morphism \(\mathrm{true}: T \rightarrow \Omega\).

1.3-3 TruthMorphismOfFalse

Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{SubobjectClassifier} )\)

The argument is a category \(C\). The output is the truth morphism \(\mathrm{false}: \mathrm{TerminalObject} \rightarrow \mathrm{SubobjectClassifier}\).

1.3-4 TruthMorphismOfFalseWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( T, \Omega )\)

The arguments are the terminal object T of the category and the subobject classifier Omega. The output is the truth morphism \(\mathrm{false}: T \rightarrow \Omega\).

1.3-5 TruthMorphismOfNot

Returns: a morphism in \(\mathrm{Hom}( \mathrm{SubobjectClassifier}, \mathrm{SubobjectClassifier} )\)

The argument is a category \(C\). The output is the truth endomorphism \(\mathrm{not}: \mathrm{SubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).

1.3-6 TruthMorphismOfNotWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( \Omega, \Omega )\)

The arguments are a subobject classifier Omega as first and as second argument. The output is the truth endomorphism \(\mathrm{not}: \Omega \rightarrow \Omega\).

1.3-7 TruthMorphismOfAnd

Returns: a morphism in \(\mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )\)

The argument is a category \(C\). The output is the truth morphism \(\mathrm{and}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).

1.3-8 TruthMorphismOfAndWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( \Omega^{\times 2}, \Omega )\)

The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \(\mathrm{and}: \Omega^{\times 2} \rightarrow \Omega\).

1.3-9 TruthMorphismOfOr

Returns: a morphism in \(\mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )\)

The argument is a category \(C\). The output is the truth morphism \(\mathrm{or}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).

1.3-10 TruthMorphismOfOrWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( \Omega^{\times 2}, \Omega )\)

The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \(\mathrm{or}: \Omega^{\times 2} \rightarrow \Omega\).

1.3-11 TruthMorphismOfImplies

Returns: a morphism in \(\mathrm{Hom}( \mathrm{CartesianSquareOfSubobjectClassifier}, \mathrm{SubobjectClassifier} )\)

The argument is a category \(C\). The output is the truth morphism \(\mathrm{implies}: \mathrm{CartesianSquareOfSubobjectClassifier} \rightarrow \mathrm{SubobjectClassifier}\).

1.3-12 TruthMorphismOfImpliesWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( \Omega^{\times 2}, \Omega )\)

The arguments are the cartesian square Omega^{\times 2} of a subobject classifier Omega of the category and the subobject classifier. The output is the truth morphism \(\mathrm{implies}: \Omega^{\times 2} \rightarrow \Omega\).

1.4 Power object

1.4-1 PowerObject

Returns: an object

The argument is an object a. The output is the power object \(P(a)\) of a.

1.4-2 PowerObjectFunctorial

Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}(b), \mathrm{PowerObject}(a) )\)

The argument is a morphism f\(:a \to b\). The output is the power morphism of \(P(f): P(b) \to P(a)\).

gap> LoadPackage( "FinSetsForCAP" );
true
gap> a := FinSet( 3 );
|3|
gap> b := FinSet( 4 );
|4|
gap> f := MapOfFinSets( a, [ 0, 1, 1 ], b );
|3| → |4|
gap> Pf := PowerObjectFunctorial( f );
|16| → |8|
gap> Display( Pf );
{ 0,..., 15 } ⱶ[ 0, 1, 6, 7, 0, 1, 6, 7, 0, 1, 6, 7, 0, 1, 6, 7 ]→ { 0,..., 7 }

1.4-3 PowerObjectFunctorialWithGivenPowerObjects

Returns: a morphism in \(\mathrm{Hom}( Pb, Pa )\)

The arguments are an object Pb, a morphism \(f:a \to b\), and object Pa, such that Pa\(= P(a)\) and Pb\(= P(b)\). The output is the power morphism of \(P(f): Pb \to Pa\).

1.4-4 PowerObjectRightEvaluationMorphism

Returns: a morphism in \(\mathrm{Hom}( a \times \mathrm{PowerObject}(a), \Omega )\)

The argument is an object a. The output is the power object right evaluation morphism of \(\epsilon_a: a \times P(a) \to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(a).

1.4-5 PowerObjectRightEvaluationMorphismWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( axPa, Omega )\)

The arguments are three objects Pa_xa, a, and Omega, such that axPa\(= a \times P(a)\) and Omega the subobject classifier of CapCategory(a). The output is the power object right evaluation morphism of \(\epsilon_a:\) axPa \(\to\) Omega.

1.4-6 PowerObjectLeftEvaluationMorphism

Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}(a) \times a, \Omega )\)

The argument is an object a. The output is the power object left evaluation morphism of \(\epsilon_a: P(a) \times a \to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(a).

1.4-7 PowerObjectLeftEvaluationMorphismWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( Pa_xa, Omega )\)

The arguments are three objects Pa_xa, a, and Omega, such that Pa_xa\(= P(a) \times a\) and Omega the subobject classifier of CapCategory(a). The output is the power object left evaluation morphism of \(\epsilon_a:\) Pa_xa \(\to\) Omega.

1.4-8 PRightTransposeMorphism

Returns: a morphism in \(\mathrm{Hom}( b, P(a) )\)

The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(f). The output is the \(P\)-right-transpose morphism b \(\to P(a)\), where \(P(a) =\) PowerObject( a ).

1.4-9 PRightTransposeMorphismWithGivenRange

Returns: a morphism in \(\mathrm{Hom}( b, Pa )\)

The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), and an object Pa, where \(\Omega\) is the subobject classifier of CapCategory(f) and Pa = PowerObject( a ). The output is the \(P\)-right-transpose morphism b \(\to\) Pa.

1.4-10 PLeftTransposeMorphism

Returns: a morphism in \(\mathrm{Hom}( a, P(b) )\)

The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), where \(\Omega\) is the subobject classifier of CapCategory(f). The output is the \(P\)-left-transpose morphism a \(\to P(b)\), where \(P(b) =\) PowerObject( b ).

1.4-11 PLeftTransposeMorphismWithGivenRange

Returns: a morphism in \(\mathrm{Hom}( a, Pb )\)

The arguments are two objects a, b, a morphism f: a \(\times\) b \(\to \Omega\), and an object Pb, where \(\Omega\) is the subobject classifier of CapCategory(f) and Pb = PowerObject( b ). The output is the \(P\)-left-transpose morphism a \(\to\) Pb.

1.4-12 UpperSegmentOfRelation

Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{PowerObject}( b ) )\)

The arguments are two objects a, b in a category \(C\) and a monomorphism mu\(: r \hookrightarrow a \times b\) defining a relation on \(a \times b\). The output is the upper segment of the relation which is a morphism \(a \to Pb\) given by the adjunction, where \(Pb\) := PowerObject( b ) is the the power object of b.

1.4-13 UpperSegmentOfRelationWithGivenRange

Returns: a morphism in \(\mathrm{Hom}( a, Pb )\)

The arguments are two objects a, b in a category \(C\), a monomorphism mu\(: r \hookrightarrow a \times b\) defining a relation on \(a \times b\), and the power object Pb := PowerObject( b ) of b. The output is the upper segment of the relation which is a morphism \(a \to Pb\) given by the adjunction.

1.4-14 LowerSegmentOfRelation

Returns: a morphism in \(\mathrm{Hom}( b, \mathrm{PowerObject}( a ) )\)

The arguments are two objects a, b in a category \(C\) and a monomorphism mu\(:r \hookrightarrow a \times b\) defining a relation on \(a \times b\). The output is the lower segment of the relation which is a morphism \(b \to Pa\) given by the adjunction, where \(Pa\) := PowerObject( a ) is the the power object of a.

1.4-15 LowerSegmentOfRelationWithGivenRange

Returns: a morphism in \(\mathrm{Hom}( b, Pa )\)

The arguments are two objects a, b in a category \(C\), a monomorphism mu\(:r \hookrightarrow a \times b\) defining a relation on \(a \times b\), and the power object Pa := PowerObject( a ) of a. The output is the lower segment of the relation which is a morphism \(b \to Pa\) given by the adjunction.

1.4-16 SingletonMorphism

Returns: a morphism in \(\mathrm{Hom}( a, \mathrm{PowerObject}(a) )\)

The argument is an object a. The output is the singleton morphism from a to the power object \(\mathrm{PowerObject}(a)\).

gap> LoadPackage( "FinSetsForCAP" );
true
gap> sFinSets := SkeletalCategoryOfFiniteSets( : no_precompiled_code := true );
SkeletalFinSets
gap> a := BigInt( 3 ) / sFinSets;
|3|
gap> sa := SingletonMorphism( a );
|3| ↪ |8|
gap> Display( sa );
{ 0, 1, 2 } ⱶ[ 1, 2, 4 ]→ { 0,..., 7 }
gap> sa = UpperSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) );
true
gap> sa = LowerSegmentOfRelation( a, a, CartesianDiagonal( a, 2 ) );
true

1.4-17 SingletonMorphismWithGivenPowerObject

Returns: a morphism in \(\mathrm{Hom}( a, Pa )\)

The arguments are an object a and an object Pa which is equal to the power object \(\mathrm{PowerObject}(a)\). The output is the singleton morphism from a to Pa.

1.4-18 IsomorphismOntoCartesianSquareOfPowerObject

Returns: a morphism in \(\mathrm{Hom}( \mathrm{Exponential}( a, \mathrm{CartesianSquareOfSubobjectClassifier}( C ) ), \mathrm{DirectProduct}( \mathrm{PowerObject}(a), \mathrm{PowerObject}(a) ) )\)

The argument is an object a in a category \(C\). The output is the isomorphism \(\mathrm{Exponential}( a, \mathrm{CartesianSquareOfSubobjectClassifier}( C ) ) \rightarrow \mathrm{DirectProduct}( \mathrm{PowerObject}(a), \mathrm{PowerObject}(a) )\).

gap> LoadPackage( "FinSetsForCAP" );
true
gap> a := FinSet( 2 );
|2|
gap> ia := IsomorphismOntoCartesianSquareOfPowerObject( a );
|16| ⭇ |16|
gap> Display( ia );
{ 0,..., 15 }\
 ⱶ[ 0, 1, 4, 5, 2, 3, 6, 7, 8, 9, 12, 13, 10, 11, 14, 15 ]→ { 0,..., 15 }

1.4-19 IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( Exp\_a\_Omega2, PaxPa )\)

The arguments are an object the exponential Exp_a_Omega2 = Exponential( a, CartesianSquareOfSubobjectClassifier ), an object a in a category \(C\), and the cartesian squre PaxPa of the power object PowerObject( a ). The output is the isomorphism \(Exp\_a\_Omega2 \stackrel{\sim}{\rightarrow} PaxPa\)

1.4-20 IntersectWithPreimagesWithGivenObjects

Returns: a morphism \(\mathrm{Hom}( PAxB, PA )\)

The input is the direct product PAxB = PA \(\times B\), a morphism f: \(A \to B\), and the power object PA = PowerObject(\(A\)). The output is the morphism PAxB \(\rightarrow\) PA, \((T, b) \mapsto T \cap f^{-1}(b)\).

1.4-21 EmbeddingOfRelativePowerObject

Returns: a monomorphism \(\mathrm{Hom}( P_fa, Pa \times b )\)

The input is a morphism f: \(a \to b\). The output is the embedding of the relative power object \(P_fa \hookrightarrow Pa \times b\), where \(Pa\) = PowerObject(\(a\)).

1.4-22 RelativePowerObjectFibrationMorphism

Returns: a monomorphism \(\mathrm{Hom}( P_fa, b )\)

The input is a morphism f: \(a \to b\). The output is the fibration morphism \(P_f: P_fa \rightarrow \times b\), where is \(P_fa\) the relative power object of f.

1.4-23 RelativePowerObjectLeftEvaluationMorphism

Returns: a monomorphism \(\mathrm{Hom}( P_fa \times a, \Omega \times b )\)

The input is a morphism f: \(a \to b\). The output is the evaluation morphism \(P_fa \times a \rightarrow \Omega \times b\), where \(P_fa\) is the relative power object of f.

1.4-24 RightFiberMorphism

Returns: a morphism in \(\mathrm{Hom}( c \times P(b \times c), P(b) )\)

The arguments are two objects b, c. The output is the morphism c \(\times\) PowerObject(b \times c) \(\to\) PowerObject( b ) that for a given relation \(R \subseteq\) b \(\times\) c and an element \(y\) in the base c computes the fiber over \(y\) as subset of b.

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> a := FinSet( 3 );
|3|
gap> b := FinSet( 2 );
|2|
gap> right := RightFiberMorphism( a, b );
|128| → |8|
gap> LoadPackage( "LazyCategories", false );
true
gap> L := LazyCategory( SkeletalFinSets : primitive_operations := true );
LazyCategory( SkeletalFinSets )
gap> lazy_right := RightFiberMorphism( a / L, b / L );
<A morphism in LazyCategory( SkeletalFinSets )>

1.4-25 RightFiberMorphismWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( cxPbxc, Pb )\)

The arguments are four objects cxPbxc, b, c, Pb, where cxPbxc = \(c \times P(b \times c)\) and Pb = PowerObject( b ). The output is the morphism that for a given relation \(R \subseteq\) b \(\times\) c and an element \(y\) in the base c computes the fiber over \(y\) as subset of b.

1.4-26 LeftFiberMorphism

Returns: a morphism in \(\mathrm{Hom}( P(b \times c) \times b, P(c) )\)

The arguments are two objects b, c. The output is the morphism PowerObject(b \times c) \(\times\) b \(\to\) PowerObject( c ) that for a given relation \(R \subseteq\) b \(\times\) c and an element \(x\) in the base b computes the fiber over \(x\) as subset of c.

gap> LoadPackage( "FinSetsForCAP", false );
true
gap> a := FinSet( 2 );
|2|
gap> b := FinSet( 3 );
|3|
gap> left := LeftFiberMorphism( a, b );
|128| → |8|
gap> LoadPackage( "LazyCategories", false );
true
gap> L := LazyCategory( SkeletalFinSets : primitive_operations := true );
LazyCategory( SkeletalFinSets )
gap> lazy_left := LeftFiberMorphism( a / L, b / L );
<A morphism in LazyCategory( SkeletalFinSets )>

1.4-27 LeftFiberMorphismWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( Pbxc_xb, Pc )\)

The arguments are four objects Pbxc_xb, b, c, Pc, where Pbxc_xb = \(P(b \times c) \times b\) and Pc = PowerObject( c ). The output is the morphism that for a given relation \(R \subseteq\) b \(\times\) c and an element \(x\) in the base b computes the fiber over \(x\) as subset of c.

1.4-28 SingletonSupportOfRelationsWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( Pbxc, Pb )\)

Return the morphism that for a given relation \(R \subseteq\) b \(\times\) c computes the subset of b over which \(R\) is a singleton.

1.5 Relative truth morphisms

1.5-1 RelativeTruthMorphismOfTrue

Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{PowerObect}( a ) )\)

The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{true}: \mathrm{TerminalObject} \rightarrow \mathrm{PowerObject}( a )\).

1.5-2 RelativeTruthMorphismOfTrueWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( T, Pa )\)

The arguments are the terminal object of the category \(C\), an object a, and the power object Pa of a. The output is the relative truth morphism \(\mathrm{true}: T \rightarrow Pa\).

1.5-3 RelativeTruthMorphismOfFalse

Returns: a morphism in \(\mathrm{Hom}( \mathrm{TerminalObject}, \mathrm{PowerObect}( a ) )\)

The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{false}: \mathrm{TerminalObject} \rightarrow \mathrm{PowerObject}( a )\).

1.5-4 RelativeTruthMorphismOfFalseWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( T, Pa )\)

The arguments are the terminal object of the category \(C\), an object a, and the power object Pa of a. The output is the relative truth morphism \(\mathrm{false}: T \rightarrow Pa\).

1.5-5 RelativeTruthMorphismOfNot

Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ), \mathrm{PowerObect}( a ) )\)

The argument is an object a in a category \(C\). The output is the relative truth endomorphism \(\mathrm{not}: \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).

1.5-6 RelativeTruthMorphismOfNotWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( Pa, Pa )\)

The arguments are the power object Pa of a, the object a, and Pa. The output is the relative truth endomorphism \(\mathrm{not}: Pa \rightarrow Pa\).

1.5-7 RelativeTruthMorphismOfAnd

Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )\)

The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{and}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).

1.5-8 RelativeTruthMorphismOfAndWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( PaxPa, Pa )\)

The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \(\mathrm{and}: PaxPa \rightarrow Pa\).

1.5-9 RelativeTruthMorphismOfOr

Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )\)

The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{or}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).

1.5-10 RelativeTruthMorphismOfOrWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( PaxPa, Pa )\)

The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \(\mathrm{or}: PaxPa \rightarrow Pa\).

1.5-11 RelativeTruthMorphismOfImplies

Returns: a morphism in \(\mathrm{Hom}( \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ), \mathrm{PowerObject}( a ) )\)

The argument is an object a in a category \(C\). The output is the relative truth morphism \(\mathrm{implies}: \mathrm{PowerObject}( a ) \times \mathrm{PowerObject}( a ) \rightarrow \mathrm{PowerObject}( a )\).

1.5-12 RelativeTruthMorphismOfImpliesWithGivenObjects

Returns: a morphism in \(\mathrm{Hom}( PaxPa, Pa )\)

The arguments are the cartesian square PaxPa of the power object Pa of a, the object a, and Pa. The output is the relative truth morphism \(\mathrm{implies}: PaxPa \rightarrow Pa\).

gap> LoadPackage( "FinSetsForCAP" );
true
gap> sFinSets := SkeletalFinSets;
SkeletalFinSets
gap> t := TerminalObject( sFinSets );
|1|
gap> TruthMorphismOfFalse( sFinSets ) = RelativeTruthMorphismOfFalse( t );
true
gap> TruthMorphismOfTrue( sFinSets ) = RelativeTruthMorphismOfTrue( t );
true
gap> TruthMorphismOfNot( sFinSets ) = RelativeTruthMorphismOfNot( t );
true
gap> TruthMorphismOfAnd( sFinSets ) = RelativeTruthMorphismOfAnd( t );
true
gap> TruthMorphismOfOr( sFinSets ) = RelativeTruthMorphismOfOr( t );
true
gap> TruthMorphismOfImplies( sFinSets ) = RelativeTruthMorphismOfImplies( t );
true
gap> a := FinSet( 2 );
|2|
gap> fPa := RelativeTruthMorphismOfFalse( a );
|1| → |4|
gap> Display( fPa );
{ 0 } ⱶ[ 0 ]→ { 0,..., 3 }
gap> tPa := RelativeTruthMorphismOfTrue( a );
|1| → |4|
gap> Display( tPa );
{ 0 } ⱶ[ 3 ]→ { 0,..., 3 }
gap> nPa := RelativeTruthMorphismOfNot( a );
|4| → |4|
gap> Display( nPa );
{ 0,..., 3 } ⱶ[ 3, 2, 1, 0 ]→ { 0,..., 3 }
gap> aPa := RelativeTruthMorphismOfAnd( a );
|16| → |4|
gap> Display( aPa );
{ 0,..., 15 } ⱶ[ 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 2, 2, 0, 1, 2, 3 ]→ { 0,..., 3 }
gap> oPa := RelativeTruthMorphismOfOr( a );
|16| → |4|
gap> Display( oPa );
{ 0,..., 15 } ⱶ[ 0, 1, 2, 3, 1, 1, 3, 3, 2, 3, 2, 3, 3, 3, 3, 3 ]→ { 0,..., 3 }
gap> iPa := RelativeTruthMorphismOfImplies( a );
|16| → |4|
gap> Display( iPa );
{ 0,..., 15 } ⱶ[ 3, 2, 1, 0, 3, 3, 1, 1, 3, 2, 3, 2, 3, 3, 3, 3 ]→ { 0,..., 3 }

1.6 Heyting algebra of subobjects

1.6-1 PseudoComplementSubobject

Returns: an object

The argument is a monomorphism \(\iota: S \hookrightarrow A\). The output is the pseudo-complement of \(S\) in \(A\), i.e., the pseudo-complement object of \(\iota\).

1.6-2 EmbeddingOfPseudoComplementSubobject

Returns: an object

The argument is a monomorphism \(\iota: S \hookrightarrow A\). The output is the embedding PseudoComplementSubobject(\(\iota\)) \(\hookrightarrow A\) of pseudo-complement object of \(\iota\).

1.6-3 EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement

Returns: an object

The argument is a monomorphism \(\iota: S \hookrightarrow A\) and an object T with IsEqualForObjects(T, PseudoComplementSubobject(\(\iota\))). The output is the embedding of \(\iota:T \hookrightarrow A\) of pseudo-complement object T of \(\iota\).

1.6-4 IntersectionSubobject

Returns: an object

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the intersection of \(S_1\) and \(S_2\), which is naturally isomorphic to the pullback of \(\iota_1\) and \(\iota_2\).

1.6-5 EmbeddingOfIntersectionSubobject

Returns: a monomorphism into \(A\)

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the embedding IntersectionSubobject(\(\iota\)) \(\hookrightarrow A\) of their intersection subobject.

1.6-6 EmbeddingOfIntersectionSubobjectWithGivenIntersection

Returns: a monomorphism in \(\mathrm{Hom}( T, A )\)

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\) and an object T with IsEqualForObjects(T, IntersectionSubobject(iota1, iota2)). The output is the embedding \(T \hookrightarrow A\) of their intersection subobject T.

1.6-7 UnionSubobject

Returns: an object

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the union of \(S_1\) and \(S_2\), which is naturally isomorphic to the image object of the coproduct morphism of \(\iota_1\) and \(\iota_2\).

1.6-8 EmbeddingOfUnionSubobject

Returns: a monomorphism into \(A\)

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the embedding UnionSubobject(iota1, iota2) \(\hookrightarrow A\) of their union subobject.

1.6-9 EmbeddingOfUnionSubobjectWithGivenUnion

Returns: a monomorphism in \(\mathrm{Hom}( U, A )\)

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\) and an object U with IsEqualForObjects(U, UnionSubobject(iota1, iota2)). The output is the embedding \(U \hookrightarrow A\) of their union subobject U.

1.6-10 RelativePseudoComplementSubobject

Returns: an object

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the relative pseudo-complement of \(S_1\) relative to \(S_2\).

1.6-11 EmbeddingOfRelativePseudoComplementSubobject

Returns: a monomorphism into \(A\)

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\). The output is the embedding RelativePseudoComplementSubobject(iota1, iota2) \(\hookrightarrow A\) of their relative pseudo-complement into \(A\).

1.6-12 EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication

Returns: a monomorphism in \(\mathrm{Hom}( I, A )\)

The arguments are two monomorphisms \(\iota_i: S_i \hookrightarrow A\) for \(i=1,2\) and an object I with IsEqualForObjects(I, RelativePseudoComplementSubobject(iota1, iota2)). The output is the embedding \(I \hookrightarrow A\) of their relative pseudo-complement I into \(A\).

1.7 Pushout complements

1.7-1 Example in FinSets

Define two composable monos \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\) in FinSets:

gap> LoadPackage( "FinSetsForCAP" );
true
gap> K := FinSet( [ 2, 3, 5 ] );;
gap> Display( K );
[ 2, 3, 5 ]
gap> L := FinSet( [ 0, 1, 2, 3, 5, 6 ] );;
gap> Display( L );
[ 0, 1, 2, 3, 5, 6 ]
gap> l := EmbeddingOfFinSets( K, L );
<A monomorphism in FinSets>
gap> G := FinSet( [ 0, 1, 2, 3, 4, 5, 6, 10 ] );;
gap> Display( G );
[ 0, 1, 2, 3, 4, 5, 6, 10 ]
gap> m := EmbeddingOfFinSets( L, G );
<A monomorphism in FinSets>

Now we compute the pushout complement \(D \stackrel{c}{\hookrightarrow} G\) of \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\):

gap> HasPushoutComplement( l, m );
true
gap> c := PushoutComplement( l, m );
<A monomorphism in FinSets>
gap> D := Source( c );;
gap> Display( D );
[ 2, 3, 4, 5, 10 ]

1.7-2 Example in SkeletalFinSets

Define two composable monos \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\) in SkeletalFinSets:

gap> LoadPackage( "FinSetsForCAP" );
true
gap> K := FinSet( 3 );
|3|
gap> L := FinSet( 6 );
|6|
gap> l := MapOfFinSets( K, [ 2, 3, 4 ], L );; IsMonomorphism( l );; l;
|3| ↪ |6|
gap> Display( l );
{ 0, 1, 2 } ⱶ[ 2, 3, 4 ]→ { 0,..., 5 }
gap> G := FinSet( 8 );
|8|
gap> Display( G );
{ 0,..., 7 }
gap> m := MapOfFinSets( L, [ 0, 1, 2, 3, 5, 6 ], G );
|6| → |8|
gap> Display( m );
{ 0,..., 5 } ⱶ[ 0, 1, 2, 3, 5, 6 ]→ { 0,..., 7 }

Now we compute the pushout complement \(D \stackrel{c}{\hookrightarrow} G\) of \(K \stackrel{l}{\hookrightarrow} L \stackrel{m}{\hookrightarrow} G\):

gap> HasPushoutComplement( l, m );
true
gap> c := PushoutComplement( l, m );
|5| → |8|
gap> Display( c );
{ 0,..., 4 } ⱶ[ 2, 3, 4, 5, 7 ]→ { 0,..., 7 }

1.7-3 HasPushoutComplement

Returns: a boolean

The arguments are two composable morphisms \(l: K \rightarrow L\), \(m: L \rightarrow G\). The output is true if there exists a morphism \(d: K \rightarrow D\) and a morphism \(g: D \rightarrow G\) such that the four morphisms \(l,d,m,g\) form a pushout diagram, i.e., such that \(m\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 1) and \(g\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 2). Otherwise the output is false.

1.7-4 PushoutComplement

Returns: a morphism

The arguments are two composable morphisms \(l: K \rightarrow L\), \(m: L \rightarrow G\). The output is a morphism \(d: K \rightarrow D\) such that there exists a morphism \(g: D \rightarrow G\) turing the four morphisms \(l,d,m,g\) into a pushout diagram, i.e., such that \(m\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 1) and \(g\)=InjectionOfCofactorOfPushoutWithGivenPushout([\(l,d\)], 2).

1.8 Double-pushout rewriting

1.8-1 DPO

Returns: a pair of morhpisms

Compute the double-pushout of m along the rule given by [ l, r ].

We start by defining a linear rewriting rule as a span of two monos \(L \stackrel{l}{\hookleftarrow} K \stackrel{r}{\hookrightarrow} R\) in FinSets:

gap> LoadPackage( "FinSetsForCAP" );
true
gap> K := FinSet( [ 2, 3, 5 ] );;
gap> Length( K );
3
gap> Display( K );
[ 2, 3, 5 ]
gap> L := FinSet( [ 0, 1, 2, 3, 5, 6 ] );;
gap> Length( L );
6
gap> Display( L );
[ 0, 1, 2, 3, 5, 6 ]
gap> R := FinSet( [ 2, 3, 4, 5, 7 ] );;
gap> Length( R );
5
gap> Display( R );
[ 2, 3, 4, 5, 7 ]
gap> l := EmbeddingOfFinSets( K, L );
<A monomorphism in FinSets>
gap> r := EmbeddingOfFinSets( K, R );
<A monomorphism in FinSets>

Then we define an object within the context of the rule and a matching \(L \stackrel{m}{\hookrightarrow} G\):

gap> G := FinSet( [ 0, 1, 2, 3, 4, 5, 6, 10 ] );;
gap> Length( G );
8
gap> Display( G );
[ 0, 1, 2, 3, 4, 5, 6, 10 ]
gap> m := EmbeddingOfFinSets( L, G );
<A monomorphism in FinSets>

The double-pushout rewriting now applies the linear rule \((l,r)\) to the matriching \(m\):

gap> p := DPO( m, l, r );;
gap> h := p[1];
<A monomorphism in FinSets>
gap> p := p[2];
<A monomorphism in FinSets>
gap> H := Target( p );;
gap> Length( H );
7
gap> Display( H );
[ [ [ 1, 2 ], [ 2, 2 ] ],\
 [ [ 1, 3 ], [ 2, 3 ] ],\
 [ [ 1, 4 ] ],\
 [ [ 1, 5 ], [ 2, 5 ] ],\
 [ [ 1, 10 ] ],\
 [ [ 2, 4 ] ],\
 [ [ 2, 7 ] ] ]

This means

• \(2, 3, 5\) are in \(K\) and hence in both \(G\) and \(R\);

• \(10\) is only in \(G\);

• \(7\) are only in \(R\);

• \(4\) is in \(G\) but it must be duplicated since it is also in \(R\) but not in \(K\).

1.9 Lawvere-Tierney topologies

Compute the Lawvere-Tierney topologies of SkeletalFinSets:

gap> LoadPackage( "FinSetsForCAP" );
true
gap> LTI := LawvereTierneyLocalModalityOperators( SkeletalFinSets );;
gap> Perform( LTI, Display );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }
{ 0, 1 } ⱶ[ 1, 1 ]→ { 0, 1 }
gap> LTS := LawvereTierneySubobjects( SkeletalFinSets );;
gap> Perform( LTS, Display );
{ 0 } ⱶ[ 1 ]→ { 0, 1 }
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }
gap> LTC := LawvereTierneyEmbeddingsOfSubobjectClassifiers( SkeletalFinSets );;
gap> Perform( LTC, Display );
{ 0, 1 } ⱶ[ 0, 1 ]→ { 0, 1 }
{ 0 } ⱶ[ 1 ]→ { 0, 1 }

1.9-1 LawvereTierneyLocalModalityOperators

Returns: a list of endomorphisms in \(\mathrm{Hom}( \mathrm{SubobjectClassifier}( T ), \mathrm{SubobjectClassifier}( T ) )\)

The input is an elementary topos T. The output is the list of Lawvere-Tierney idempotents of the subobject classifier of the topos T.

1.9-2 LawvereTierneySubobjects

Returns: a list of monomorphisms into \(\mathrm{SubobjectClassifier}( T )\)

The input is an elementary topos T. The output is the list of Lawvere-Tierney subobjects of the subobject classifier of the topos T.

1.9-3 LawvereTierneyEmbeddingsOfSubobjectClassifiers

Returns: a list of monomorphisms \(\mathrm{SubobjectClassifier}( T )\)

The input is an elementary topos T. The output is the list of embeddings of the subobject classifiers of full sheaf subtoposes (with respect to the Lawvere-Tierney topologies of the topos T) into the subobject classifier of T.

1.10 Add-methods

1.10-1 AddCartesianSquareOfSubobjectClassifier

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CartesianSquareOfSubobjectClassifier. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{CartesianSquareOfSubobjectClassifier}()\).

1.10-2 AddClassifyingMorphismOfSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ClassifyingMorphismOfSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( alpha ) \mapsto \mathtt{ClassifyingMorphismOfSubobject}(alpha)\).

1.10-3 AddClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( alpha, Omega ) \mapsto \mathtt{ClassifyingMorphismOfSubobjectWithGivenSubobjectClassifier}(alpha, Omega)\).

1.10-4 AddCoproductComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation CoproductComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota ) \mapsto \mathtt{CoproductComplement}(iota)\).

1.10-5 AddDirectProductComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation DirectProductComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( pi ) \mapsto \mathtt{DirectProductComplement}(pi)\).

1.10-6 AddEmbeddingOfIntersectionSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfIntersectionSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfIntersectionSubobject}(iota1, iota2)\).

1.10-7 AddEmbeddingOfIntersectionSubobjectWithGivenIntersection

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfIntersectionSubobjectWithGivenIntersection. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota1, iota2, intersection ) \mapsto \mathtt{EmbeddingOfIntersectionSubobjectWithGivenIntersection}(iota1, iota2, intersection)\).

1.10-8 AddEmbeddingOfPseudoComplementSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfPseudoComplementSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota ) \mapsto \mathtt{EmbeddingOfPseudoComplementSubobject}(iota)\).

1.10-9 AddEmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota, complement ) \mapsto \mathtt{EmbeddingOfPseudoComplementSubobjectWithGivenPseudoComplement}(iota, complement)\).

1.10-10 AddEmbeddingOfRelativePseudoComplementSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfRelativePseudoComplementSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfRelativePseudoComplementSubobject}(iota1, iota2)\).

1.10-11 AddEmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota1, iota2, implication ) \mapsto \mathtt{EmbeddingOfRelativePseudoComplementSubobjectWithGivenImplication}(iota1, iota2, implication)\).

1.10-12 AddEmbeddingOfUnionSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfUnionSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota1, iota2 ) \mapsto \mathtt{EmbeddingOfUnionSubobject}(iota1, iota2)\).

1.10-13 AddEmbeddingOfUnionSubobjectWithGivenUnion

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation EmbeddingOfUnionSubobjectWithGivenUnion. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota1, iota2, union ) \mapsto \mathtt{EmbeddingOfUnionSubobjectWithGivenUnion}(iota1, iota2, union)\).

1.10-14 AddExactCoverWithGlobalElements

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ExactCoverWithGlobalElements. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2 ) \mapsto \mathtt{ExactCoverWithGlobalElements}(arg2)\).

1.10-15 AddHasPushoutComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation HasPushoutComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2, arg3 ) \mapsto \mathtt{HasPushoutComplement}(arg2, arg3)\).

1.10-16 AddIndexOfNonliftableMorphismFromDistinguishedObject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IndexOfNonliftableMorphismFromDistinguishedObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota ) \mapsto \mathtt{IndexOfNonliftableMorphismFromDistinguishedObject}(iota)\).

1.10-17 AddInjectionOfCoproductComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InjectionOfCoproductComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota ) \mapsto \mathtt{InjectionOfCoproductComplement}(iota)\).

1.10-18 AddInjectionOfCoproductComplementWithGivenCoproductComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation InjectionOfCoproductComplementWithGivenCoproductComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota, complement ) \mapsto \mathtt{InjectionOfCoproductComplementWithGivenCoproductComplement}(iota, complement)\).

1.10-19 AddIntersectionSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IntersectionSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2, arg3 ) \mapsto \mathtt{IntersectionSubobject}(arg2, arg3)\).

1.10-20 AddIsomorphismOntoCartesianSquareOfPowerObject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismOntoCartesianSquareOfPowerObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{IsomorphismOntoCartesianSquareOfPowerObject}(a)\).

1.10-21 AddIsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ExpaOmega2, a, PaxPa ) \mapsto \mathtt{IsomorphismOntoCartesianSquareOfPowerObjectWithGivenObjects}(ExpaOmega2, a, PaxPa)\).

1.10-22 AddLawvereTierneyEmbeddingsOfSubobjectClassifiers

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LawvereTierneyEmbeddingsOfSubobjectClassifiers. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{LawvereTierneyEmbeddingsOfSubobjectClassifiers}()\).

1.10-23 AddLawvereTierneyLocalModalityOperators

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LawvereTierneyLocalModalityOperators. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{LawvereTierneyLocalModalityOperators}()\).

1.10-24 AddLawvereTierneySubobjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LawvereTierneySubobjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{LawvereTierneySubobjects}()\).

1.10-25 AddLeftFiberMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftFiberMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( b, c ) \mapsto \mathtt{LeftFiberMorphism}(b, c)\).

1.10-26 AddLeftFiberMorphismWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LeftFiberMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Pbxc_b, b, c, Pc ) \mapsto \mathtt{LeftFiberMorphismWithGivenObjects}(Pbxc_b, b, c, Pc)\).

1.10-27 AddListOfSubobjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ListOfSubobjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2 ) \mapsto \mathtt{ListOfSubobjects}(arg2)\).

1.10-28 AddLowerSegmentOfRelation

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LowerSegmentOfRelation. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, mu ) \mapsto \mathtt{LowerSegmentOfRelation}(a, b, mu)\).

1.10-29 AddLowerSegmentOfRelationWithGivenRange

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation LowerSegmentOfRelationWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, mu, Pa ) \mapsto \mathtt{LowerSegmentOfRelationWithGivenRange}(a, b, mu, Pa)\).

1.10-30 AddNonliftableMorphismFromDistinguishedObject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation NonliftableMorphismFromDistinguishedObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( iota ) \mapsto \mathtt{NonliftableMorphismFromDistinguishedObject}(iota)\).

1.10-31 AddPLeftTransposeMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PLeftTransposeMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f ) \mapsto \mathtt{PLeftTransposeMorphism}(a, b, f)\).

1.10-32 AddPLeftTransposeMorphismWithGivenRange

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PLeftTransposeMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f, Pb ) \mapsto \mathtt{PLeftTransposeMorphismWithGivenRange}(a, b, f, Pb)\).

1.10-33 AddPRightTransposeMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PRightTransposeMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f ) \mapsto \mathtt{PRightTransposeMorphism}(a, b, f)\).

1.10-34 AddPRightTransposeMorphismWithGivenRange

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PRightTransposeMorphismWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, f, Pa ) \mapsto \mathtt{PRightTransposeMorphismWithGivenRange}(a, b, f, Pa)\).

1.10-35 AddPowerObject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2 ) \mapsto \mathtt{PowerObject}(arg2)\).

1.10-36 AddPowerObjectFunctorial

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectFunctorial. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( f ) \mapsto \mathtt{PowerObjectFunctorial}(f)\).

1.10-37 AddPowerObjectFunctorialWithGivenPowerObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectFunctorialWithGivenPowerObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Pb, f, Pa ) \mapsto \mathtt{PowerObjectFunctorialWithGivenPowerObjects}(Pb, f, Pa)\).

1.10-38 AddPowerObjectLeftEvaluationMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectLeftEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{PowerObjectLeftEvaluationMorphism}(a)\).

1.10-39 AddPowerObjectLeftEvaluationMorphismWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectLeftEvaluationMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Pa_xa, a, Omega ) \mapsto \mathtt{PowerObjectLeftEvaluationMorphismWithGivenObjects}(Pa_xa, a, Omega)\).

1.10-40 AddPowerObjectRightEvaluationMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectRightEvaluationMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{PowerObjectRightEvaluationMorphism}(a)\).

1.10-41 AddPowerObjectRightEvaluationMorphismWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PowerObjectRightEvaluationMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( axPa, a, Omega ) \mapsto \mathtt{PowerObjectRightEvaluationMorphismWithGivenObjects}(axPa, a, Omega)\).

1.10-42 AddProjectionInDirectProductComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ProjectionInDirectProductComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( pi ) \mapsto \mathtt{ProjectionInDirectProductComplement}(pi)\).

1.10-43 AddProjectionInDirectProductComplementWithGivenDirectProductComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation ProjectionInDirectProductComplementWithGivenDirectProductComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( pi, complement ) \mapsto \mathtt{ProjectionInDirectProductComplementWithGivenDirectProductComplement}(pi, complement)\).

1.10-44 AddPseudoComplementSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PseudoComplementSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2 ) \mapsto \mathtt{PseudoComplementSubobject}(arg2)\).

1.10-45 AddPushoutComplement

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation PushoutComplement. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( l, m ) \mapsto \mathtt{PushoutComplement}(l, m)\).

1.10-46 AddRelativePseudoComplementSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativePseudoComplementSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2, arg3 ) \mapsto \mathtt{RelativePseudoComplementSubobject}(arg2, arg3)\).

1.10-47 AddRelativeTruthMorphismOfAnd

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfAnd. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfAnd}(a)\).

1.10-48 AddRelativeTruthMorphismOfAndWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfAndWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfAndWithGivenObjects}(PaxPa, a, Pa)\).

1.10-49 AddRelativeTruthMorphismOfFalse

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfFalse. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfFalse}(a)\).

1.10-50 AddRelativeTruthMorphismOfFalseWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfFalseWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( T, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfFalseWithGivenObjects}(T, a, Pa)\).

1.10-51 AddRelativeTruthMorphismOfImplies

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfImplies. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfImplies}(a)\).

1.10-52 AddRelativeTruthMorphismOfImpliesWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfImpliesWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfImpliesWithGivenObjects}(PaxPa, a, Pa)\).

1.10-53 AddRelativeTruthMorphismOfNot

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfNot. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfNot}(a)\).

1.10-54 AddRelativeTruthMorphismOfNotWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfNotWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Pa, a, Pa1 ) \mapsto \mathtt{RelativeTruthMorphismOfNotWithGivenObjects}(Pa, a, Pa1)\).

1.10-55 AddRelativeTruthMorphismOfOr

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfOr. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfOr}(a)\).

1.10-56 AddRelativeTruthMorphismOfOrWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfOrWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( PaxPa, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfOrWithGivenObjects}(PaxPa, a, Pa)\).

1.10-57 AddRelativeTruthMorphismOfTrue

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfTrue. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{RelativeTruthMorphismOfTrue}(a)\).

1.10-58 AddRelativeTruthMorphismOfTrueWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RelativeTruthMorphismOfTrueWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( T, a, Pa ) \mapsto \mathtt{RelativeTruthMorphismOfTrueWithGivenObjects}(T, a, Pa)\).

1.10-59 AddRightFiberMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightFiberMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( b, c ) \mapsto \mathtt{RightFiberMorphism}(b, c)\).

1.10-60 AddRightFiberMorphismWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation RightFiberMorphismWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( cxPbxc, b, c, Pb ) \mapsto \mathtt{RightFiberMorphismWithGivenObjects}(cxPbxc, b, c, Pb)\).

1.10-61 AddSingletonMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SingletonMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a ) \mapsto \mathtt{SingletonMorphism}(a)\).

1.10-62 AddSingletonMorphismWithGivenPowerObject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SingletonMorphismWithGivenPowerObject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, Pa ) \mapsto \mathtt{SingletonMorphismWithGivenPowerObject}(a, Pa)\).

1.10-63 AddSubobjectClassifier

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SubobjectClassifier. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{SubobjectClassifier}()\).

1.10-64 AddSubobjectOfClassifyingMorphism

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation SubobjectOfClassifyingMorphism. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( alpha ) \mapsto \mathtt{SubobjectOfClassifyingMorphism}(alpha)\).

1.10-65 AddTruthMorphismOfAnd

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfAnd. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{TruthMorphismOfAnd}()\).

1.10-66 AddTruthMorphismOfAndWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfAndWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfAndWithGivenObjects}(Omega2, Omega)\).

1.10-67 AddTruthMorphismOfFalse

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfFalse. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{TruthMorphismOfFalse}()\).

1.10-68 AddTruthMorphismOfFalseWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfFalseWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( T, Omega ) \mapsto \mathtt{TruthMorphismOfFalseWithGivenObjects}(T, Omega)\).

1.10-69 AddTruthMorphismOfImplies

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfImplies. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{TruthMorphismOfImplies}()\).

1.10-70 AddTruthMorphismOfImpliesWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfImpliesWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfImpliesWithGivenObjects}(Omega2, Omega)\).

1.10-71 AddTruthMorphismOfNot

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfNot. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{TruthMorphismOfNot}()\).

1.10-72 AddTruthMorphismOfNotWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfNotWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Omega, Omega1 ) \mapsto \mathtt{TruthMorphismOfNotWithGivenObjects}(Omega, Omega1)\).

1.10-73 AddTruthMorphismOfOr

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfOr. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{TruthMorphismOfOr}()\).

1.10-74 AddTruthMorphismOfOrWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfOrWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( Omega2, Omega ) \mapsto \mathtt{TruthMorphismOfOrWithGivenObjects}(Omega2, Omega)\).

1.10-75 AddTruthMorphismOfTrue

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfTrue. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( ) \mapsto \mathtt{TruthMorphismOfTrue}()\).

1.10-76 AddTruthMorphismOfTrueWithGivenObjects

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation TruthMorphismOfTrueWithGivenObjects. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( T, Omega ) \mapsto \mathtt{TruthMorphismOfTrueWithGivenObjects}(T, Omega)\).

1.10-77 AddUnionSubobject

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UnionSubobject. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( arg2, arg3 ) \mapsto \mathtt{UnionSubobject}(arg2, arg3)\).

1.10-78 AddUpperSegmentOfRelation

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UpperSegmentOfRelation. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, mu ) \mapsto \mathtt{UpperSegmentOfRelation}(a, b, mu)\).

1.10-79 AddUpperSegmentOfRelationWithGivenRange

Returns: nothing

The arguments are a category \(C\) and a function \(F\). This operation adds the given function \(F\) to the category for the basic operation UpperSegmentOfRelationWithGivenRange. Optionally, a weight (default: 100) can be specified which should roughly correspond to the computational complexity of the function (lower weight = less complex = faster execution). \(F: ( a, b, mu, Pb ) \mapsto \mathtt{UpperSegmentOfRelationWithGivenRange}(a, b, mu, Pb)\).

1.11 Coproduct and direct product complements

1.11-1 CoproductComplement

Returns: an object

The argument is a morphism iota\(: S \to T\) which is a coproduct injection of some binary coproduct. The output is an object \(C\) such that \(S \sqcup C \cong T\).

1.11-2 InjectionOfCoproductComplement

Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \iota ) )\)

The argument is a morphism iota\(: S \to T\) which is a coproduct injection of some binary coproduct. The output is a coproduct injection \(\iota_2: C \to T\) such that UniversalMorphismFromCoproduct( iota, \(\iota_2\) )\(: S \sqcup C \to T\) is an isomorphism.

1.11-3 InjectionOfCoproductComplementWithGivenCoproductComplement

Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \iota ) )\)

The argument is a morphism iota\(: S \to T\) which is a coproduct injection of some binary coproduct and a coproduct complement C. The output is a coproduct injection \(\iota_2:\) C \(\to T\) such that UniversalMorphismFromCoproduct( iota, \(\iota_2\) )\(: S \sqcup C \to T\) is an isomorphism.

1.11-4 DirectProductComplement

Returns: an object

The argument is a morphism pi\(: S \to T\) which is a product projection of some binary direct product. The output is an object \(C\) such that \(S \times C \cong T\).

1.11-5 ProjectionInDirectProductComplement

Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \pi ) )\)

The argument is a morphism pi\(: S \to T\) which is a direct product projection of some binary direct product. The output is a direct product projection \(\pi_2: C \to T\) such that UniversalMorphismIntoDirectProduct( pi, \(\pi_2\) )\(: T \to S \times C\) is an isomorphism.

1.11-6 ProjectionInDirectProductComplementWithGivenDirectProductComplement

Returns: a morphism in \(\mathrm{Hom}( C, \mathrm{Target}( \pi ) )\)

The argument is a morphism pi\(: S \to T\) which is a direct product projection of some binary direct product and a coproduct complement C. The output is a direct product projection \(\pi_2:\) C \(\to T\) such that UniversalMorphismIntoDirectProduct( pi, \(\pi_2\) )\(: T \to S \times C\) is an isomorphism.

generated by GAPDoc2HTML