Go backward to OrthogonalityGo up to TopGo forward to Categorical Product |

- Are our constructions of records and lambda abstractions the "right"
ones?
- Justification by category theory.
- Categorical product.
- Categorical exponentiation.

- Definitions:
- <E
, E_{1}>:= (_{2}`fst`=`E`,_{1}`snd`=`E`)_{2} *e**V*1 :=`with`*e*`do``fst`*e**V*2 :=`with`*e*`do``snd`- (E
= E_{1}) := [[_{2}`pi`|- E:_{1}`theta`]]*e*= [[`pi`|- E:_{2}`theta`]]*e*,

*e*in`Env`_{pi}

- <E

Author: Wolfgang Schreiner

Last Modification: May 14, 1998