Basic SemanticsQuick index:
1. Categories with finite products ================================== Categories with finite products (CFPs) are categories in which we can interpret tuples and projections. Our archetypal CFP is Set. An example of the translation: a,a',(b,c) |---------------> (c,a'),a' becomes: <<π_3;π_2,π_1>,π_1> A×A×(B×C) ------------------> (C×A)×A How? Let's look at how we construct (c,a'),a' from a,a',(b,c): a,a',(b,c) ----------π_3 b,c a,a',(b,c) ---π_2 ----------π_2 c a' a,a',(b,c) ----------------<,> ----------π_2 c,a' a' -------------------------<,> (c,a'),a' Now let's make the contexts explicit (p := a,a',(b,c), for typographical reasons): p|-a,a',(b,c) -------------π_3 p|-b,c p|-a,a',(b,c) ------π_2 -------------π_2 p|-c p|-a' p|-a,a',(b,c) -----------------------<,> -------------π_2 p|-c,a' p|-a' -------------------------------<,> p|-(c,a'),a' Translating: id --- π_3 id ------- --- π_3;π_2 π_2 id ---------------- --- <π_3;π_2,π_2> π_2 --------------------- <<π_3;π_2,π_2>,π_2> Notation: 1={*} is the 0-ary product. Example: a,b|->* (``!'') is the only morphism from A×B to 1. It's not important to differentiate the ``*''s - for example, *,*' |-> *,*' and *,*' |- *',* are the same morphism from 1×1 to 1×1 - we can write it just as *,* |-> *,*. L 2. A ring in a CFP ================== A ring in a CFP is an object R equipped with five morphisms, z s 1 ----> R <----- R×R * |---> 0 1 ----> R <----- R×R * |---> 1 u m a+b <----| a,b n ab <----| a,b R -----> R a |---> -a These morphisms must obey certain equations, one for each ring axiom. For example, ∀a,b,c. a(b+c) = ab+ac becomes the following equation on morphisms: (a,b,c |-> a(b+c)) = (a,b,c |-> ab+ac) t|-b t|-c t|-a t|-b t|-a t|-c ---------- ---------- ---------- t|-b,c t|-a,b t|-a,c ------ ------ ----- t|-a t|-b+c t|-ab t|-ac -------------- ------------------ t|-a,(b+c) t|-ab,ac ---------- -------- t|-a(b+c) = t|-ab+ac π_1 π_2 π_0 π_1 π_0 π_2 --------- --------- --------- <π_1,π_2> <π_0,π_1> <π_0,π_2> ----------- ----------- ----------- π_0 <π_1,π_2>;s <π_0,π_1>;m <π_0,π_2>;m ------------------ ------------------------- <π_0,<π_1,π_2>;s> <<π_0,π_1>;m,<π_0,π_2>;m> ------------------- --------------------------- <π_0,<π_1,π_2>;s>;m = <<π_0,π_1>;m,<π_0,π_2>;m>;s L 3. CCC Diagrams =============== Note (1): these diagrams function as a ``skeleton'' for the whole proof - we take the diagram, add layers of meat and skin, and we reconstruct the whole animal. As far as I know, the standard proofs for CCC<->λ1 don't have a ``center'' that is as clear as we have here. Note (2): our idea of ``dictionaries'' is related to the idea of ``internal languages'' in Categorical Semantics. It is common in, e.g., Topos Theory, to take a set-theoretical proof, then check that it is well-behaved enough, and then say that ``this proof works in any topos''. This corresponds to our liftings; but internal languages assign precise meanings to all well-formed expressions of a certaing language, while our dictionaries will only attribute meanings to those expressions that are mentioned, directly or indirectly, in our proofs. /Internal languages induce infinite dictionaries/; and our way of building dictionaries from proofs will let us deal with arising ambiguities one by one, in organic (and ad-hoc) ways... 4. CCCs in half-DNC =================== This diagram expresses the structure in a CCC: A CCC is a category plus this "structure": --| a |-- a a,b <==== a / - \ - - - / | \ | | <--> | v v v v v v b <--| b,c |--> c * c ===> b|->c The product diagram comprises two operations on morphisms, and the adjunction diagram four: (we'll forget the terminal for the moment) / a \ / a \ | - | | - - | | | | |-> | / \ | | v | | v v | \ b,c / \ b c / / a \ / a \ | - - | | - | | / \ | |-> | | | | v v | | v | \ b c / \ b,c / a',b <==== a' - - | <--| | v v a,b <==== a - - | <--| | | |--> | v v c ===> b|->c - - | |--> | v v c' ==> b|->c' a',b <==== a' - - p|-<a(πp),π'p> | <--| | a'|-a(a') v v a,b <==== a - - p|-f(πp)(π'p) | <--| | a|-f(a) p|-c(p) | |--> | a|-λb.c(<a,b>) v v c ===> b|->c - - c|-c'(c) | |--> | f|-λb.c'(fb) v v c' ==> b|->c' 5. From CCCs to λ-calculus: products ==================================== From diagrams to natural deduction: propositional calculus / P \ / P \ P P | - | | - - | : : | | | |-> | / \ | P|-Q&R P|-Q&R Q&R Q&R | v | | v v | ====== ====== --- --- \ Q&R / \ Q R / P|-Q P|-R Q R / P \ / P \ P P | - - | | - | : : | / \ | |-> | | | P|-Q P|-R Q R | v v | | v | =========== ------- \ Q R / \ Q&R / P|-Q&R Q&R / a \ / a \ a a | - | | - - | : : | | | |-> | / \ | a|-b,c a|-b,c b,c b,c | v | | v v | ====== ====== --- --- \ b,c / \ b c / a|-b a|-c b b / a \ / a \ a a | - - | | - | : : | / \ | |-> | | | a|-b a|-c b c | v v | | v | =========== ------- \ b c / \ b,c / a|-b,c a,c In half-DNC: / a \ / a \ a a | - | | - - | : : | | | |-> | / \ | a|-p(a) a|-p(a) p(a) p(a) | v | | v v | ======== ========= ----- ------ \ p(a) / \πp(a) π'p(a)/ a|-πp(a) a|-π'p(a) πp(a) π'p(a) / a \ / a \ a a | - - | | - | : : | / \ | |-> | | | a|-b(a) a|-c(a) b(a) c(a) | v v | | v | ================= ----------- \ b(a) c(a) / \<b(a),c(a)>/ a|-<b(a),c(a)> <b(a),c(a)> 6. From CCCs to λ-calculus: equations for products ================================================== The two arrows (coming from the natural transformations) are inverses, so their two composites must be identites: / a \ / a \ / a \ | - | | - - | | - | | | | |-> | / \ | |-> | | | = id | v | | v v | | v | \ p(a) / \πp(a) π'p(a)/ \<πp(a),π'p(a)>/ / a \ / a \ / a \ | - - | | - | | - - | | / \ | |-> | | | |-> | / \ | = id | v v | | v | | v v | \ b(a) c(a) / \<b(a),c(a)>/ \π<b(a),c(a)> π'<b(a),c(a)>/ ∀p:B×C. p=<πp,π'p> ∀b:B,c:C. b=π<b,c> ∀b:B,c:C. c=π'<b,c> 7. Deleted diagrams =================== a,b <==== a - - | <--| | v v a',b <==== a' a,b <==== a a,b <==== a - - - - | <--| | | |--> | v v v v c ===> b|->c c ===> b|->c c ===> b|->c - - | |--> | v v c' ==> b|->c' If we translate these six operations to half-DNC we get: / a \ / a \ | - | | - - | | | | |-> | / \ | | v | | v v | \ p(a) / \ πp(a) π'p(a) / / a \ / a \ | - - | | - | | / \ | |-> | | | | v v | | v | \ b(a) c(a) / \ <b(a),c(a)> / p <=========== a - - | <--| | v v <a'(πp),π'p> <=== a'(a) p <========= a p <========== a - - - - | <--| | | |--> | v v v v f(πp)(π'p) ===> f(a) c(p) ====> λb.c(<a,b>) c ===========> f - - | |--> | v v c'(c) =====> λb.c'(fb) 8. New diagrams =============== An adjunction has 4 operations on morphisms =========================================== P'&Q <==== P' - - | <--| | v v P&Q <==== P - - | <--| | | |--> | v v R ====> Q⊃R - - | |--> | v v R ====> Q⊃R Translating categorical operations to λ-calculus ================================================ P'&Q ---- P'&Q <==== P' P' P'&Q - - : ---- P'&Q|-P&Q | <--| | P'|-P P'|-P P Q v v ========= ------ P&Q <==== P P'&Q|-P&Q P&Q a',b p ---- -- a',b <==== a' a' a',b πp p - - : : : --- p|-<a(πp),π'p> | <--| | a'|-a(a') a(a') b a(πp) π'p v v ---------- ----------- a,b <==== a <a(a'),b> <a(πp),π'p> a',b <==== a' - - p|-<a(πp),π'p> | <--| | a'|-a(a') v v a,b <==== a - - p|-f(πp)(pi'p) | <--| | a|-f(a) p|-c(p) | |--> | a|-λb.p(<a,b>) v v c ===> b|->c - - c|-c'(c) | |--> | f|-λb.c'(fb) v v c' ==> b|->c' The product and the terminal ============================ Translating λ-calculus rules to categorical constructions ========================================================= |