Tekst źródłowy strony Teoria kategorii dla informatyków/Wykład 4: Zaawansowane konstrukcje uniwersalne

{{kotwica|wyklad4|}}

==Eksponent==

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

{{wzor|mod4:eq:bij|4.1|<math>\mathbf{Set}(Z\times A,B)\cong \mathbf{Set}(Z,B^A)</math>}}

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

<center>[[Grafika:tk-4.1.png]]</center>

gdzie <math>\mathrm{ev}\colon B^A\times A\to B</math> jest '''ewaluacją''' definiowaną jako <math>\mathrm{ev}(f,a) := f(a)</math>. Rzeczywiście:

<center><math>(\mathrm{ev}\circ (\mathrm{curry}(f)\times 1_A))(z,a)= \mathrm{ev}(\mathrm{curry}(f)(z),a)=\mathrm{ev}(f(z,-),a)=f(z,a)</math></center>

albo w końcu:

<center><math>\mathrm{ev}\circ (\mathrm{curry}(f)\times 1_A)=f</math></center>

Powyższe rozważania mają sens nie tylko w <math>\mathbf{Set}</math>, ale i w każdej kategorii z produktami. Otrzymujemy więc następującą definicję:


{{definicja|4.1 [eksponent]|mod4:def:ekspo|
Niech <math>\mathbf{C}</math> będzie kategorią z produktami. '''Eksponentem''' obiektów <math>A</math> i <math>B</math> w <math>\mathbf{C}</math> jest obiekt <math>[A,B]\in \mathbf{C}_0</math> wraz ze strzałką <math>\mathrm{ev}\colon [A,B]\times A\to B</math>, nazywaną '''ewaluacją''', taką że dla dowolnego obiektu <math>Z\in \mathbf{C}_0</math> i strzałki <math>f\colon Z\times A\to B</math> istnieje dokładnie jedna strzałka <math>\mathrm{curry}(f)\colon Z\to [A,B]</math> spełniająca równanie:

<center><math>\mathrm{ev}\circ (\mathrm{curry}(f)\times 1_A) = f</math></center>

wyrażone na diagramie jako:

<center>[[Grafika:tk-4.2.png]]</center>
}}

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

Zauważmy, że dla dowolnej strzałki <math>g\colon Z\to [A,B]</math> możemy zdefiniować jej odwrotność jako 

<center><math>\mathrm{uncurry}(g) := \mathrm{ev}\circ (g\times 1_A)\colon Z\times A\to B</math></center>

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

<center><math>\mathrm{curry}(\mathrm{uncurry}(g))=g</math></center>

oraz dla dowolnej <math>f\colon Z\times A\to B</math> komutowanie powyższego diagramu natychmiast implikuje, że:

<center><math>\mathrm{uncurry}(\mathrm{curry}(f))= f</math></center>

Pokazaliśmy więc izomorfizm:

{{wzor|mod4:eq:expizo|4.2|<math>\mathrm{Hom}_{\mathbf{C}}(Z\times A, B)\cong \mathrm{Hom}_{\mathbf{C}}(Z, [A,B])</math>,}}

