-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathlistisos.tex
83 lines (65 loc) · 2.87 KB
/
listisos.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
\subsection{List of isomorphisms}\label{list-of-isomorphisms}
\subsubsection{Linear negation}\label{linear-negation-1}
\(\begin{array}{rclcrcl}
A\biorth & \cong& A\\
(A\tens B)\orth & \cong& A\orth\parr B\orth & \quad& \one\orth & \cong& \bot\\
(A\parr B)\orth & \cong& A\orth\tens B\orth & \quad& \bot\orth & \cong& \one\\
(A\with B)\orth & \cong& A\orth\plus B\orth & \quad& \top\orth & \cong& \zero\\
(A\plus B)\orth & \cong& A\orth\with B\orth & \quad& \zero\orth & \cong& \top\\
(\oc A)\orth & \cong& \wn A\orth\\
(\wn A)\orth & \cong& \oc A\orth\\
\end{array}\)
\subsubsection{Neutrals}\label{neutrals}
\(\begin{array}{rclcl}
A\tens\one & \cong& \one\tens A&\cong &A\\
A\parr\bot & \cong& \bot\parr A&\cong &A\\
A\with\top & \cong& \top\with A&\cong &A\\
A\plus\zero & \cong& \zero\plus A&\cong &A\\
\end{array}\)
\subsubsection{Commutativity}\label{commutativity-1}
\(\begin{array}{rcl}
A\tens B & \cong& B\tens A\\
A\parr B & \cong& B\parr A\\
A\with B & \cong& B\with A\\
A\plus B & \cong& B\plus A\\
\end{array}\)
\subsubsection{Associativity}\label{associativity}
\(\begin{array}{rcl}
(A\tens B)\tens C & \cong& A\tens(B\tens C)\\
(A\parr B)\parr C & \cong& A\parr(B\parr C)\\
(A\with B)\with C & \cong& A\with(B\with C)\\
(A\plus B)\plus C & \cong& A\plus(B\plus C)\\
\end{array}\)
\subsubsection{Multiplicative-additive distributivity}\label{multiplicative-additive-distributivity}
\(\begin{array}{rclcrcl}
A\tens(B\plus C) & \cong& (A\tens B)\plus(A\tens C) & \quad&
A\tens\zero & \cong& \zero\\
A\parr(B\with C) & \cong& (A\parr B)\with(A\parr C) & \quad&
A\parr\top & \cong& \top\\
\end{array}\)
\subsubsection{Linear implication}\label{linear-implication}
\(\begin{array}{rclcrcl}
A\limp B & \cong& A\orth\parr B\\
A\limp B & \cong& B\orth\limp A\orth\\
A\tens B \limp C & \cong& A\limp B \limp C\\
\end{array}\)
\subsubsection{The exponential isomorphisms}\label{the-exponential-isomorphisms}
\(\begin{array}{rclcrcl}
\oc(A\with B) & \cong& \oc A\tens\oc B & \quad& \oc\top & \cong& \one\\
\wn(A\plus B) & \cong& \wn A\parr\wn B & \quad& \wn\zero & \cong& \bot\\
\end{array}\)
\subsubsection{Quantifiers}\label{quantifiers-1}
\(\begin{array}{rclcrcl}
\forall \xi_1. \forall\xi_2. A & \cong& \forall\xi_2. \forall\xi_1. A\\
\exists \xi_1. \exists\xi_2.A & \cong& \exists\xi_2.\exists\xi_1.A\\
\\
\forall \xi . (A \parr B) & \cong& A \parr \forall \xi.B \quad (\xi\notin A) \\
\exists \xi . (A \tens B) & \cong& A \tens \exists \xi.B \quad (\xi\notin A) \\
\\
\forall \xi . (A \with B) & \cong& (\forall \xi . A) \with (\forall \xi . B) & & \forall \xi . \top & \cong& \top \\
\exists \xi . (A \plus B) & \cong& (\exists \xi . A) \plus (\exists \xi . B) & & \exists \xi . \zero & \cong& \zero
\end{array}\)
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: