homが反変・共変の双関手であることは、直接示す必要はありません（間接的に言えます）が、計算のための具体的な表示は必要になります。
内容：
グラフ射と変形の結合
f:A→B がグラフ射、β:w⇒w':B (0→1) C が変形だとします。両端がグラフ射である変形の定義より、
- β:B(0)→C(1)
- β;s = w(0) （w(1) は自動的に決まる）
- β;t = w'(0) （w'(1) は自動的に決まる）
fとβの結合〈composition〉を次のように定義します。
- (f;;β)(a) := β(f(a)) ∈C(1)
f;;β が変形 A (0→1) C になるのは明らかですが、
- f;;β: f;w⇒f;w' : A (0→1) C
つまり、f;;β の両端は、f;w と f;w' になります。
同様に、α:u⇒u':A (0→1) B, g:B→C に対して、
- (α;;g)(a) := g(α(a)) ∈C(1)
と定義すると、
- α;;g: u;g⇒u';g : A (0→1) C
ホムグラフとグラフ射
A', A, Y, Y' ∈|SG|, p:A'→A, q:Y→Y' in SG とします。文字の使用が奇妙なのは、後で出てくる記法と合わせるため。hom(-, -) の片側にグラフ射、もう一方にはグラフを入れた形を直接定義します。
hom(p:A'→A, Y):hom(A, Y)→hom(A', Y) :=
[
λ0u∈hom(A, Y).(
p;u /* グラフ射の結合 図式順、pを前結合 */
∈Hom(A', Y) )
ALSO
λ1u⇒v∈hom(A, Y).(
p;;(u⇒v) /* グラフ射と変形の結合 図式順、pを前結合 */
∈Defm(A', Y) )
]
hom(A, q:Y→Y'):hom(A, Y)→hom(A, Y') :=
[
λ0u∈hom(A, Y).(
u;q /* グラフ射の結合 図式順、qを後結合 */
∈Hom(A, Y') )
ALSO
λ1u⇒v∈hom(A, Y).(
(u⇒v);;q /* 変形とグラフ射の結合 図式順、qを後結合 */
∈Defm(A, Y') )
]
