$𝜂$ -unicity

An $𝜂$ -unicity rule is a conversion rule, usually a judgemental equality, expressing the uniqueness of a connectives canonical terms. This is in some sense dual to $𝛽$ -computation, since $𝜂$ -unicity specifies the result of an introduction rule applied to an eliminator. For example, in the untyped λ-calculus, we have

𝜆 𝑥 . 𝑓 𝑥 = 𝜂 𝑓,

and thus “all functions are $𝜆$ -abstractions”. Similarly, in the simply typed λ-calculus, we have

𝑝 = ⟨ 𝐩 𝐫 1 (𝑝), 𝐩 𝐫 2 (𝑝) ⟩ : 𝐴 \times 𝐵

thus “all terms in the product type are pairs.”

Internalizing judgemental structure

In terms of Internalizing judgemental structure, if a connective $Υ$ is specified by a family of bijections

𝜄 : 𝐴 Γ ≅ 𝐵 Γ

natural in $Γ$ where

$𝐴 Γ$ is either $T m (Γ, Υ)$ or $T m (Γ . Υ, 𝐴)$ ;
$𝐵 Γ$ is a meta-set constructed from sets of terms (“judgementally-determined structure”)

then $𝜂$ -unicity comes from the identity

𝜄 - 1 \circ 𝜄 = i d 𝐴 Γ .

#state/tidy | #lang/en | #SemBr

𝜂-unicity

Internalizing judgemental structure

$𝜂$ -unicity