ONT Re: Higher Order Categorical Logic -- Discussion
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
HOC. Discussion Note 2
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
JA = Jon Awbrey
L&S = Lambek & Scott
MA = Murray Altheim
JA: Actually, if could you get as far as understanding the definition
of a natural transformation on page 8, that would be a lot. But
there's no reason to expect that you could do that on your own.
I spent a lot of time on the SUO list trying to get across basic
category-theoretic ways of thinking in concrete contexts without
ever mentioning the legion of officious titles, ideas which folks
would need to grasp before they could understand 1/10 of what RK
is talking about, but they seem to prefer the razzle-dazzle to
the nitty-gritty.
MA: Both the razzle-dazzle and the nitty-gritty are snowing me right now.
JA: What you ran into is the sort of place where the authors try
to impress people who have had a couple of years of graduate
courses in algebra and topology with the fact that they can
sum up those two years of study in a single paragraph. But
that is just a side-show bit, and you can ignore all of it.
In my notes to the Ontology List I skipped from page 11 to
page 41 just by way of getting to the logical motivations
a little quicker.
MA: So basically, you're saying to ignore the "Introduction to Category Theory"
section and jump straight to "Cartesian closed categories and Lambda Calculus"?
After understanding through page 8?
MA: Part of the difficult is language: I don't have any experience
in this particular use of English. Even simple stuff is not so
simple without the background, and I tend to not like to guess.
E.g., the idea that a morphism "sends objects of $A$ to objects
of $B$ and arrows of $A$ to arrows of $B$" might sound ostensibly
like some kind of "morphing", but I have no idea what it really
means in practice. "sends"? How is that different from "maps"?
"maps" and "sends" are just synonyms here.
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.
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?
4. is there a composition operation on arrows?
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).
L&S: | Example C1. The category of 'sets'. Its objects are
| arbitrary sets and its morphisms are arbitrary mappings.
| We call this category "Sets".
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.)
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.
a classic example would be the logarithm mapping from
a domain (D, *) of real numbers under multiplication (*)
to a domain (E, +) of real numbers under addition (+).
1. log : (D, *) -> (E, +).
the log function maps the object D to the object E,
mapping the structure of (*) to the structure of (+).
2. log(1) = 0.
the log function maps the multiplicative identity 1
to the additive identity 0.
3. log(x * y) = log(x) + log(y)
one says: "the image of the product is the sum of the images".
this describes a form of analogy or metaphor between (*) and (+).
L&S: | Example C3. The category of 'preordered sets'.
| Its objects are preordered sets, that is, sets
| with a reflexive and transitive relation on them,
| and its morphisms are monotone mappings, that is,
| mappings that preserve this relation.
say that (D, -<) is a reflexive and transitive order relation on D.
say that (E, =<) is a reflexive and transitive order relation on E.
a "monotone" (order-preserving) mapping f : D -> E is one such that:
x -< y implies f(x) =< f(y),
again, we can think of f as describing or establishing an analogy or
a metaphor between the ordering (-<) on D and the ordering (=<) on E.
JA: Category theory is really just a study in metaphors.
And, well, metaphors between metaphors (= functors).
And, well, metaphors between functors (= nat.trans).
In one of my first courses in this stuff we got to
do a "creative" final paper, and I wrote an intro
to the main ideas in the form of a science fiction
story. Probably still have it buried in a basement
box somewhere, but don't know if I could find it now.
MA: While stories like that sometimes help, they also sometimes
just mask the actual content. What would be great would be
a discussion of this in plain English, if that were possible.
JA: The stuff that I append here could provide us with a good couple
of months of study, but then you'd have the most essential bits.
MA: ??? You have appended the literal contents of pages 4-8 of the book.
yes, just that much.
MA: And I must say that while the symbols in the book are difficult,
their transformations into ASCII make it quite a bit harder to
deal with.
you get used to it. and it's quick.
MA: Maybe if we just honed in on something at the beginning?
Say, Example C4, where we see definitions for deductive
systems and categories.
okay, tomorrow ...
jon awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
http://www.cs.bsu.edu/homepages/mighty/history.html
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o