Goto Chapter: Top 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 Ind

### 5 Co-Heyting algebras

#### 5.1 Properties

##### 5.1-1 IsCoHeytingAlgebroid
 ‣ IsCoHeytingAlgebroid( C ) ( property )

Returns: true or false

The property of C being a co-Heyting algebroid.

##### 5.1-2 IsCoHeytingAlgebra
 ‣ IsCoHeytingAlgebra( C ) ( property )

Returns: true or false

The property of C being a co-Heyting algebra.

#### 5.2 Operations

##### 5.2-1 ConegationOnObjects
 ‣ ConegationOnObjects( a ) ( attribute )

Returns: an object

The argument is an object a. The output is its co-negated object \ulcorner a.

##### 5.2-2 ConegationOnMorphisms
 ‣ ConegationOnMorphisms( alpha ) ( attribute )

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

The argument is a morphism \alpha: a \rightarrow b. The output is its negated morphism \ulcorner \alpha: \ulcorner b \rightarrow \ulcorner a.

##### 5.2-3 ConegationOnMorphismsWithGivenConegations
 ‣ ConegationOnMorphismsWithGivenConegations( s, alpha, r ) ( operation )

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

The argument is an object s = \ulcorner b, a morphism \alpha: a \rightarrow b, and an object r = \ulcorner a. The output is the negated morphism \ulcorner \alpha: \ulcorner b \rightarrow \ulcorner a.

##### 5.2-4 MorphismFromDoubleConegation
 ‣ MorphismFromDoubleConegation( a ) ( attribute )

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

The argument is an object a. The output is the morphism from the double conegation \ulcorner\ulcorner a \rightarrow a.

##### 5.2-5 MorphismFromDoubleConegationWithGivenDoubleConegation
 ‣ MorphismFromDoubleConegationWithGivenDoubleConegation( a, r ) ( operation )

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

The arguments are an object a, and an object r = \ulcorner\ulcorner a. The output is the morphism from the double conegation \ulcorner\ulcorner a \rightarrow a.

#### 5.3 Stable internal coHom

##### 5.3-1 StableInternalCoHom
 ‣ StableInternalCoHom( V, W ) ( operation )

Returns: a CAP object

Return the stable internal coHom: \mathrm{\underline{coHom}}(\mathrm{\underline{coHom}}(...\mathrm{\underline{coHom}}(V,W)...,W),W).

 ‣ AddConegationOnMorphisms( 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 ConegationOnMorphisms. F: ( alpha ) \mapsto \mathtt{ConegationOnMorphisms}(alpha).

 ‣ AddConegationOnMorphismsWithGivenConegations( 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 ConegationOnMorphismsWithGivenConegations. F: ( s, alpha, r ) \mapsto \mathtt{ConegationOnMorphismsWithGivenConegations}(s, alpha, r).

 ‣ AddConegationOnObjects( 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 ConegationOnObjects. F: ( arg2 ) \mapsto \mathtt{ConegationOnObjects}(arg2).

 ‣ AddMorphismFromDoubleConegation( 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 MorphismFromDoubleConegation. F: ( a ) \mapsto \mathtt{MorphismFromDoubleConegation}(a).

 ‣ AddMorphismFromDoubleConegationWithGivenDoubleConegation( C, F ) ( operation )
The arguments are a category C and a function F. This operation adds the given function F to the category for the basic operation MorphismFromDoubleConegationWithGivenDoubleConegation. F: ( a, s ) \mapsto \mathtt{MorphismFromDoubleConegationWithGivenDoubleConegation}(a, s).