Teoria kategorii dla informatyków/Wykład 4: Zaawansowane konstrukcje uniwersalne

Eksponent

Mając dane dwa zbiory $A$ i $B$, możemy stworzyć- zgodnie z aksjomatyką teorii mnogości - zbiór wszystkich funkcji typu $A\to B$ oznaczany $B^A$. W języku kategoryjnym powiedzielibyśmy, że dla danych dwóch obiektów $A,B\in {\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}_0$, istnieje zawsze inny obiekt $B^A$, który nazwiemy tu eksponentem. Jeszcze krócej tę samą myśl wypowiemy tak: $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$ ma eksponenty. Spróbujmy zbadać, jaką własnością uniwersalną charakteryzują się eksponenty w $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$. Oto nieformalny tok rozumowania: skoro $B^A$, który łatwo będzie nam też zapisywać w miarę potrzeby jako $[A,B]$, jest pewnym specjalnym obiektem $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$, to muszą z nim być związane strzałki, które go dekonstruują, czyli rozkładają na czynniki $A$, $B$, z których powstał. (Tak było na przykład w przypadku produktu $A\times B$, gdzie destruktorami są projekcje.) Teoria mnogości wspomaga nas tutaj twierdzeniem, że istnieje izmorfizm

$\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}(Z\times A,B)\cong \mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}(Z,B^A)$      (4.1)

Rzeczywiście, dowolnej funkcji $f:Z\times A\to B$ przyporządkowujemy funkcję $\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f):Z\to B^A$ jako: $\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)(z):=f(z,-)$. Operacja $\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}$, nazywana kuryfikacją, jest szukaną bijekcją. Sens tej bijekcji możemy odczytać w następujący sposób - mając dane: funkcję $f:Z\times A\to B$ i dwa elementy $z\in Z$, $a\in A$, wartość $f(z,a)$ powstaje albo przez bezpośrednią aplikację funkcji $f$ do pary argumentów $(z,a)$, albo poprzez aplikację funkcji $\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)$ do argumentu $z$ i potem ewaluację tak powstałej funkcji na argumencie $a$. Innymi słowy, poniższy diagram komutuje:

gdzie $\mathrm{e}\mathrm{v}:B^A\times A\to B$ jest ewaluacją definiowaną jako $\mathrm{e}\mathrm{v}(f,a):=f(a)$. Rzeczywiście:

$(\mathrm{e}\mathrm{v}\circ (\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)\times 1_A))(z,a)=\mathrm{e}\mathrm{v}(\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)(z),a)=\mathrm{e}\mathrm{v}(f(z,-),a)=f(z,a)$

albo w końcu:

$\mathrm{e}\mathrm{v}\circ (\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)\times 1_A)=f$

Powyższe rozważania mają sens nie tylko w $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$, ale i w każdej kategorii z produktami. Otrzymujemy więc następującą definicję:

Definicja 4.1 [eksponent]

Niech $\mathbf{𝐂}$ będzie kategorią z produktami. Eksponentem obiektów $A$ i $B$ w $\mathbf{𝐂}$ jest obiekt $[A,B]\in {\mathbf{𝐂}}_0$ wraz ze strzałką $\mathrm{e}\mathrm{v}:[A,B]\times A\to B$, nazywaną ewaluacją, taką że dla dowolnego obiektu $Z\in {\mathbf{𝐂}}_0$ i strzałki $f:Z\times A\to B$ istnieje dokładnie jedna strzałka $\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f):Z\to [A,B]$ spełniająca równanie:

$\mathrm{e}\mathrm{v}\circ (\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)\times 1_A)=f$

wyrażone na diagramie jako:

Uwaga techniczna: często w dowodach pojawiają się naraz ewaluacje różnych typów; wygodnie wtedy $\mathrm{e}\mathrm{v}:[A,B]\times A\to B$ oznaczyć jako ${\mathrm{e}\mathrm{v}}_{A,B}$.

Zauważmy, że dla dowolnej strzałki $g:Z\to [A,B]$ możemy zdefiniować jej odwrotność jako

$\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(g):=\mathrm{e}\mathrm{v}\circ (g\times 1_A):Z\times A\to B$

Wtedy własność uniwersalna z powyższej definicji daje nam:

$\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(g))=g$

oraz dla dowolnej $f:Z\times A\to B$ komutowanie powyższego diagramu natychmiast implikuje, że:

$\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f))=f$

Pokazaliśmy więc izomorfizm:

