A.1.5 The finite types
We introduce primitive constants ⋆, 𝟎, 𝟏, satisfying the following rules:
-
•
𝟎:𝒰0, 𝟏:𝒰0
-
•
⋆:𝟏
Given C:𝟎→𝒰n we can introduce a defined constant f:∏(x:𝟎)C(x), with no defining equations.
Given C:𝟏→𝒰n and d:C(⋆) we can introduce a defined constant f:∏(x:𝟏)C(x), with defining equation f(⋆):≡d.
Title | A.1.5 The finite types |
---|---|
\metatable |