Oi pessoas,
acho que isto aqui pode interessar a várias pessoas da lista:
Downcasing Types
================
When we represent a category C in a type system it becomes a 7-uple,
whose first four components - class of objects, Hom, id, composition
- are "structure"; the other three components are "properties", and
only these last three involve equalities of morphisms.
We can define a projection that keeps the "structure" and drops the
"properties" part; it takes a category and returns a
"proto-category", and it also acts on functors, isos, adjunctions,
proofs, etc, producing proto-functors, proto-proofs, and so on.
We say that this projection goes from the "real world" to the
"syntactical world"; and that it takes a "real proof", P, of some
categorical fact, and returns its "syntactical skeleton", P-. This
P- is especially amenable to diagrammatic representations, because
it has only the constructions from the original P --- the diagram
chasings have been dropped.
We will show how to "lift" the proto-proofs of the Yoneda Lemma and
of some facts about monads and about hyperdoctrines from the
syntactical world to the real world. Also, we will show how each
arrow in our diagrams is a term in a precise diagrammatic language,
and how these diagrams can be read out as definitions. The
"downcased" diagrams for hyperdoctrines, in particular, look as
diagrams about Set (the archetypical hyperdoctrine), yet they state
the definition of an arbitrary hyperdoctrine, plus (proto-)theorems.
Link:
http://angg.twu.net/math-b.html#unilog-2010
São notas para um minicurso pra não-especialistas, ainda não estão em
forma final, e talvez mereçam um "abstract" menos técnico que este,
mas mesmo assim... 8-)
[[]],
Eduardo Ochs
[email protected]
http://angg.twu.net/
_______________________________________________
Logica-l mailing list
[email protected]
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
