Tuesday, 22 January 2002 2:30 - 4:00 Eduardo Ochs A system of natural deduction for categories Abstract: We will present a logic (system NDC) whose terms represent categories, objects, morphisms, functors, natural transformations, sets, and points, and whose deductions represent certain constructive operations involving those entities; certain categorical facts are ``essentially syntactical'', in the sense that such a fact, A, can be proved by expressing it as a term of system NDC, A', then looking for a deduction for A' in NDC, then filling up the missing details. Deductions in NDC are quite short, but NDC ``sees only the syntactical side and ignores the equational side'' --- for example, the rule that constructs a functor in NDC doesn't check if the resulting entity respects identities and compositions, so it builds only a ``proto-functor''; the equational conditions must be checked in separate. The presentation will be focused on formalizing system NDC, and on analyzing a few toy examples --- mainly the syntactical proofs of the Yoneda Lemma, and of all the steps of the demonstration that a category of the form Set^C is an elementary topos.