Prod の普遍性を表す簡単な例

[Seasawher]

variable {A B C : Type}

/-- 積の普遍性から導かれる射 -/
def fork (f : A → B) (g : A → C) : A → B × C :=
  fun a => (f a, g a)

/-- 第一成分への射影 -/
abbrev exl := @Prod.fst A B

/-- 第二成分への射影 -/
abbrev exr := @Prod.snd A B

open Prod

/-- ### 積の普遍性
すべての積への関数は、`fork` で書き表すことができる。 -/
example (h : A → B × C) : fork (fst ∘ h) (snd ∘ h) = h := rfl

/-- A × B → A × B は fork -/
example : fork fst snd = @id (A × B) := rfl

[Seasawher]

引用元：Calculating Functional Programs の 1.3.4

[Seasawher]

積の普遍性は次のように述べたほうが良い。

import Mathlib.Tactic

/-- ### 積の普遍性
すべての積への関数は、`fork` で書き表すことができる。 -/
example (h : A → B × C) : h = fork f g ↔ fst ∘ h = f ∧ snd ∘ h = g := by
  constructor <;> aesop