Accession Number:

AD1000314

Title:

Toward the Automation of Category Theory

Descriptive Note:

Technical Report

Corporate Author:

Cornell University Ithaca United States

Personal Author(s):

Report Date:

2004-09-08

Pagination or Media Count:

22.0

Abstract:

We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories FunC D, E and FunC, FunD, E are naturally isomorphic.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE