 Then evaluation is

ε

B ,C

=

(1

MOR

(

B

;

C

)

)

.

So

ε

B ,C

(

p

;

q

) = (

(1

MOR

(

B

;

C

)

))(

p

;

q

) = (1

MOR

(

B

;

C

)

)(

p

)(

q

) =

p

(

q

)

.

Proposition 8.

Evaluation is a morphism of

Dig

.

Proof.

Because

ε

B ,C

(

p

;

q

) =

(1

MOR

(

B

;

C

)

)

.

It remains to prove:

[FIXME:

ε

X ,Y

. What are

X

and

Y

?]

ε

(

f

×

1

A

) =

f

;

(

ε

(

g

×

1

A

)) =

g

.

Proof.

ε

(

f

×

1

A

)(

a

;

p

) =

ε

((

f

)

a

;

p

) = (

f

)

ap

=

f

(

a

;

p

)

. So

ε

(

f

×

1

A

) =

f

.

(

ε

(

g

×

1

A

))(

p

)(

q

) = (

ε

(

g

×

1

A

))(

p

;

q

) =

ε

(

g

×

1

A

)(

p

;

q

) =

ε

(

g p

;

q

) =

g

(

p

)(

q

)

. So

(

ε

(

g

×

1

A

)) =

g

.

Exponentials in category Fcd

Define

Fcd

f

=

FCD

Dig

f

Definition 9.

A category is

cartesian closed

iff:

ε

(

f

×

1

A

) =

f

.

(

ε

(

g

×

1

A

)) =

g

.

But this follows from functoriality of

FCD

.

??

Embed

Fcd

into

Dig

by the formulas:

A

λX

P

Ob

A

:

h

A

i

X

f

h

f

i

Obviously this embedding (denote it

T

) is an injective (both on objects and morphisms) functor.

ε

A,B

Fcd

(

p

×

q

) =

h

p

i

q

[TODO: Should

p

and

q

be atomic?]

Rld

is induced by

Dig

.

Due its injectivity and functoriality, it is enough to prove:

1. binary products are preserved

2.

ε

T

A,

T

B

Dig

= T

ε

A,B

Fcd

3. that

Dig

T

f

= T

Fcd

f

for every

f

:

A

B

(T

ε

A,B

Fcd

)(

p

×

q

) =

h

ε

A,B

Fcd

i

(

p

×

q

) =

h

p

i

q

ε

T

A,

T

B

Dig

X

= (T

B

)

T

A

X

= (

λY

P

Ob

B

:

h

B

i

Y

)

λX

P

Ob

A

:

h

A

i

X

X

??

3