${\mathrm{H}\mathrm{o}\mathrm{m}}_{\mathbf{𝐂}}(Z\times A,B)\cong {\mathrm{H}\mathrm{o}\mathrm{m}}_{\mathbf{𝐂}}(Z,[A,B])$,      (4.2)

który uogólnia izomorfizm (4.1) dla $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$.

Kategorie kartezjańsko zamknięte

Kategorie, w których istnieją eksponenty zasługują na wyróżnienie:

Definicja 4.2

Kategoria $\mathbf{𝐂}$ jest kartezjańsko zamknięta, jeśli posiada obiekt końcowy, produkty binarne i eksponenty.

Oto przykłady:

• $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$ jest kartezjańsko zamknięta. Podobnie ${\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}_{fin}$, gdyż konstrukcje są takie same, jak dla $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$, a eksponent $[A,B]$ dla zbiorów skończonych jest zbiorem skończonym.
• Kategoria $\mathbf{𝐏}\mathbf{𝐨}\mathbf{𝐬}$ jest kartezjańsko zamknięta. Produkt dwóch posetów $(P,\le )\times (Q,\le )$ definiuje się jako produkt zbiorów $P\times Q$ wraz z relacją częściowego porządku po współrzędnych: $(p_1,q_1)\le (p_2,q_2)$ wtedy i tylko wtedy, gdy $(p_1\le p_2)\wedge (q_1\le q_2)$ wraz z naturalnymi projekcjami ${\pi }_P(p,q):=p$ i ${\pi }_Q(p,q):=q$. Jako eksponent $[P,Q]$ bierzemy zbiór wszystkich funkcji monotonicznych typu $P\to Q$ wraz z porządkiem po współrzędnych: $f⊑g⟺\mathrm{\forall }z\in P(f(z)\le g(z))$ Ewaluacja i kuryfikacja są definiowane tak jak w $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$, wystarczy więc sprawdzić, że są monotoniczne. Jeśli $(f,p)\le (q,r)$ w $[P,Q]\times P$, to $\mathrm{e}\mathrm{v}(f,p)=f(p)\le g(p)\le g(r)=\mathrm{e}\mathrm{v}(g,r)$ a zatem ewaluacja jest monotoniczna. Natomiast dla $f:Z\times P\to Q$, $z⊑z^{\prime }$, $p\in P$ mamy $\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)(z)(p)=f(z,p)\le f(z^{\prime },p)=\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)(z^{\prime })(p)$ co świadczy o tym, że $\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)(z)\le \mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)(z^{\prime })$, czyli że kuryfikacja jest monotoniczna dla każdej funkcji $f$.
• Dwie ważne dla semantyki języków programowania kategorie kartezjańsko zamknięte: kategorię posetów zupełnych $\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}$ i kategorię bc-dziedzin $\mathbf{𝐁}\mathbf{𝐂}$ omawiamy oddzielnie w Wykładzie 13.
• Poset $(P,\le )$ z elementem najmniejszym $0$ jako kategoria jest kartezjańsko zamknięty wtedy i tylko wtedy, gdy jest algebrą Heytinga, zobacz podrozdział nt. algebr Heytinga.
• $\mathbf{𝐂}\mathbf{𝐚}\mathbf{𝐭}$ - kategoria wszystkich małych kategorii - jest kartezjańsko zamknięta.
• Dla dowolnej małej kategorii $\mathbf{𝐂}$ kategoria funktorów $[{\mathbf{𝐂}}^{op},\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}]$ jest kartezjańsko zamknięta. Do tego przykładu wrócimy w Wykładach 7 i 8.
• Kartezjańsko zamknięte nie są: $\mathbf{𝐕}\mathbf{𝐞}\mathbf{𝐜}\mathbf{𝐭}$, $\mathbf{𝐀}\mathbf{𝐛}$, $\mathbf{𝐓}\mathbf{𝐨}\mathbf{𝐩}$, $\mathbf{𝐌}\mathbf{𝐞}\mathbf{𝐭}$, ... z różnych przyczyn.

Algebry Heytinga

Przypomnijmy najpierw - w telegraficznym skrócie -pojęcia kraty dystrybutywnej i algebry Boole'a: Niech $(L,\le )$ będzie kratą z elementem najmniejszym $\mathbf{𝟎}$ i elementem największym $\mathbf{𝟏}$. Łatwo się przekonać, że kratę można również zdefiniować jako algebrę, bez relacji $\le$, jedynie za pomocą równości i prymitywnych operacji $\wedge ,\vee ,\mathbf{𝟎},\mathbf{𝟏}$.

Stwierdzenie 4.3

