ONT Re: Higher Order Categorical Logic -- Discussion
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
HOC. Discussion Note 5
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
JA = Jon Awbrey
L&S = Lambek & Scott
MA = Murray Altheim
JA: "maps" and "sends" are just synonyms here.
MA: Okay. (he says, thinking he might be on firm ground but never
sure if the mud will suddenly slide out from under him ...)
a function f is a set of ordered pairs f = {<x1, y1>, <x2, y2>, ...}.
we say that f associates, maps, sends, etc. x1 to y1, x2 to y2, ... .
and all of those are just conventional idioms for the ordered pairs.
in short, functions have a purely formal existence, but we can use
their forms to describe more concrete things like associations of
ideas, maps in geography, processes that take place in time, etc.
the set of all ordered pairs that you can form by taking
the first element from X and the second element from Y
is called the "cartesian product" X x Y.
we write S c T for "S is a subset of T".
a "2-adic relation" L between X and Y is an arbitrary set of ordered pairs
with the first from X and the second from Y, that is, any subset of X x Y,
so we can say that L c X x Y.
a "function" f : X -> Y is a special case of a 2-adic relation f c X x Y
that has just this one additional property: every element x in X appears
in one and only one ordered pair of f.
so functions all look like this:
1 2 3 4 5 6
o o o o o o X
\ | / | / /
\ | / | / / f
\|/ |/ /
o o o o o Y
1 2 3 4 5
JA: in the beginning one starts with concrete categories:
HOC. http://suo.ieee.org/ontology/thrd36.html#03373
HOC 1. http://suo.ieee.org/ontology/msg03373.html
L&S: | Part 0. Introduction to Category Theory
|
| 1. Categories and Functors
|
| In this section we present what our reader is expected
| to know about category theory. We begin with a rather
| informal definition.
|
| Definition 1.1. A 'concrete category' is a collection of two kinds
| of entities, called 'objects' and 'morphisms'. The former are sets
| which are endowed with some kind of structure, and the latter are
| mappings, that is, functions from one object to another, in some
| sense preserving that structure. Among the morphisms, there is
| attached to each object A the 'identity mapping' 1_A : A -> A
| such that 1_A(a) = a for all a in A. Moreover, morphisms
| f : A -> B and g : B -> C may be 'composed' to produce
| a morphism gf : A -> C such that (gf)(a) = g(f(a))
| for all a in A.
MA: Okay. Baby steps. I'm not going to
pretend to understand something I'm
not sure I actually do understand.
JA: this is the checklist for any category:
1. what are the objects?
2. what are the arrows?
3. is there an identity arrow for each object?
MA: What does this mean? That there is an arrow connecting
the object to some other object establishing its identity?
What constitutes "identity" in this context? If we're not
connecting these objects to things in the real world (I'm
assuming given my hand was recently slapped that we're solely
in the realm of abstract mathematics), that "identity" has some
mathematical definition.
a concrete category C consists of a set of objects, called Obj(C),
and a set of arrows, or (homo)morphisms, called Arr(C), or Hom(C).
(the extra language is left over from a recent cultural revolution).
in a concrete category C the objects are just sets,
let's say there's the set X = {1, 2, 3, 4, 5} in C
and the set Y = {1, 2, 3, 4, 5, 6} in C.
1 2 3 4 5
o o o o o X
o o o o o o Y
1 2 3 4 5 6
the definition then demands that 1_X, the identity arrow for X,
and 1_Y, the identity arrow for Y, must be included in Arr(C),
that is, listed among the arrows of C.
concretely considered, 1_X is the mapping from X to X that
looks like this, reading the ordered pairs down the page:
1 2 3 4 5
o o o o o X
| | | | |
| | | | | 1_X
| | | | |
o o o o o X
1 2 3 4 5
one writes 1_X (x) = x for all x in X.
concretely considered, 1_Y is the mapping from Y to Y that
looks like this, reading the ordered pairs down the page:
1 2 3 4 5 6
o o o o o o Y
| | | | | |
| | | | | | 1_Y
| | | | | |
o o o o o o Y
1 2 3 4 5 6
one writes 1_Y (x) = x for all x in Y.
you could stop right there and have a valid example of a category,
as the identity arrows trivially compose according to the rules,
1_X o 1_X = 1_X and 1_Y o 1_Y = 1_Y. (We sometimes use "o" for
emphasis to indicate the composition operation.)
JA: 4. is there a composition operation on arrows?
MA: What does this mean? ("composition operation")
on the arrows rather than the objects?
in a concrete category, composition of arrows
is just the usual composition of functions.
an ordered pair of functions, f : U -> V and g : X -> Y,
in that order, is "composable" if V = X. that is to say,
the target of f is the source of g. at this point, folks
will follow different conventions, and even shift paradigms
from one context to the next. unfortunately, it is slightly
more popular to do things backasswards, in the following way:
if we have f : X -> Y and g : Y -> Z, then the composition of g on f
is the function written g o f : X -> Z, or just gf : X -> Z, and this
is defined by the equation (g o f)(x) = gf(x) = g(f(x)) for all x in X.
by way of illustration, suppose we have X and Y as above,
and suppose we add the object Z = {1, 2, 3, 4, 5, 6, 7}.
consider the function f : X -> Y that looks like this:
1 2 3 4 5
o o o o o X
\ \ \ \ |
\ \ \ \ | f
\ \ \ \|
o o o o o o Y
1 2 3 4 5 6
Consider the function g : Y -> Z that looks like this:
1 2 3 4 5 6
o o o o o o Y
\ \ \ \ \ |
\ \ \ \ \ | g
\ \ \ \ \|
o o o o o o o Z
1 2 3 4 5 6 7
the composition g o f : X -> Z can be visualized
by following up f with g in the following manner:
1 2 3 4 5
o o o o o X
\ \ \ \ |
\ \ \ \ | f
\ \ \ \|
o o o o o o Y
\ \ \ \ \ |
\ \ \ \ \ | g
\ \ \ \ \|
o o o o o o o Z
1 2 3 4 5 6 7
then you just replace each 2-edge path with
a 1-edge path, ignoring the multiplicities:
1 2 3 4 5
o o o o o X
\ \ \ \ |
\ \ \ \ | g o f
\ \ \ \|
o o o o o o o Z
1 2 3 4 5 6 7
JA: for a concrete category, the objects are sets.
for a concrete category, the arrows are mappings between sets.
(in concrete categories, the arrows are usually called morphisms).
MA: So this is not simple graph theory, since the graph objects
are themselves graphs (I'm assuming that a set can be modeled
as a graph?)
yes, this is more like an "application of graph theory" to codify
at a fairly high level of abstraction the structure in a category.
(graph theorists simpliciter usually do not talk this way, and would
insist on calling them "labeled digraphs" or labeled directed graphs.)
thus, a node in one of these directed graphs stands for a whole set of
elements, and a single directed edge stands for a function between sets.
L&S: | Example C1. The category of 'sets'. Its objects are
| arbitrary sets and its morphisms are arbitrary mappings.
| We call this category "Sets".
JA: Category C1 = Sets.
C1 takes any set to be an object of the category.
C1 takes any mapping between sets to be an arrow.
(this is a case of trivial structure to preserve.)
MA: This seems fairly clear.
JA: The next examples are sets plus "structure",
in these cases, something like a "sums table",
a "times table", or a "less than" relation is
defined on the sets of the category and also
preserved by the arrows of the category.
L&S: | Example C2. The category of 'monoids'. Its objects are
| monoids, that is, semigroups with unity element, and its
| morphisms are homomorphisms, that is, mappings which
| preserve multiplication (the semigroup operation)
| and the unity element.
MA: The unity element being "="? What does the
phrase "preserve multiplication" mean?
a "semigroup" is a set with a 2-ary operation (*)
subject to an associative law, a*(b*c) = (a*b)*c.
sometimes you think of (*) as multiplication,
and write a*b as ab. other times you think
of (*) as addition, and write a*b as a+b.
the "unity element" is just another name
for the identity element in the system.
if you are thinking of (*) on analogy
with multiplication, you will use "1"
and write 1*a = a = a*1. if you are
thinking of (*) on analogy with sum,
you use "0" and write 0+a = a = a+0.
have to break here. will pick up at "preserve".
jon awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o