CWF

Properties

$\forall$ is a functor. It applies to types:

$$\forall Type=Ty(\forall P)$$

Preserves substitutions.

Relates to:

• Hoffman Preseaf Semantics.
• Standard Model Semantics
• Meta-circular Semantics
• Contextual Semantics
• Substitutions are just functions
• Types are maps