Niech $L$ będzie zbiorem z operacjami: $\wedge :L\times L\to L$ $\vee :L\times L\to L$ $\mathbf{𝟎}:1\to L$ $\mathbf{𝟏}:1\to L$

gdzie $\wedge$ i $\vee$ są łączne i przemienne oraz spełniają następujące aksjomaty:

$x\wedge x=x$ $x\vee x=x$ $\mathbf{𝟏}\wedge x=x$ $\mathbf{𝟎}\vee x=x$ $x\wedge (y\vee x)=x=(x\wedge y)\vee x$

dla dowolnych $x,y,z\in L$. Wówczas $(L,\le )$ jest kratą, gdzie $\le$ definiujemy jako

$x\le y⟺x=x\wedge y$

lub równoważnie:

$x\le y⟺y=x\vee y$

Oczywiście twierdzenie odwrotne też zachodzi.

Niektóre spośród krat posiadają ciekawą własność:

Definicja 4.4

Kratę $(L,\le )$ nazywamy dystrybutywną, jeśli dla dowolnych $x,y,z\in L$ zachodzi $x\wedge (y\vee z)=(x\wedge y)\vee (x\wedge z)$

Fakt 4.5

Powyższa równość w definicji implikuje równość dualną: $x\vee (y\wedge z)=(x\vee y)\wedge (x\vee z)$

Definicja 4.6

Elementem przeciwnym do $x$ w kracie $L$ nazywamy element $a\in L$ taki, że $x\wedge a=\mathbf{𝟎}$ i $x\vee a=\mathbf{𝟏}$.

Fakt 4.7

W kracie dystrybutywnej element przeciwny do $x$ jest jedyny. Oznaczamy go wówczas jako $\mathrm{\neg }x$.

Najbardziej znanymi kratami dystrybutywnymi są niewątpliwie algebry Boole'a.

