- (ΦX,A,Y(f)□A^);ev = f
ΦX,A,Y(f) = Φ(f) = F と置いて、(ΦX,A,Y(f)□A^) = F□A^ を計算する。
F□A^ : X□A→hom(A, Y)□A = [ λ0(x, a)∈A□A.( (F(x), a) ∈hom(A, Y)□A ) ALSO λ1(x→x', a)∈A□A.( (F(x→x'), a) ∈hom(A, Y)□A ) OR λ1(x, a→a')∈A□A.( (F(x), a→a') ∈hom(A, Y)□A ) ] : X□A→hom(A, Y)□A = λ[(x, a) ALSO (x→x', a) OR (x, a→a')∈X□A.( [ ( (F(x), a) ∈hom(A, Y)□A) ALSO ( (F(x→x'), a) ∈hom(A, Y)□A) OR ( (F(x), a→a') ∈hom(A, Y)□A) ] ∈hom(A, Y)□A )
これに ev〈エバル | 評価射〉を後結合すると、
λ[(x, a) ALSO (x→x', a) OR (x, a→a')∈X□A.( [ ( F(x)(a) ∈Y) ALSO ( (F(x→x')(a) ∈Y) OR ( (F(x)(a→a') ∈Y) ] ∈Y )
という写像になる。F = Φ(f) だったので、これは f に他ならない。したがって、
- (ΦX,A,Y(f)□A^);ev = f
が成立する。