Toward the Automation of Category Theory

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 Fun[C D, E] and Fun[C, Fun[D, E]] are naturally isomorphic.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 08, 2004
Accession Number
AD1000314

Entities

People

  • Dexter Kozen

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Calculus
  • Computational Complexity
  • Computer Science
  • Computers
  • Construction
  • Environment
  • Equations
  • Identities
  • Judgment
  • Language
  • Mathematics
  • New York
  • Notation
  • Programming Languages
  • Reasoning
  • Symbols
  • Verification

Fields of Study

  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.