Definicja 4.8 [algebra Boole'a]

Algebrą Boole'a nazywamy kratę dystrybutywną, w której każdy element $x$ ma element przeciwny.

Fakt 4.9

W dowolnej algebrze Boole'a $L$ zachodzą równości:

$\mathrm{\neg }(x\vee y)=\mathrm{\neg }x\wedge \mathrm{\neg }y$ $\mathrm{\neg }(x\wedge y)=\mathrm{\neg }x\vee \mathrm{\neg }y$ $\mathrm{\neg }\mathrm{\neg }x=x$

Pierwszą i drugą równość nazywamy prawami de Morgana.

Algebry Boole'a są szczególnymi przypadkami innych krat dystrybutywnych, tzw. algebr Heytinga, które omawiamy poniżej:

Definicja 4.10 [algebra Heytinga]

Algebrą Heytinga nazywamy kratę $(L,\le )$ z elementem najmniejszym $\mathbf{𝟎}$, elementem największym $\mathbf{𝟏}$ i operacją $\Rightarrow :L\times L\to L$ definiowaną dla każdej pary elementów $x,y\in L$ jako: $x\Rightarrow y:=\bigvee \{z\in L\mid z\wedge x\le y\}$

Taka definicja może na pierwszy rzut oka wydawać się przypadkowa. Punkt widzenia teorii kategorii rozjaśnia wątpliwości natychmiast: Jeśli potraktujemy kratę $(L,\le ,\mathbf{𝟎},\mathbf{𝟏})$ jako kategorię, będzie to kategoria, w której pomiędzy dwoma dowolnymi obiektami istnieje co najwyżej jedna strzałka, z elementem początkowym $\mathbf{𝟎}$, końcowym $\mathbf{𝟏}$, produktami (infima binarne: $\wedge$) i koproduktami (suprema: $\vee$). Krata taka jest algebrą Heytinga wtedy i tylko wtedy, gdy istnieje operacja $\Rightarrow$ taka, że

$x\Rightarrow y=\bigvee \{z\in L\mid z\wedge x\le y\}$

dla każdego $x,y\in L$. Ta definicja da się przepisać następująco:

$z\le x\Rightarrow y⟺z\wedge x\le y$

co w terminach kategoryjnych oznacza, ze istnieje bijekcja pomiędzy strzałkami ${\mathrm{H}\mathrm{o}\mathrm{m}}_L(z,x\Rightarrow y)$ i strzałkami $\mathrm{H}\mathrm{o}\mathrm{m}(z\wedge x,y)$. A ten warunek jest dokładnie warunkiem uniwersalnym dla elementu $x\Rightarrow y$ traktowanego jako eksponent!

A zatem: algebra Heytinga to poset z elementem najmniejszym, który jako kategoria jest kartezjańsko zamknięty. Warto zapamiętać tę charakteryzację.

Ponieważ:

Fakt 4.11

W dowolnej algebrze Boole'a mamy: $z\le (\mathrm{\neg }x\vee y)⟺z\wedge x\le y$

więc każda algebra Boole'a jest algebrą Heytinga. Można też pokazać, że:

Fakt 4.12

W dowolnej algebrze Heytinga $L$, jeśli dla $x\in L$ istnieje $\mathrm{\neg }x$, to musi być $\mathrm{\neg }x=x\Rightarrow \mathbf{𝟎}$.

Kartezjańska zamkniętość algebr Heytinga daje nam natychmiast następujące równości (które w innych kategoriach są izomorfizmami) i nierówności (czyli istnienie odpowiednich strzałek) - porównaj Zadanie 4.3:

Fakt 4.13

W dowolnej algebrze Heytinga zachodzą zależności: $x\le (y\Rightarrow (x\wedge y))$ $y\wedge (y\Rightarrow x)\le x$ $(x\Rightarrow \mathbf{𝟏})=\mathbf{𝟏}$ $(\mathbf{𝟏}\Rightarrow x)=x$ $(y\wedge z)\Rightarrow x=(z\Rightarrow (y\Rightarrow x))$ $(x\Rightarrow (y\wedge z))=(x\Rightarrow y)\wedge (x\Rightarrow z)$ $\mathbf{𝟏}\le x\Rightarrow x$ $\mathbf{𝟏}\le (x\Rightarrow (y\Rightarrow x))$ $\mathbf{𝟏}\le (x\Rightarrow (y\Rightarrow z))\Rightarrow ((x\Rightarrow y)\Rightarrow (x\Rightarrow z))$

Powyższe własności doprowadzają nas do najważniejszego wniosku w tym podrozdziale: algebry Heytinga są algebraicznym odpowiednikiem rachunku intuicjonistycznej logiki zdaniowej. Naszkicujmy tę odpowiedniość w obie strony: dla danej algebry Heytinga $(L,\le ,\mathbf{𝟎},\mathbf{𝟏},\wedge ,\vee ,\Rightarrow )$ traktujemy elementy $x\in L$ jako zmienne, $\le$ jako syntaktyczną relację dedukcji $⊢$, $\mathbf{𝟎}$, $\mathbf{𝟏}$ jako stałe fałsz i prawda, zaś operacje $\wedge ,\vee ,\Rightarrow$ jako spójniki zdaniowe. Wówczas taki system jest rachunkiem zdaniowym logiki intuicjonistycznej.

Odwrotnie, załóżmy, że mamy dany język zdaniowy, intuicjonistyczny, ${ℒ}$, składający się ze zmiennych zdaniowych $x,y,z,..$, z których za pomocą spójników $\wedge ,\vee ,\Rightarrow$ i stałych $\mathbf{𝟎},\mathbf{𝟏}$ tworzymy w znany sposób zdania $p,q,r,..$ oraz z syntaktycznej relacji dedukcji $⊢$ podlegającej aksjomatom:

• $⊢$ jest zwrotna i przechodnia,
• $p⊢\mathbf{𝟏}$,
• $\mathbf{𝟎}⊢p$,
• $p⊢q$ i $p⊢r$ wtedy i tylko wtedy, gdy $p⊢q\wedge r$,
• $p⊢r$ i $q⊢r$ wtedy i tylko wtedy, gdy $p\vee q⊢r$,
• $p\wedge q⊢r$ wtedy i tylko wtedy, gdy $p⊢q\Rightarrow r$.

Wówczas z ${ℒ}$ tworzymy algebrę $H({ℒ})$, tzw. algebrę Lindenbauma - Tarskiego składającą się z klas abstrakcji $[p]$ relacji równoważności $=$ danej przez

$[p]=[q]⟺p⊣⊢q$

Algebra $H({ℒ})$ jest częściowym porządkiem:

$[p]\le [q]:⟺p⊢q$

z elementem największym $[\mathbf{𝟏}]$ i najmniejszym $[\mathbf{𝟎}]$. Operacje algebry są zadane jako: $[p]\wedge [q]:=[p\wedge q]$, i tak samo dla $\vee$ oraz $\Rightarrow$. Tak utworzona algebra $H({ℒ})$ jest algebrą Heytinga, która - co więcej - ma tę własność, że zdanie $p$ można udowodnić w ${ℒ}$ wtedy i tylko wtedy, gdy $[p]=\mathbf{𝟏}$ w $H({ℒ})$.

Kategorie kartezjańsko zamknięte a lambda rachunek

Oczywiście można i trzeba sobie zadać pytanie: skoro algebry Heytinga są algebraicznym równoważnikiem zdaniowego rachunku logiki intuicjonistycznej, to czy ten fenomen przenosi się na ogólne kategorie kartezjańsko zamknięte? Pytamy zatem: jaki język odpowiada dowolnej kategorii kartezjańsko zamkniętej $\mathbf{𝐂}$? Nie dość, że pytanie jest dobrze postawione, co się okaże za chwilę, to jeszcze ma bardzo satysfakcjonującą odpowiedź: tym językiem jest rachunek lambda! W rzeczywistości struktury: kategorii kartezjańsko zamkniętej i lambda rachunku, są dwoma odbiciami tego samego zjawiska, czy też - jeśli ktoś woli inną poetykę - kategorie k.z. i $\lambda$-rachunek są dwiema manifestacjami tej samej struktury matematycznej. Poniżej spróbujemy wykazać tą tezę w kilku krokach:

• Po pierwsze, pokażmy, że dla $\lambda$-rachunku kategoria $\mathbf{𝐂}(\lambda )$, zdefiniowana w Zadaniu 1.11, wzbogacona o obiekt końcowy (który zawsze łatwo dodać), jest kartezjańsko zamknięta. Widzieliśmy już w podrozdziale nt. produktów, że ta kategoria posiada produkty. Pokażemy zatem, że posiada eksponenty. Oczywiście $[A,B]:=A\to B$ dla typów $A,B$, zaś ewaluacja i odwrotność kuryfikacji są zdefiniowane, jak następuje:

$\mathrm{e}\mathrm{v}:=\lambda z.{\pi }_1(z){\pi }_2(z):[A,B]\times A\to B$ $\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f):=\lambda z.\lambda x.f(z,x):Z\to [A,B]$

