- 2 as a metacategory (CWM 1.1)
- 2 as an internal category in Set, i.e., 2∈Cat(Set) (CWM 1.2)
- 2 as a category enriched in Set, i.e., as a Set-category, i.e., 2∈Set-Cat (CWM 1.8, 7.7)
- 2 as a category enriched in itself, i.e., as a 2-category, i.e., 2∈2-Cat (BCECT 1.6.3)
- Set and 2 as cccccs - complete and cocomplete cartesian closed categories
- Relations between the categories
2 as a metacategory (CWM 1.1)
(The metacategory 2) has data consisting of:two objects, ⊥ and ⊤, and three arrows, 1⊥:⊥→⊥, <:⊥→⊤, and 1⊤:⊤→⊤
(<:⊥→⊤ is of course usually denoted ⊥<⊤).
(Its identity arrows) are evident, and (its composition operation) is defined by (the unit axiom).
Note that no mention of sets has been made.
2 as an internal category in Set, i.e., 2∈Cat(Set) (CWM 1.2)
(The internal category 2 in Set) has data consisting ofa set of objects 20={⊥,⊤} and
a set of arrows 21={1⊥,<,1⊤},
together with (source, target, identity, and composition functions) which implement (the operations defined for the metacategory 2).
The only difference between the definition of 2 (as a metacategory) and (as an internal category in Set) is (the explicit mention of sets and functions).
2 as a category enriched in Set, i.e., as a Set-category, i.e., 2∈Set-Cat (CWM 1.8, 7.7)
Again, we have the set of objects {⊥,⊤}, now denoted by ob2 (because the subscript ()0 will soon be given another meaning).We also have a hom-function −2−:ob2×ob2→Set,
taking each (pair of objects) to {the set of arrows from (the first, source, object) to (the second, target, object)}.
We represent the hom-function as a table:
| target | ⊤ | {<} | {1⊤} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊥ | {1⊥} | ∅ | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⟨source⟩2⟨target⟩ | ⊥ | ⊤ | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| source | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
2 as a category enriched in itself, i.e., as a 2-category, i.e., 2∈2-Cat (BCECT 1.6.3)
(The internal hom for 2) is shown in (the center of the display below), where it can be easily compared to (some related functions).
|
|
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
We can compare (the two Set-categories, 2 and Set) to (the 2-category 2) with (the following two diagrams).
The labels above the arrows are the names of the arrows in the Set-categories
(for the last arrow on each line, there is no label above, indicating that there is no such arrow in the Set-category; the Set arrow ∅→{∅} exists, but is here unnamed);
labels below arrows indicate the value of (⟨source⟩2⟨target⟩=[⟨source⟩,⟨target⟩]) for the indicated source and target.
⊥1⊥→⊤⊥<→⊤⊤1⊤→⊤⊤→⊥⊥2 above, 2 below∅1∅→∅→{∅}1{∅}→{∅}→∅Set above
There is a lot of information packed into those hom-tables. For example:
[That (the edge corresponding to (⟨source⟩=⊥)) is all ⊤] is equivalent to (⊥ being initial in 20).
[That (the edge corresponding to (⟨target⟩=⊤)) is all ⊤] is equivalent to (⊤ being terminal in 20).
[That (the edge corresponding to (⟨source⟩=⊤)) is identical to its input] is equivalent to ([⊤,−]i=12). (The letter i comes from a generalization in the paper [CC].)
[That (the edge corresponding to (⟨target⟩=⊥)) interchanges truth values] is equivalent to ([−,⊥]=¬ (negation)).
The subscript ()0 changes meaning when going between (internal category theory) and (enriched category theory)
On the one hand, (an internal category A in a category E) can be viewed as (a truncated simplicial object in E),
with A0 = the object of objects, A1 = the object of arrows, A2 = the object of composable pairs of arrows, and A3 = the object of composable triples of arrows.
That is a useful point of view, and it sets the meaning in internal category theory for A0.
On the other hand, in (enriched category theory), there is a long tradition, starting with the Eilenberg-Kelly paper “Closed Categories” and continuing through Kelly’s basic text, Basic Concepts of Enriched Category Theory,
where (the ()0 subscript) has a different meaning when applied to (an enriched category).
If A is (an enriched category), A0 is NOT (A’s set of objects) (Kelly denotes that by obA, while some other authors use |A|),
but rather (A’s underlying ordinary (Set-enriched) category), as defined in section 1.3 of [BCECT].
We wish to emphasize (the enriched categorical point of view), so we adopt its notation.
Thus henceforth 20 is not the mere set {⊥,⊤}, but rather an isomorph of the ordinary category, and linear order, 2.
2 and Set as cccccs - complete and cocomplete cartesian closed categories
We assume as already known the fact that 2 and Set are complete and cocomplete cartesian closed categories, whose operations include:| completeness | cocompleteness | internal hom | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| arity: | nullary | binary | arbitrary | nullary | binary | arbitrary | binary | |||
| 2 | ⊤ | ∧ | ∀ or ⋀ | ⊥ | ∨ | ∃ or ⋁ | ⇒ | |||
| Set | 1 | × | ∏ | ∅ | + | ∑ or ∐ | [,] | |||
The other operations necessary for completeness and cocompleteness in Set are equalizers and coequalizers.
For Set equalizers are easy, while coequalizers involve completing a parallel pair of functions into an equivalence relation, then taking the quotient of that relation.
References
CWM, Mac Lane, Saunders, Categories for the Working Mathematician (1971,1998)BCECT, Kelly, Max, Basic Concepts of Enriched Category Theory (1982/2005)
CC, Eilenberg and Kelly, “Closed Categories” (1966)
NAMC, Janelidze and Kelly, “Note on Actions of a Monoidal Category” (2001)
Draft stuff:
Relations between the categories
This section is a rough draft:
From (the total order 2) to (the 2-category 2):
The total order (2,≤) has
binary products = binary meets = conjunction = ∧,
and, for each B∈2, the order-preserving function −∧B:2→2
has a right adjoint, denoted B⇒− or [B,−] or, combining the previous two notations, [B⇒−] , thus we have:
π:(A∧B≤C) iff (A≤[B⇒C]),a special case ofA⊗B(V0)Cπ≅II, §3A(V0)[B,C]for V0=2.
From (the 2-category 2) to (its underlying total order 20):
Given the internal hom [,], i.e., ⇒, define
v:(A≤B) iff (⊤=[A⇒B]),which is almost a special case ofA(V0)Bv≅II (3.12)I(V0)[A,B].
(The general cases indicated above) are standard situations in (the theory of closed categories; see section II.3 of [CC]).
The references below the ≅ symbols are references to that paper.
The “almost” qualifier is required because (the situation in which it appears) is (a definition of ≤ in V0), not (an isomorphism between already existing objects).
(The order relation thus defined on {⊥,⊤}) is exactly the same as (that given by fiat on {⊥,⊤} in the definition of 2 as a metacategory, etc.).
Thus 20 and 2 are isomorphic total orders.
ar21⊥<1⊤≅≤2⟨⊥,⊥⟩⟨⊥,⊤⟩⟨⊤,⊤⟩≅ar(20)⊤=⊥2⊥⊤=⊥2⊤⊤=⊤2⊤→1↘↓↙⌟
