List of isomorphisms
From LLWiki
(Difference between revisions)
(First list) |
(Quantifiers added) |
||
Line 73: | Line 73: | ||
\oc(A\with B) &\cong& \oc A\tens\oc B &\quad& \oc\top &\cong& \one\\ |
\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\\ |
\wn(A\plus B) &\cong& \wn A\parr\wn B &\quad& \wn\zero &\cong& \bot\\ |
||
+ | \end{array} |
||
+ | </math> |
||
+ | |||
+ | == Quantifiers == |
||
+ | |||
+ | |||
+ | <math> |
||
+ | \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} |
\end{array} |
||
</math> |
</math> |
Latest revision as of 22:43, 27 October 2013
Contents |
[edit] Linear negation
[edit] Neutrals
[edit] Commutativity
[edit] Associativity
[edit] Multiplicative-additive distributivity
[edit] Linear implication
[edit] The exponential isomorphisms
[edit] Quantifiers