gdzie $z:Z,x:A$. Wtedy - pamiętając, że

$g\times h=\lambda w.⟨g{\pi }_1(w),h{\pi }_2(w)⟩$

mamy:

$\mathrm{e}\mathrm{v}\circ (\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)\times 1_A)=\lambda v.(\lambda z.{\pi }_1(z){\pi }_2(z))(\lambda w.⟨(\lambda y.\lambda x.f(y,x)){\pi }_1(w),(\lambda u.u){\pi }_2(w)⟩)v=\lambda v.(\lambda z.{\pi }_1(z){\pi }_2(z))(⟨\lambda x.f({\pi }_1(v),x),{\pi }_2(v)⟩)=\lambda v.(\lambda x.f({\pi }_1(v),x)){\pi }_2(v)=\lambda v.f({\pi }_1(v),{\pi }_2(v))=\lambda v.fv=f$

Naszkicowaliśmy zatem dowód, że $\mathbf{𝐂}(\lambda )$ jest kategorią kartezjańsko zamkniętą.

• Odwrotnie, mając daną kategorię kartezjańsko zamkniętą $\mathbf{𝐂}$, definiujemy język ${ℒ}(\mathbf{𝐂})$ jak następuje: typy to obiekty $\mathbf{𝐂}$; termy typu $A\to B$ to strzałki typu $A\to B$; termy proste typu $A$ to strzałki typu $\mathbf{𝟏}\to A$; równania języka ${ℒ}(\mathbf{𝐂})$ to znane równania w $\mathbf{𝐂}$, m.in. te wynikające z kartezjańskiej zamkniętości, np.:

$\lambda x.{\pi }_1(x)=p_1$ $\lambda x.{\pi }_2(x)=p_2$ $\lambda y.f(x,y)=\mathrm{c}\mathrm{u}\mathrm{r}\mathrm{r}\mathrm{y}(f)(x)$

i tak dalej.

• Dwie opisane powyżej konstrukcje są w ścisłym sensie odwrotne do siebie, ponieważ możemy udowodnić, że $\mathbf{𝐂}({ℒ}(\mathbf{𝐂}))\cong \mathbf{𝐂}$, tzn. kategorie $\mathbf{𝐂}(\lambda (\mathbf{𝐂}))$ i $\mathbf{𝐂}$ są izmorficzne oraz że języki $\lambda$ i ${ℒ}(\mathbf{𝐂}(\lambda ))$ są sobie równoważne w sensie, który jest dokładnie przedyskutowany w książce J.Lambeka i O. Scotta pt. Introduction to Higher-Order Categorical Logic, Cambridge University Press, 1986.