Analiza i konstrukcje systemów logicznych w ujęciu teorii kategorii
Michal R. Przybylek
1 Wstęp
Główne zestawy narzędzi i metodyk do radzenia sobie z logiką można po- dzielić na dwie grupy: te z podejścia teorio-dowodowego — w którym logikę traktujemy jako pewnego rodzaju system dedukcyjny (kategorię) oraz te z podejścia teorio-modelowego — w którym logikę stanowi relacja spełniania pomiędzy klasą modeli, a klasą formuł nad wspólnym językiem. Te dwa niezależne podejścia występują często łącznie. Definiując logikę jako system dedukcyjny (jak dzieje się to np. w logikach intuicjonistycznych, liniowych, czy temporalnych), ważnym zadaniem staje się znalezienie „właściwej” klasy modeli, nad którą dany system logiczny jest poprawny (i najlepiej pełny).
Podobnie, definiując logikę jako relację pomiędzy modelami i formułami (jak dzieje się np. w klasycznej logice), ważnym zadaniem jest znalezienie popraw- nego (i najlepiej pełnego) systemu dedukcyjnego.
Pojęciem łączącym obydwa wspomniane wyżej podejścia jest pojęcie sys- temu logicznego. W najprostszym ujęciu przez system logiczny można rozu- mieć trójkę: zbiór częściowo-uporządkowany (poset — ang. partially ordered set) hSen, ≤Seni, gdzie Sen nazywamy zbiorem zdań, częściowo-uporządkowany zbiór (lub klasę) hMod , ≤Modi, gdzie Mod nazywamy zbiorem (klasą) modeli, oraz relację spełniania |= ⊆ Mod × Sen kompatybilną z częściowymi po- rządkami ≤Sen i ≤Mod:
M |= φ, N ≤Mod M, φ ≤Sen ψ ⇒ N |= ψ
Przykład 1.1 (Logika zdań). Niech hSen, `i będzie zbiorem formuł rachunku zdań nad zbiorem zmiennych zdaniowych Var uporządkowanym przez relację dowodliwości ` w klasycznej logice , tj.: dla dowolnych formuł φ, ψ ∈ Sen
zachodzi:
φ ` ψ
wtedy i tylko wtedy gdy φ dowodzi ψ. Przyjmijmy, że Mod jest klasą par hB, νi, gdzie B jest algebrą Boola, natomiast ν jest wartościowaniem zmien- nych Var w algebrę B. Wtedy relacja spełniania |= ⊆ Mod × Sen zdefi- niowana dla dowolnej formuły φ ∈ Sen i dowolnej algebry Boola B wraz z wartościowaniem ν : Var → B:
hB, νi |= φ
wtedy i tylko wtedy gdy ν#(φ) daje wartość > w algebrze B, gdzie ν# jest indukcyjnym rozszerzeniem ν na zbiór wszystkich formuł φ, ψ ∈ Sen:
ν#(X ∈ Var ) = ν(X) ν#(>) = >
ν#(⊥) = ⊥
ν#(φ ∧ ψ) = ν#(φ) ∧ ν#(ψ) ν#(φ ∨ ψ) = ν#(φ) ∨ ν#(ψ) ν#(φ ⇒ ψ) = ν#(φ) ⇒ ν#(ψ) tworzy system logiczny wraz z hSen, `i i hMod , =i.
Przykład 1.2 (Struktura Kripkego). Niech hSen, =i będzie zbiorem formuł rachunku zdań jak w poprzednim przykładzie, ale tym razem z trywialnym częściowym-porządkiem zadawanym przez równość =. Niech hMod , ≥i będzie dowolnym zbiorem częściowo-uporządkowanym. Struktura Kripkego to sys- tem logiczny pomiędzy hSen, =i a hMod, ≥i spełniający następujące wa- runki dla dowolnych p, q ∈ Mod oraz φ, ψ ∈ Sen:
• (ekstensjonalna prawda) p > jest zawsze prawdziwe
• (ekstensjonalny fałsz) p ⊥ nigdy nie jest prawdziwe
• (ekstensjonalna koniunkcja) p φ ∧ ψ witw. p φ i p ψ
• (ekstensjonalna dysjunkcja) p φ ∨ ψ witw. p φ lub p ψ
• (ekstensjonalna implikacja) p φ ⇒ ψ witw. dla każdego q ≥ p zacho- dzi: q φ implikuje q ψ
Taki system logiczny może być rozszerzony do systemu logicznego pomiędzy hSen, `Ii i hMod , ≥i, gdzie dla φ, ψ ∈ Sen:
φ `I ψ
wtedy i tylko wtedy gdy dla każdego stanu p ∈ Mod zachodzi:
p φ ⇒ ψ
Zdefiniowane wyżej pojęcie systemu logicznego ma swój teorio-kategoryjny odpowiednik w postaci dystrybutora pomiędzy wzbogacanymi kategoriami.
Natomiast semantyka zadawana przez relację |= w Przykładzie 1.1, oraz se- mantyka zadawana przez relację w Przykładzie 1.2 są trywialnymi przykła- dami konwolucji Day’a dla kategorii wzbogacanych algebrą dwuelementową {0 ≤ 1}. Nietrywialnym przykładem konwolucji Day’a są semantyki logik podstrukturalnych (jak np. logika liniowa) w trójkratach.
Przykład 1.3 (Semantyka w trójkratach). Trójkrata to para uporządkowana hX, Ri, gdzie X jest zbiorem, a R : X × X × X → 2 jest trójargumentową relacją na zbiorze X. Niech Σ będzie sygnaturą składającą się z trzech bi- narnych symboli ⊗, (, orazL ( i oznaczmy przez L algebrę termów z ΣR nad zbiorem zmiennych Var . Semantyka L w trójkracie hX, Ri to relacja ⊆ X × L spełniająca:
• x φ ⊗ ψ witw. istnieją y, z ∈ X takie, że:
y φ ∧ z ψ ∧ R(x, y, z)
• y φ ( ψ witw. dla każdych x, z ∈ X zachodzi:L z φ ∧ R(x, y, z) ⇒ x ψ
• z φ( ψ witw. dla każdych x, y ∈ X zachodzi:R y φ ∧ R(x, y, z) ⇒ x ψ
Dla zbioru częściowo-uporządkowanego hX, ≤i reguły semantyki w trójkracie:
R(x, y, z) ⇔ x ≤ y ∧ x ≤ z
odpowiadają regułom ekstensjonalnej koniunkcji i ekstensjonalnej implikacji z semantyki Kripkego.
Tak więc zarówno pojęcie klasycznej semantyki w algebrach Boola, se- mantyki Kripkego dla logiki intuicjonistycznej jak i pojęcie semantyki w trójkratach dla logik podstrukturalnych można otrzymać „za darmo” jako rodzaj konwolucji Day’a. Celem rozprawy jest zbudowanie ogólnej teorii po- zwalającej na abstrakcyjne wprowadzenie pojęcia systemu logicznego, oraz zbudowanie narzędzi umożliwiających otrzymywanie „darmowych” semantyk dla rachunków lambda i ich logik.
2 Wyniki rozprawy
Niech W C
|−|//
Woo C
J będzie sprzężeniem pomiędzy kategorią C i 2-kategorią W, gdzie funktor J jest lewym sprzężonym funktora |−|. Mówimy, że takie sprzężenie wprowadza pojęcie dyskretności na W, jeżeli jedność sprzężenia jest izomorfizmem. W dalszej części kategorię C będziemy utożsamiać z jej obrazem w W i oznaczać przez Disc(W).
Przypomnijmy, że w dowolnej kartezjańskiej kategorii W każdy obiekt A ∈ W posiada jedyną (kartezjańską) komonoidalną strukturę:
1oo ! AA ∆ //A × A
gdzie ∆ = hid , id i jest morfizmem diagonalnym. Gdy W jest 2-kategorią lokalnie małych kategorii Cat, klasyczne pojęcia obiektów końcowych (po- czątkowych) oraz produktów (koproduktów) binarnych w A ∈ Cat zada- wane są przez funktory prawe (odpowiednio: lewe) sprzężone do struktury komonoidalnej na A. Analogicznie wprowadzimy pojęcie wewnętrznych (kar- tezjańskich) spójników w obiektach dowolnej kartezjańskiej 2-kategorii W.
Definicja 2.1 (Wewnętrzne (ko)kartezjańskie spójniki). Niech W będzie kar- tezjańską 2-kategorią. Powiemy, że obiekt A ∈ W ma wewnętrzną wartość końcową {•}A (początkową {}A) jeżeli jedyny morfizm A→ 1 posiada prawy! sprzężony 1 {•}→ A (odpowiednio: lewy sprzężony 1A {}→ A ). Powiemy także,A że A ∈ W ma wewnętrzne binarne produkty ×A (koprodukty tA) jeżeli mor- fizm diagonalny A ∆→ A × A posiada prawy sprzężony A × AA ×→ A (odpo-A wiednio: lewy sprzężony A × At→ A ).A
Wprowadzenie wewnętrznie domkniętych spójników jest już mniej oczy- wiste. Mark Weber w pracy [1] próbował zrobić to w następujący spo-
sób: obiekt A z kartezjańskiej 2-kategorii jest wewnętrznie kartezjańsko do- mknięty, jeżeli posiada wewnętrzne produkty ×Aoraz dla każdego globalnego elementu 1 → A morfizm:x
A idA×x //A × A ×A//A
posiada prawy sprzężony. Niestety, taka definicja jest nieadekwatna w wielu kontekstach i nie pokrywa się z klasycznymi definicjami dla kartezjańsko do- mkniętych wewnętrznych kategorii, czy kartezjańsko domkniętych rozwłók- nień. Proponujemy inną definicję.
Definicja 2.2 (Wewnętrzna kartezjańska domkniętość). Niech W będzie kar- tezjańską 2-kategorią z pojęciem dyskretności. Powiemy, że obiekt A ∈ W jest wewnętrznie kartezjańsko domknięty jeżeli posiada wewnętrzne produkty, oraz morfizm:
A × |A| h×A◦(id ×A),π|A|i //A × |A|
posiada prawy sprzężony, gdzie A jest kojednością sprzężenia zadającego dys- kretność na W.
A później rozszerzamy ją na monoidalne 2-kategorie z monoidalną notacją dyskretności (tj. kategoria obiektów dyskretnych jest kartezjańska, a funktor włożenia jest op-luźnym funktorem monoidalnym).
Pokazujemy następujące twierdzenie.
Twierdzenie 2.3 (Parametryzowany rachunek lambda z prostym systemem typów). Niech W będzie kartezjańską 2-kategorią z notacją dyskretności. Za- łóżmy, że obiekt A ∈ W jest wewnętrznie kartezjańsko domknięty. Wtedy dla każdego dyskretnego obiektu X ∈ Disc(W) kategoria homW(X, A) jest kartezjańsko domknięta. Ponadto, jeżeli A ma wewnętrzne koprodukty, to kategoria homW(X, A) także posiada koprodukty.
Wprowadzamy także pojęcie parametrycznych (ko)produktów jako pra- wych (odpowiednio: lewych) rozszerzeń Kana.
Definicja 2.4 (Parametryczne (ko)produkty). Niech W będzie 2-kategorią.
Rozważmy obiekt A ∈ W, oraz morfizm s : X → Y ∈ W. Parametryczny ele- ment τX: X → A ma koprodukt wzdłuż s jeżeli istnieje prawe (odpowiednio:
lewe) rozszerzenie Kana Q
sτX (odpowiednio: `
sτX) τX wzdłuż s. Ponadto, będziemy nazywac taki (ko)produkt stabilnym, jeżeli rozszerzenie Kana jest stabilne pod obiektami przecinkowymi.
Jeżeli 2-kategoria W posiada pojęcie dyskretności, to (ko)produkty para- metryzowane dyskretnymi obiektami nazywamy obiektami polimorficznymi.
Aby uzasadnić sensowność zdefiniowanych w rozprawie wewnętrznych spójników i parametrycznych (ko)produktów, wprowadzamy kategorie sto- warzyszone z obiektami skończenie zupełnej 2-kategorii posiadającej pojęcie dyskretności.
Twierdzenie 2.5 (Twierdzenie o reprezentacji). Niech W będzie 2-kategorią posiadającą pojęcie dyskretności i skończone (ważone) granice. Każdemu obiektowi A ∈ W możemy przypisać Disc(W)-wewnętrzną kategorię, tzw. ka- tegorię stowarzyszoną. Co więcej, takie przyporządkowanie sprawia, że W staje się pełną (i gęstą) 2-podkategorią 2-kategorii Cat(Disc(W)) kategorii Disc(W)-wewnętrznych wtedy i tylko wtedy gdy Disc(W) jest gęstą podkate- gorią W.
Zachodzi następujące twierdzenie.
Twierdzenie 2.6 (O adekwatności wewnętrznych spójników). Niech W bę- dzie skończenie zupełną 2-kategorią posiadającą pojęcie dyskretności. Jeżeli obiekt A ∈ W ma wewnętrzne spójniki, to jego stowarzyszona kategoria ma odpowiadające spójniki w klasycznym sensie. Jeżeli dyskretne obiekty są gę- ste w W, to zachodzi także implikacja odwrotna. Ponadto, A posiada poli- morficzne (ko)produkty wtedy i tylko wtedy gdy jego stowarzyszona kategoria posiada proste (ko)produkty w klasycznym sensie.
Na tym poziomie ogólności dowodzimy twierdzenie o niezupełności bę- dące rozszerzeniem klasycznego twierdzenia Freyda o nieistnieniu małych zupełnych niezdegenerowanych kategorii.
Twierdzenie 2.7 (Twierdzenie o niezupełności). Niech W będzie lokalnie małą 2-kategorią, a G ⊂ W 2-generującą rodziną obiektów z W. Ponadto, załóżmy, że dla obiektów z G istnieją tensory ze zbiorami (tj. stałe kopro- dukty). Jeżeli dla dowolnego X ∈ G, dowolnego zbioru λ oraz dowolnej funk- cji s : λ → λ0 obiekt C ∈ W ma wszystkie produkty parametryzowane przez λ ⊗ X wzdłuż s ⊗ X, to C jest reprezentowalnie posetem — tj. dla dowolnego obiektu K ∈ W kategoria homW(K, C) jest posetem.
Jako prosty wniosek z powyższego twierdzenia otrzymujemy uogólnienie twierdzenia Freyda na kategorie wewnętrzne.
Wniosek 2.8 (Twierdzenie Freyda dla kategorii wewnętrznych). Niech C bę- dzie kategorią z tensorami (tj. ze stałymi koproduktami). Jeżeli C-wewnętrzna kategoria jest wewnętrznie zupełna, to jest ona wewnętrznym zbiorem czę- ściowo uporządkowanym.
Warto zwrócić uwagę, że powyższy wniosek nie ma zastosowania do efek- tywnego toposu Hylanda, ponieważ topos ten nie posiada tensorów ze zbio- rami (nie posiada nawet przeliczalnych koproduktów na obiekcie końcowym).
Wprowadzamy, kluczowe dla rozważań o abstrakcyjnych systemach lo- gicznych, pojęcie trójkąta Yonedy i jego 2-wymiarowy odpowiednik — tzw. bi- trójkąt Yonedy.
Definicja 2.9 (Trójkąt Yonedy). Niech W będzie 2-kategorią. Trójkąt Yonedy w W zapisywany η : y . hf, gi składa się z trzech morfizmów y : A → A, f : A → B i g : B → A oraz 2-morfizmu η : y → g ◦ f , który ukazuje g jako stabilne lewe rozszerzenie Kana y wzdłuż f i ukazuje f jako absolutne lewe podniesienie Kana y względem g:
{ η
A y //A
A
B
f =Liftg(y)
A
B
::
g=Lanf(y)
Struktury podobne do trójkątów Yonedy pozwalają na wprowadzenie po- jęcia „reprezentowalnych relacji” w 2-kategoriach [2].
Przy rozważaniu trójkątów Yonedy w 2-kategorii lokalnie małych (sła- bych) 2-kategorii, zasadne jest nieznaczne osłabienie powyższych warunków.
Definicja 2.10 (Bitrójkąt Yonedy). Bitrójkąt Yonedy η : Y . hF, Gi składa się z pseudofunktorów Y : A → A, F : A → B, G : B → A pomiędzy (słabymi)
2-kategoriami (tj. bikategoriami) A, A, B oraz 2-naturalnej transformacji η : Y → G ◦ F , która indukuje naturalne równoważności:
homA(Y (−2), G(−1)) ≈ homB(F (−2), −1) oraz:
homA(G(−1), −2) ≈ hom(homB(F (−3), −1), homA(Y (−3), −2))
Gdzie ostatnia równoważność powinna być intuicyjnie rozumiana jako:
G(−) ≈ Z A∈A
homB(F (A), −) × Y (A) Klasycznym przykładem bitrójkąta Yonedy jest:
η : Y : cat → Cat . hJ : cat → Dist, P : Dist → Cati
gdzie cat jest 2-kategorią małych kategorii, Cat jest 2-kategorią lokalnie małych kategorii, a Dist jest (słabą) 2-kategorią dystrybutorów. Wtedy J : cat → Dist, Y : cat → Cat są kanonicznymi włożeniami, natomiast P : Dist → Cat jest kowariantnym „2-potęgowym” pseudofunktorem Set(−)op zdefiniowanym na dystrybutorach za pomocą lewych rozszerzeń Kana, a ηA: A → SetAop włożeniem Yonedy małej kategorii A w lokalnie małą ka- tegorię SetAop. Bezpośrednio z definicji 2-kategorii Dist istnieją naturalne izomorfizmy:
homDist(A, B) ≈ homCat(A, SetBop)
gdzie A i B są małymi kategoriami. Dlatego, aby pokazać, że P jest (sła- bym) punktowym lewym rozszerzeniem Kana, wystarczy pokazać, że Y jest gęstym funktorem. Ale Y jest gęsty, bo kategoria końcowa 1 jest (2-)gęstą podkategorią Cat, a Y jest wierny i pełny.
Pokazujemy, że podobna sytuacja ma miejsce dla kategorii wewnętrznych, oraz dla kategorii wzbogacanych.
Twierdzenie 2.11 (C-wewnętrzne 2-potęgi). Niech C będzie skończenie ko- zupełną lokalnie kartezjańsko domkniętą kategorią. Istnieje wtedy bitrójkąt Yonedy
η : fam : cat(C) → CatCop . hJ : cat(C) → Dist(C), P : Dist(C) → CatCopi gdzie cat(C) jest 2-kategorią C-wewnętrznych kategorii, Dist(C) jest (słabą) 2-kategorią C-wewnętrznych dystrybutorów, J jest kanonicznym włożeniem, a:
fam : cat(C) → CatCop
jest kanoniczną eksternalizacją wewnętrznej kategorii. Pseudofunktor:
P : Dist(C) → CatCop
jest zdefiniowany następująco:
P (A) = fam(C)fam(A)op P (A9 B)F = LanyA(F )
gdzie fam(C) jest ścisłą kategorią indeksowaną odpowiadającą fundamental- nemu (tj. kodziedzinowemu) rozwłóknieniu cod (C), oraz:
yA: fam(A) → fam(C)fam(A)op
jest klasycznym wewnętrznym włożeniem Yonedy zdefiniowanym jako karte- zjańska transpozycja:
hom(−2, −1) : fam(A) × fam(A)op → fam(C)
Twierdzenie 2.12 (C-wzbogacane 2-potęgi). Niech hI, ⊗, Ci będzie zupełną i kozupełną symetryczną monoidalnie domkniętą kategorią. Istnieje wtedy bitrójkąt Yonedy:
η : Y : CatS(C) → Cat(C) . hJ : CatS(C) → Dist(C), P : Dist(C) → Cat(C)i gdzie CatS(C) jest 2-kategorią małych C-wzbogacanych kategorii, Cat(C) jest 2-kategorią wszystkich (tj. lokalnie małych) C-wzbogacanych kategorii, Dist(C) jest (słabą) 2-kategorią C-wzbogacanych dystrybutorów pomiędzy ma- łymi kategoriami, natomiast J, Y są kanonicznymi włożeniami. Pseudofunk- tor:
P : Dist(C) → Cat(C) jest zdefiniowany jako:
P (A) = CAop P (A9 B)F = LanyA(F )
gdzie yA: A → CAop jest C-wzbogacanym funktorem Yonedy.
W swojej rozprawie doktorskiej [3], Brain Day pokazał, że dla kategorii wzbogacanych pseudofunktor:
P : Dist(C) → Cat(C)
przyporządkowuje (słabym) monoidom w Dist(C) (tzw. kategoriom promo- noidalnym), (bi)domkniete monoidy w Cat(C) (tzw. kategorie monoidalne).
Jeżeli M : A ⊗ A 9 A jest C-wzbogacanym dystrybutorem, będącym częścią struktury promonoidalnej na A, to struktura (bi)monoidalnie domknięta in- dukowana jest na CAop za pomocą tzw. konwolucji:
(F ⊗M G)(−) =
Z B,C∈A
F (B) ⊗ G(C) ⊗ M (−, B, C) z lewym liniowym wykładnikiem definiowanym jako:
(F (LM G)(−) = Z
A,C∈A
G(A)F (C)⊗M (A,−,C)
i prawym liniowym wykładnikiem definiowanym jako:
(F (RM G)(−) = Z
A,B∈A
G(A)F (B)⊗M (A,B,−)
W niniejszej rozprawie, dowodzimy, że podobna sytuacja ma miejsce dla kategorii wewnętrznych.
Twierdzenie 2.13 (Wewnętrzna konwolucja). Niech C będzie skończenie ko- zupełną lokalnie kartezjańsko domkniętą kategorią. Dla dowolnego C-wewnętrznego dystrybutora µ : A × A 9 A istnieje (bi)domknięta magma na fam(C)fam(A)op. Ponadto, jeżeli µ : A × A 9 A wraz z η : 1 9 A tworzy słabą (symetryczną) strukturę monoidalną, to indukowana magma jest częścią słabej (symetrycz- nej) struktury monoidalnej.
Wyposażeni w powyższy aparat pojęciowy jesteśmy w stanie scharak- teryzować uniwersa, w których można otrzymać „darmową semantykę” na obiektach.
Definicja 2.14 (Uniwersum potęgowych semantyk). Niech η : Y . hF, Gi bę- dzie bitrójkątem Yonedy z Y : A → A, F : A → B, G : B → A, gdzie A jest monoidalną 2-kategorią z notacją dyskretności, A jest monoidalną 2-kategorią ze skończonymi koproduktami i monoidalną notacją dyskretności, a B jest monoidalną 2-kategorią. Dodatkowo załóżmy, że Y zachowuje dyskretne obiekty, Y oraz F zachowują strukturę magm, a G odwzorowuje magmy z B w we- wnętrznie (bi)domknięte magmy w A. Trójkąt η : Y . hF, Gi będziemy na- zywać uniwersum potęgowych semantyk dla magm jeżeli dla każdego V ∈ Disc(A) funktor:
FV(X) 7→ Y (V ) t (X ⊗ X) t (|X| ⊗ X) t (|X| ⊗ X) posiada algebrę początkową LambekV.
Sens powyższej definicji jest następujący — biorąc dowolny morfizm R : M ⊗ M → M w B, o którym myślimy jak o “relacji” w A, oraz dowolny morfizm |= : V → M
w B, o którym myślimy jako o wartościowaniu zmiennych V , dostajemy wolną semantykę definiowaną jako jedyny morfizm LambekV → P (M ) z algebry po- czątkowej LambekV do algebry:
Y (V )t(P (M )⊗P (M ))t(|P (M )|⊗P (M ))t(|P (M )|⊗P (M )) |=,⊗R,
(LR,(RR //P (M )
gdzie ⊗R,(LR,(RR jest wewnętrznie (bi)domkniętą magmą na P (M ) indu- kowaną przez R.
Podobnie definiujemy uniwersa potęgowe dla monoidów i w przypadku gdy obiekty postaci P (A) dla dowolnego A ∈ B posiadają wewnętrzne ko- produkty, rozszerzamy semantykę indukowaną przez algebrę początkową o wewnętrzny obiekt początkowy i wewnętrzne produkty binarne. Przykła- dami uniwersów potęgowych semantyk spełniających powyższe założenia są bitrójkąty Yonedy kategorii wzbogacanych i kategorii wewnętrznych. Oma- wiane we wstępie semantyki, są wolnymi semantykami zadawanymi przez uniwersum potęgowe kategorii wzbogacanych 2-elementową algebrą Boola {0 ≤ 1}. Przykładowo, semantyka Kripkego powstaje jako wolna seman- tyka dla trywialnej struktury komonoidalnej na częściowo uporządkowanym zbiorze Mod oraz wartościowania zmiennych .
Literatura
[1] M. Weber, Yoneda Structures from 2-toposes, Applied Categorical Struc- tures 15-3 (2007)
[2] R. Street, R. Walters, Yoneda structures on 2-categories, Journal of Pure and Applied Algebra 50 (1978)
[3] B. Day, Construction of Biclosed Categories, PhD Thesis, University of New South Wales (1970)
http://www.math.mq.edu.au/~street/DayPhD.pdf
