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

### 4 Heyting algebras

#### 4.1 Properties

##### 4.1-1 IsHeytingAlgebroid
 ‣ IsHeytingAlgebroid( C ) ( property )

Returns: true or false

The property of C being a Heyting algebroid.

##### 4.1-2 IsHeytingAlgebra
 ‣ IsHeytingAlgebra( C ) ( property )

Returns: true or false

The property of C being a Heyting algebra.

#### 4.2 Operations

##### 4.2-1 NegationOnObjects
 ‣ NegationOnObjects( a ) ( attribute )

Returns: an object

The argument is an object $$a$$. The output is its negated object $$\neg a$$.

##### 4.2-2 NegationOnMorphisms
 ‣ NegationOnMorphisms( alpha ) ( attribute )

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

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

##### 4.2-3 NegationOnMorphismsWithGivenNegations
 ‣ NegationOnMorphismsWithGivenNegations( s, alpha, r ) ( operation )

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

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

##### 4.2-4 MorphismToDoubleNegation
 ‣ MorphismToDoubleNegation( a ) ( attribute )

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

The argument is an object $$a$$. The output is the morphism to the double negation $$a \rightarrow \neg\neg a$$.

##### 4.2-5 MorphismToDoubleNegationWithGivenDoubleNegation
 ‣ MorphismToDoubleNegationWithGivenDoubleNegation( a, r ) ( operation )

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

The arguments are an object $$a$$, and an object $$r = \neg\neg a$$. The output is the morphism to the double negation $$a \rightarrow \neg\neg a$$.

#### 4.3 Stable internal Hom

##### 4.3-1 StableInternalHom
 ‣ StableInternalHom( J, I ) ( operation )

Returns: a CAP object

Return the stable internal Hom: $$\mathrm{\underline{Hom}}(J,\mathrm{\underline{Hom}}(J,...\mathrm{\underline{Hom}}(J,I)...))$$.

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

 ‣ AddMorphismToDoubleNegationWithGivenDoubleNegation( 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 MorphismToDoubleNegationWithGivenDoubleNegation. $$F: ( a, r ) \mapsto \mathtt{MorphismToDoubleNegationWithGivenDoubleNegation}(a, r)$$.

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

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

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