PS

If expression

いわゆるif文の圏論的表現。

Distributive category

  •  \mathcal{C} has finite products:  (\times, 1)
  •  \mathcal{C} has finite coproducts:  (+, 0)
  •  (A \times B) + (A \times C) \cong A \times (B + C)

なるcategory  \mathcal{C} のこと。

以下、distributive category  \mathcal{C} について・・・

Predicate

  •  \mathtt{T} := \mathtt{F} := \mathbb{1}
  •  p : A \to \mathtt{T} + \mathtt{F}

Guard

  •  p ? := A \overset{\langle 1 _ A, p \rangle}{\to} A \times (\mathtt{T} + \mathtt{F}) \cong (A \times \mathtt{T} ) + (A \times \mathtt{F}) \overset{\pi _ A + \pi _ A}{\to} A + A

If expression

  •  f : A \to B
  •  g : A \to C
  •  \operatorname{\mathtt{if}} p \operatorname{\mathtt{then}} f \operatorname{\mathtt{else}} g := A \overset{p?}{\to} A + A \overset{f + g}{\to} B + C

参考文献