‣ IsBiHeytingAlgebroid ( C ) | ( property ) |
Returns: true
or false
The property of C being a bi-Heyting algebroid.
‣ IsBiHeytingAlgebra ( C ) | ( property ) |
Returns: true
or false
The property of C being a bi-Heyting algebra.
‣ IsBooleanAlgebroid ( C ) | ( property ) |
Returns: true
or false
The property of C being a Boolean algebroid.
‣ IsBooleanAlgebra ( C ) | ( property ) |
Returns: true
or false
The property of C being a Boolean algebra.
‣ MorphismFromDoubleNegation ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(\neg\neg a, a)\).
The argument is an object \(a\). The output is the inverse \(\neg\neg a \rightarrow a\) of the morphism to the double negation.
‣ MorphismFromDoubleNegationWithGivenDoubleNegation ( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(\neg\neg a, a)\).
The argument is an object \(a\), and an object \(s = \neg\neg a\). The output is the inverse \(\neg\neg a \rightarrow a\) of the morphism to the double negation.
‣ MorphismToDoubleConegation ( a ) | ( attribute ) |
Returns: a morphism in \(\mathrm{Hom}(a, \ulcorner\ulcorner a)\).
The argument is an object \(a\). The output is the inverse \(a \rightarrow \ulcorner\ulcorner a\) of the morphism from the double conegation.
‣ MorphismToDoubleConegationWithGivenDoubleConegation ( a, s ) | ( operation ) |
Returns: a morphism in \(\mathrm{Hom}(a, \ulcorner\ulcorner a)\).
The argument is an object \(a\), and an object \(r = \ulcorner\ulcorner a\). The output is the inverse \(a \rightarrow \ulcorner\ulcorner a\) of the morphism from the double conegation.
‣ AddMorphismFromDoubleNegation ( C, F ) | ( operation ) |
‣ AddMorphismFromDoubleNegation ( C, F, weight ) | ( operation ) |
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 MorphismFromDoubleNegation
. 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{MorphismFromDoubleNegation}(a)\).
‣ AddMorphismFromDoubleNegationWithGivenDoubleNegation ( C, F ) | ( operation ) |
‣ AddMorphismFromDoubleNegationWithGivenDoubleNegation ( C, F, weight ) | ( operation ) |
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 MorphismFromDoubleNegationWithGivenDoubleNegation
. 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, s ) \mapsto \mathtt{MorphismFromDoubleNegationWithGivenDoubleNegation}(a, s)\).
‣ AddMorphismToDoubleConegation ( C, F ) | ( operation ) |
‣ AddMorphismToDoubleConegation ( C, F, weight ) | ( operation ) |
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 MorphismToDoubleConegation
. 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{MorphismToDoubleConegation}(a)\).
‣ AddMorphismToDoubleConegationWithGivenDoubleConegation ( C, F ) | ( operation ) |
‣ AddMorphismToDoubleConegationWithGivenDoubleConegation ( C, F, weight ) | ( operation ) |
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 MorphismToDoubleConegationWithGivenDoubleConegation
. 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, r ) \mapsto \mathtt{MorphismToDoubleConegationWithGivenDoubleConegation}(a, r)\).
generated by GAPDoc2HTML