型システム λ1× を以下のように定める。 まず、 型 A と項 M を、 A ::= α∣1∣A×A∣A⇀A M ::= a∣⋆∣⟨M,M⟩∣fstM∣sndM∣λa.M∣MM で定める。 ここで、 α と a はそれぞれ原子型と変項を表す。 次に、 項の型割り当ての推論規則を、 Γ,a:A,Γ󰎘⊢a:A ⊢⋆:1 Γ⊢M:A Γ⊢N:B Γ⊢⟨M,N⟩:A×B Γ⊢M:A×B Γ⊢fstM:A Γ⊢M:A×B Γ⊢sndM:B Γ,a:A⊢M:B Γ⊢λa.M:A⇀B Γ⊢M:A⇀B Γ⊢N:#A Γ⊢MN:B で定める。 最後に、 同じ型を割り当てられた項の間の等号を、 ⋆ = M fst⟨M,N⟩ = M snd⟨M,N⟩ = N ⟨fstM,sndM⟩ = M (λa.M)N = M[a:=N] λa.Ma = M で定め、 合同関係になるように拡張する。 ただし、 最後の等式において M は自由変項に a を含まないものとする。

型システム 󱁑 を考える。 有限直積をもつ圏 󰒚 に対し、 変換 - が、

• 󱁑 の型 A に対し、 󰒚 の対象 A が定まっている。
• 󱁑 における項の型割り当て Γ⊢M:A に対し、 󰒚 の射 Γ⊢M:A:Γ→A が定まっている。 ここで、 Γ≡b1:B1,⋯,bn:Bn と書くとき、 Γ=B1×⋯×Bn と定めた。 なお、 記法を簡略化して、 Γ⊢M:A の代わりに単に M と書くこともある。

を満たすように定まっている。 このとき、 - を 󱁑 の 󰒚 での 「解釈 (interpretation)」 という。

単純型付きラムダ計算 λ1× は、 任意のカルテシアン閉圏で標準的な解釈をもつ。 さらに、 λ1× における型割り当て Γ⊢M:A および Γ⊢N:A に対し、 λ1× において M=N が成り立つための必要十分条件は、 任意のカルテシアン閉圏において M=N が成り立つことである。

型システム Arrow を λ1× の拡張として以下のように定める。 まず、 型 A と項 M を、 A ::= ⋯∣[A,A] M ::= ⋯∣arrM∣M⋙M∣firstM と拡張する。 次に、 項の型割り当ての推論規則に、 Γ⊢M:A⇀B Γ⊢arrM:[A,B] Γ⊢F:[A,B] Γ⊢G:[B,C] Γ⊢F⋙G:[A,C] Γ⊢F:[A,B] Γ⊢firstF:[A×C,B×C] を追加する。 最後に、 同じ型を割り当てられた項の間の等号に、 arrid⋙F = F F⋙arrid = F (F⋙G)⋙H = F⋙(G⋙H) arr(M⊳N) = arrM⋙arrN first(arrM) = arr(M×id) firstF⋙arr(id×M) = arr(id×M)⋙firstF first(F⋙G) = firstF⋙firstG firstF⋙arrfst = arrfst⋙F first(firstF)⋙arrassoc = arrassoc⋙firstF を追加し、 合同関係になるように拡張する。 ここで、 id : A⇀A ≡ λa.a fst : A×B⇀A ≡ λp.fstp assoc : (A×B)×C⇀A×(B×C) ≡ λp.⟨fst(fstp),⟨snd(fstp),sndp)⟩⟩ ⊳ : (A⇀B)×(B⇀C)⇀(A⇀C) ≡ λm.λn.λa.n(ma) × : (A⇀B)×(B⇀D)⇀(A×C⇀B×D) ≡ λm.λn.λp.⟨m(fstp),n(sndp)⟩ で定めている。 すなわち順に、 恒等関数, 直積から第 1 成分への射影関数, 3 つの直積の結合を変える関数, 関数の合成演算, 関数の直積演算である。