‣ 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 ) |
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. F: ( a ) \mapsto \mathtt{MorphismFromDoubleNegation}(a).
‣ AddMorphismFromDoubleNegationWithGivenDoubleNegation( C, F ) | ( 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. F: ( a, s ) \mapsto \mathtt{MorphismFromDoubleNegationWithGivenDoubleNegation}(a, s).
‣ AddMorphismToDoubleConegation( C, F ) | ( 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. F: ( a ) \mapsto \mathtt{MorphismToDoubleConegation}(a).
‣ AddMorphismToDoubleConegationWithGivenDoubleConegation( C, F ) | ( 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. F: ( a, r ) \mapsto \mathtt{MorphismToDoubleConegationWithGivenDoubleConegation}(a, r).
‣ 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.
generated by GAPDoc2HTML