Syntax Definition ht 2

Description: The type of all functions from type α to type β.

Hypotheses

Ref	Expression
hal	type α
hbe	type β

Assertion

Ref	Expression
ht	type (α → β)

This syntax is primitive. The first axiom using it is ax-weq 40.