Provable formulas - Revision history

Olivier Laurent: Identites added

2013-10-29T13:27:50Z

Identites added

2013-10-28T19:31:03Z

stub tag removed

2013-10-28T19:30:06Z

‎Factorizations: exists/plus added

2013-10-28T18:36:44Z

Modified order of sections

2013-10-28T18:35:32Z

‎Distributivities: added principles and commutations

2013-10-28T18:25:17Z

Promotion principles added

2013-10-28T18:22:07Z

‎Factorizations: plus/par added

2013-10-28T18:21:26Z

‎Distributivities: tens/with added

2013-10-28T18:18:28Z

‎Monoidality of exponentials: monoidality laws for additives

2013-10-28T18:15:12Z

Quantifiers added

← Older revision		Revision as of 13:27, 29 October 2013
Line 28:		Line 28:

	<math>(\forall \xi . A) \plus (\forall \xi . B) \limp \forall \xi . (A \plus B)</math>		<math>(\forall \xi . A) \plus (\forall \xi . B) \limp \forall \xi . (A \plus B)</math>
		+
		+	== Identities ==
		+
		+	<math>\one \limp A\orth\parr A</math>
		+
		+	<math>A\tens A\orth \limp\bot</math>

	== Additive structure ==		== Additive structure ==

← Older revision		Revision as of 19:31, 28 October 2013
Line 1:		Line 1:
−	{{stub}}
−
	Important provable formulas are given by [[List of isomorphisms\|isomorphisms]] and by [[List of equivalences\|equivalences]].		Important provable formulas are given by [[List of isomorphisms\|isomorphisms]] and by [[List of equivalences\|equivalences]].

← Older revision		Revision as of 19:30, 28 October 2013
Line 28:		Line 28:

	<math>(A\parr B)\plus (A\parr C) \limp A\parr (B\plus C)</math>		<math>(A\parr B)\plus (A\parr C) \limp A\parr (B\plus C)</math>
		+
		+	<math>(\forall \xi . A) \plus (\forall \xi . B) \limp \forall \xi . (A \plus B)</math>

	== Additive structure ==		== Additive structure ==

@@ Line 22: / Line 22: @@
 <math>A \tens \forall \xi.B \limp \forall \xi. (A \tens B) \quad  (\xi\notin A)</math>
 == Factorizations ==
@@ Line 100: / Line 90: @@
 \end{array}
 </math>

@@ Line 7: / Line 7: @@
 == Distributivities ==
-<math>A\tens (B\parr C) \limp (A\tens B)\parr C</math>
+=== Standard distributivities ===
 <math>A\plus (B\with C) \limp (A\plus B)\with (A\plus C)</math>
 <math>A\tens (B\with C) \limp (A\tens B)\with (A\tens C)</math>
 == Factorizations ==

@@ Line 69: / Line 69: @@
  \wn{(A \with B)} &\limp& \wn{A} \with \wn{B} \\
  \oc{A} \plus \oc{B} &\limp& \oc{(A \plus B)}
 \end{array}
 </math>

← Older revision		Revision as of 18:22, 28 October 2013
Line 16:		Line 16:

	<math>(A\with B)\plus (A\with C) \limp A\with (B\plus C)</math>		<math>(A\with B)\plus (A\with C) \limp A\with (B\plus C)</math>
		+
		+	<math>(A\parr B)\plus (A\parr C) \limp A\parr (B\plus C)</math>

	== Additive structure ==		== Additive structure ==

@@ Line 58: / Line 58: @@
 \begin{array}{rcl}
   \wn(A\parr B) &\limp& \wn A\parr\wn B \\
-  \oc A\tens\oc B &\limp& \oc(A\tens B)
+  \oc A\tens\oc B &\limp& \oc(A\tens B) \\
 \end{array}
 </math>

@@ Line 21: / Line 21: @@
   A\with B &\limp& A &\quad& A\with B &\limp& B &\quad& A &\limp& \top\\
   A &\limp& A\plus B &\quad& B &\limp& A\plus B &\quad& \zero &\limp& A
 \end{array}
 </math>