section 分数の定義と掛け算 { declare 0-mor F in Set define F := Int×(Int\{0}) declare 0-mor 1 in F // オーバーロード define 1 := (1, 1) declare 1-mor m : F×F → F in Set reserve a, b, c ∈F reserve x, y ∈Int define m := λ(a, b).( (a_1×b_1, a_2×b_2) ) justification x ≠ 0 ∧ y ≠ 0 ⇒ x×y ≠ 0 declare 1-mor assoc_pred : F×F×F → Bool in Set define assoc_pred := λ(a, b, c).( m(m(a, b), c) = m(a, m(b, c)) on F ) declare 2-mor @id assoc :: True_{F×F×F} ⇒ assco_pred : F×F×F → Bool in Set // assoc の 証明 // 1 は定義しているが、この節では単位律には言及しないとする。 // 0-mor in 0-cat から 1-mor in 1-cat への変換が必要かも。 }
組織化・構造化:
signature Semigroup { declare 0-mor U in Set declare 1-mor m : U×U→ U in Set local declare 1-mor assoc_pred : U×U×U → Bool in Set local define assoc_pred := λ(a, b, c)∈U×U×U.( m(m(a, b), c) = m(a, m(b, c)) on U ) declare 2-mor @id assoc :: True_{U×U×U} ⇒ assco_pred : U×U×U → Bool in Set } model F of Semigroup { define U := Int×(Int\{0}) define m := λ(a, b)∈U×U.( (a_1×b_1, a_2×b_2) ) define assoc := (assocの証明) }
記述の簡素化:
signature Semigroup within Set{ 0-mor U 1-mor m : U×U→ U let assoc_pred : U×U×U → Bool := λ(a, b, c)∈U×U×U.( m(m(a, b), c) = m(a, m(b, c)) on U ) 2-mor assoc :: True_{U×U×U} ⇒ assco_pred : U×U×U → Bool } model F of Semigroup { U := Int×(Int\{0}) m := λ(a, b)∈U×U.( (a_1×b_1, a_2×b_2) ) assoc := (assocの証明) }