‣ 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