Relation

A relation $𝑃$ between collections $𝐴$ and $𝐵$ is a binary predicate on elements of $𝐴$ and elements of $𝐵$ :

𝑎 \in 𝐴, 𝑏 \in 𝐵 ⊢ 𝑃 (𝑎, 𝑏) p r o p .

A relation between $𝐴$ and itself is also called a relation on $𝐴$ .

Encodings

Type theory

In dependent type theory, under the paradigm of propositions as some types, a relation $𝑃$ beween types $𝐴$ and $𝐵$ is a fibration

𝑎 : 𝐴, 𝑏 : 𝐵 ⊢ 𝑃 (𝑎, 𝑏)

such that for all $𝑎 : 𝐴, 𝑏 : 𝐵$ , $𝑃 (𝑎, 𝑏)$ is an h-Prop.

Material set theory

To talk about relations internal to material set theory, we must encode relations as sets. Following the approach of type theory, one might be tempted to define a relation as a function $𝐴 \times 𝐵 \to Ω$ , where $Ω$ is the set of truth values (classically $Ω = {⊤, ⊥}$ ). But in material set theory, functions themselves are encoded as relations. Thus in $Z F$ one more typically define a relation is identified with the following subset of the cartesian product

𝑅 = {(𝑎, 𝑏) \in 𝐴 \times 𝐵 : 𝑎 𝑅 𝑏}

Classification

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