指標とモデルによる記述

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の証明)
}