który uogólnia izomorfizm [[Teoria_kategorii_dla_informatyków/Wykład_4:_Zaawansowane_konstrukcje_uniwersalne#mod4:eq:bij|(4.1)]] dla <math>\mathbf{Set}</math>.

==Kategorie kartezjańsko zamknięte==
{{kotwica|mod4:subsection:ccc|}}

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


{{definicja|4.2|mod4:def:ccc| Kategoria <math>\mathbf{C}</math> jest '''kartezjańsko zamknięta''', jeśli posiada obiekt końcowy, produkty binarne i eksponenty.}}


Oto przykłady:
* <math>\mathbf{Set}</math> jest kartezjańsko zamknięta. Podobnie <math>\mathbf{Set}_{fin}</math>, gdyż konstrukcje są takie same, jak dla <math>\mathbf{Set}</math>, a eksponent <math>[A,B]</math> dla zbiorów skończonych jest zbiorem skończonym.
* Kategoria <math>\mathbf{Pos}</math> jest kartezjańsko zamknięta. Produkt dwóch posetów <math>(P, \leq)\times (Q,\leq)</math> definiuje się jako produkt zbiorów <math>P\times Q</math> wraz z relacją częściowego porządku po współrzędnych: <math>(p_1, q_1)\leq (p_2,q_2)</math> wtedy i tylko wtedy, gdy <math>(p_1\leq p_2)\wedge(q_1\leq q_2)</math> wraz z naturalnymi projekcjami <math>\pi_P(p,q) := p</math> i <math>\pi_Q(p,q):=q</math>. Jako eksponent <math>[P,Q]</math> bierzemy zbiór wszystkich funkcji monotonicznych typu <math>P\to Q</math> wraz z porządkiem po współrzędnych: <math>f \sqsubseteq g\iff \forall z\in P\ (f(z)\leq g(z))</math> Ewaluacja i kuryfikacja są definiowane tak jak w <math>\mathbf{Set}</math>, wystarczy więc sprawdzić, że  są monotoniczne. Jeśli <math>(f,p)\leq (q,r)</math> w <math>[P,Q]\times P</math>, to <math>\mathrm{ev}(f,p)=f(p)\leq g(p)\leq g(r)=\mathrm{ev}(g,r)</math> a zatem ewaluacja jest monotoniczna. Natomiast dla <math>f\colon Z\times P\to Q</math>, <math>z\sqsubseteq z'</math>, <math>p\in P</math> mamy <math>\mathrm{curry}(f)(z)(p)=f(z,p)\leq f(z',p)=\mathrm{curry}(f)(z')(p)</math> co świadczy o tym, że <math>\mathrm{curry}(f)(z)\leq\mathrm{curry}(f)(z')</math>, czyli że kuryfikacja jest monotoniczna dla każdej funkcji <math>f</math>.
* Dwie ważne dla semantyki języków programowania kategorie kartezjańsko zamknięte: kategorię posetów zupełnych <math>\mathbf{Dcpo}</math> i kategorię bc-dziedzin <math>\mathbf{BC}</math> omawiamy oddzielnie w Wykładzie [[Teoria_kategorii_dla_informatyków/Wykład_13:_Teoria_dziedzin_II#wyklad13|13]].
* Poset <math>(P,\leq)</math> z elementem najmniejszym <math>0</math> jako kategoria jest kartezjańsko zamknięty wtedy i tylko wtedy, gdy jest '''algebrą Heytinga''', zobacz podrozdział [[Teoria_kategorii_dla_informatyków/Wykład_4:_Zaawansowane_konstrukcje_uniwersalne#mod4:subsection:algHey|nt. algebr Heytinga]].
* <math>\mathbf{Cat}</math> - kategoria wszystkich małych kategorii - jest kartezjańsko zamknięta.
* Dla dowolnej małej kategorii <math>\mathbf{C}</math> kategoria funktorów <math>[\mathbf{C}^{op},\mathbf{Set}]</math> jest kartezjańsko zamknięta. Do tego przykładu wrócimy w Wykładach [[Teoria_kategorii_dla_informatyków//Wykład_7:_Lemat_Yonedy_i_funktory_reprezentowalne#wyklad7|7]] i [[Teoria_kategorii_dla_informatyków/Wykład_8:_Diagramy,_granice_i_kogranice#wyklad8|8]].
* Kartezjańsko zamknięte ''nie'' są: <math>\mathbf{Vect}</math>, <math>\mathbf{Ab}</math>, <math>\mathbf{Top}</math>, <math>\mathbf{Met}</math>, ... z różnych przyczyn.

==Algebry Heytinga==
{{kotwica|mod4:subsection:algHey|}}

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

{{stwierdzenie|4.3|mod4:prop:krata| Niech <math>L</math> będzie zbiorem z operacjami:

<center><math>\wedge\colon L\times L\to L</math></center>

<center><math>\vee\colon L\times L\to L</math></center>

<center><math>\mathbf{0}\colon 1\to L</math></center>

<center><math>\mathbf{1}\colon 1\to L</math></center>

gdzie <math>\wedge</math> i <math>\vee</math> są łączne i przemienne oraz spełniają następujące aksjomaty:

<center><math>x\wedge x=x</math></center>

<center><math>x\vee x=x</math></center>

<center><math>\mathbf{1}\wedge x=x</math></center>

<center><math>\mathbf{0}\vee x = x</math></center>

<center><math>x\wedge(y\vee x)=x=(x\wedge y)\vee x</math></center>

dla dowolnych <math>x,y,z\in L</math>. Wówczas <math>(L,\leq)</math> jest kratą, gdzie <math>\leq</math> definiujemy jako

<center><math>x\leq y\iff x=x\wedge y</math></center>

lub równoważnie:

<center><math>x\leq y\iff y=x\vee y</math></center>
}} 

Oczywiście twierdzenie odwrotne też zachodzi.

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

{{definicja|4.4|mod4:def:dist| Kratę <math>(L,\leq)</math> nazywamy dystrybutywną, jeśli dla dowolnych <math>x,y,z\in L</math> zachodzi 

<center><math>x\wedge(y\vee z) = (x\wedge y)\vee (x\wedge z)</math></center>
}}

{{fakt|4.5|mod4:fact:A|Powyższa równość w definicji implikuje równość dualną:

<center><math>x\vee(y\wedge z)=(x\vee y)\wedge (x\vee z)</math></center>
}}


{{definicja|4.6|mod4:def:przeciwny| Elementem przeciwnym do <math>x</math> w kracie <math>L</math> nazywamy element <math>a\in L</math> taki, że <math>x\wedge a =\mathbf{0}</math> i <math>x\vee a=\mathbf{1}</math>.}}


{{fakt|4.7|mod4:fact:B| W kracie dystrybutywnej element przeciwny do <math>x</math> jest jedyny. Oznaczamy go wówczas jako <math>\neg x</math>.}}


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


{{definicja|4.8 [algebra Boole'a]|mod4:def:Boole| Algebrą Boole'a nazywamy kratę dystrybutywną, w której każdy element <math>x</math> ma element przeciwny.}}


{{fakt|4.9|mod4:fact:C|
W dowolnej algebrze Boole'a <math>L</math> zachodzą równości:

<center><math>\neg (x\vee y) = \neg x \wedge \neg y</math></center>

<center><math>\neg (x\wedge y)=\neg x\vee \neg y</math></center>

<center><math>\neg \neg x = x</math></center>

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]|mod4:def:Heyting|Algebrą Heytinga nazywamy kratę <math>(L,\leq)</math> z elementem najmniejszym <math>\mathbf{0}</math>, elementem największym <math>\mathbf{1}</math> i operacją <math>\Rightarrow\colon L\times L\to L</math> definiowaną dla każdej pary elementów <math>x,y\in L</math> jako: 

<center><math>x\Rightarrow y := \bigvee\{ z\in L\mid z\wedge x\leq y\}</math></center>
}}

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ę <math>(L,\leq,\mathbf{0},\mathbf{1})</math> 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 <math>\mathbf{0}</math>, końcowym <math>\mathbf{1}</math>, produktami (infima binarne: <math>\wedge</math>) i koproduktami (suprema: <math>\vee</math>). Krata taka jest algebrą Heytinga wtedy i tylko wtedy, gdy istnieje operacja <math>\Rightarrow</math> taka, że

<center><math>x\Rightarrow y = \bigvee\{ z\in L\mid z\wedge x\leq y\}</math></center>

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

<center><math>z\leq x\Rightarrow y\ \iff \ z\wedge x \leq y</math></center>

co w terminach kategoryjnych oznacza, ze istnieje bijekcja pomiędzy strzałkami <math>\mathrm{Hom}_L(z,x\Rightarrow y)</math> i strzałkami <math>\mathrm{Hom}(z\wedge x,y)</math>. A ten warunek jest dokładnie warunkiem uniwersalnym dla elementu <math>x\Rightarrow y</math> 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|mod4:fact:D| W dowolnej algebrze Boole'a mamy:

<center><math>z\leq (\neg x\vee y)\iff z\wedge x\leq y</math></center>
}}


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


{{fakt|4.12|mod4:fact:E|W dowolnej algebrze Heytinga <math>L</math>, jeśli dla <math>x\in L</math> istnieje <math>\neg x</math>, to musi być <math>\neg x = x\Rightarrow \mathbf{0}</math>.}}


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 [[Teoria_kategorii_dla_informatyków/Ćwiczenia_4:_Zaawansowane_konstrukcje_uniwersalne#mod4:zad3|Zadanie 4.3]]:


{{fakt|4.13|mod4:fact:F|W dowolnej algebrze Heytinga zachodzą zależności:

<center><math>x\leq (y\Rightarrow (x\wedge y))</math></center>

<center><math>y\wedge (y\Rightarrow x)\leq x</math></center>

<center><math>(x\Rightarrow \mathbf{1})=\mathbf{1}</math></center>

<center><math>(\mathbf{1}\Rightarrow x)=x</math></center>

<center><math>(y\wedge z)\Rightarrow x = (z\Rightarrow (y\Rightarrow x))</math></center>

<center><math>(x\Rightarrow (y\wedge z))=(x\Rightarrow y)\wedge (x\Rightarrow z)</math></center>

<center><math>\mathbf{1}\leq x\Rightarrow x</math></center>

<center><math>\mathbf{1}\leq (x\Rightarrow (y\Rightarrow x))</math></center>

<center><math>\mathbf{1}\leq (x\Rightarrow (y\Rightarrow z))\Rightarrow ((x\Rightarrow y)\Rightarrow (x\Rightarrow z))</math></center>
}}


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 <math>(L,\leq, \mathbf{0},\mathbf{1}, \wedge,\vee,\Rightarrow)</math> traktujemy elementy <math>x\in L</math> jako zmienne, <math>\leq</math> jako syntaktyczną relację dedukcji <math>\vdash</math>, <math>\mathbf{0}</math>, <math>\mathbf{1}</math> jako stałe fałsz i prawda, zaś operacje <math>\wedge, \vee, \Rightarrow</math> jako spójniki zdaniowe. Wówczas taki system jest rachunkiem zdaniowym logiki intuicjonistycznej. 

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

* <math>\vdash</math> jest zwrotna i przechodnia,
* <math>p\vdash \mathbf{1}</math>,
* <math>\mathbf{0} \vdash p</math>,
* <math>p\vdash q</math> i <math>p\vdash r</math> wtedy i tylko wtedy, gdy <math>p\vdash q\wedge r</math>,
* <math>p\vdash r</math> i <math>q\vdash r</math> wtedy i tylko wtedy, gdy <math>p\vee q\vdash r</math>,
* <math>p\wedge q\vdash r</math> wtedy i tylko wtedy, gdy <math>p\vdash q\Rightarrow r</math>.

Wówczas z <math>\mathcal{L}</math> tworzymy algebrę <math>H(\mathcal{L})</math>, tzw. '''algebrę Lindenbauma - Tarskiego''' składającą się z klas abstrakcji <math>[p]</math> relacji równoważności <math>=</math> danej przez 

<center><math>[p]=[q] \ \iff \ p\dashv\vdash q</math></center>

Algebra <math>H(\mathcal{L})</math> jest częściowym porządkiem:

<center><math>[p]\leq [q] \ :\iff \ p\vdash q</math></center>

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

==Kategorie kartezjańsko zamknięte a lambda rachunek==
{{kotwica|mod4:subsection:ccclambda|}}

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 <math>\mathbf{C}</math>? 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 <math>\lambda</math>-rachunek są dwiema manifestacjami tej samej struktury matematycznej. Poniżej spróbujemy wykazać tą tezę w kilku krokach:

* Po pierwsze, pokażmy, że dla <math>\lambda</math>-rachunku kategoria <math>\mathbf{C}(\lambda)</math>, zdefiniowana w  [[Teoria_kategorii_dla_informatyków/Ćwiczenia_1:_Teoria_kategorii_jako_abstrakcyjna_teoria_funkcji#mod1:zad11|Zadaniu 1.11]], wzbogacona o obiekt końcowy (który zawsze łatwo dodać), jest kartezjańsko zamknięta. Widzieliśmy już w [[Teoria_kategorii_dla_informatyków/Wykład_3:_Zasada_dualności_i_proste_konstrukcje_uniwersalne#mod3:subsection:prodikoprod|podrozdziale nt. produktów]], że ta kategoria posiada produkty. Pokażemy zatem, że posiada eksponenty. Oczywiście <math>[A,B] := A\to B</math> dla typów <math>A,B</math>, zaś ewaluacja i odwrotność kuryfikacji są zdefiniowane, jak następuje:

<center><math>\mathrm{ev} := \lambda z.\pi_1(z)\pi_2(z)\colon [A,B]\times A\to B</math></center>

<center><math>\mathrm{uncurry}(f) := \lambda z.\lambda x.f(z,x)\colon Z\to [A,B]</math></center>

gdzie <math>z:Z,x:A</math>. Wtedy - pamiętając, że 

<center><math>g\times h = \lambda w. \langle g\pi_1(w),h\pi_2(w)\rangle</math></center>

mamy:

<center><math>\mathrm{ev}\circ (\mathrm{curry}(f)\times 1_A) = \lambda v. (\lambda z.\pi_1(z)\pi_2(z))(\lambda w.\langle (\lambda y.\lambda x.f(y,x))\pi_1(w), (\lambda u.u)\pi_2(w)\rangle)v = \lambda v. (\lambda z.\pi_1(z)\pi_2(z))(\langle\lambda x.f(\pi_1(v),x),\pi_2(v)\rangle) = \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</math></center>

Naszkicowaliśmy zatem dowód, że <math>\mathbf{C}(\lambda)</math> jest kategorią kartezjańsko zamkniętą. 
* Odwrotnie, mając daną kategorię kartezjańsko zamkniętą <math>\mathbf{C}</math>, definiujemy język <math>\mathcal{L}(\mathbf{C})</math> jak następuje: typy to obiekty <math>\mathbf{C}</math>; termy typu <math>A\to B</math> to strzałki typu <math>A\to B</math>; termy proste typu <math>A</math> to strzałki typu <math>\mathbf{1}\to A</math>; równania języka <math>\mathcal{L}(\mathbf{C})</math> to znane równania w <math>\mathbf{C}</math>, m.in. te wynikające z kartezjańskiej zamkniętości, np.: 

<center><math>\lambda x.\pi_1(x) = p_1</math></center>

<center><math>\lambda x.\pi_2(x) = p_2</math></center>

<center><math>\lambda y.f(x,y) = \mathrm{curry}(f)(x)</math></center>

i tak dalej. 
* Dwie opisane powyżej konstrukcje są w ścisłym sensie odwrotne do siebie, ponieważ możemy udowodnić, że <math>\mathbf{C}(\mathcal{L}(\mathbf{C}))\cong \mathbf{C}</math>, tzn. kategorie <math>\mathbf{C}(\lambda(\mathbf{C}))</math> i <math>\mathbf{C}</math> są izmorficzne oraz że języki <math>\lambda</math> i <math>\mathcal{L}(\mathbf{C}(\lambda))</math> 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.