Why commutative diagrams coincide with equivalent proofs

DOI10.1090/conm/013/685975zbMath0504.18004OpenAlexW4238560411MaRDI QIDQ4740068

Saunders Mac Lane

Publication date: 1982

Published in: Contemporary Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1090/conm/013/685975

zbMATH Keywords

coherencereductioncut eliminationproof theoryderivationrules of inferencesymmetric monoidal closed categoriescanonical arrowscommutativity of diagram

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Structure of proofs (03F07) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Foundations, relations to logic and deductive systems (18A15)

Related Items (7)

From petri nets to linear logic ⋮ Principal types of BCK-lambda-terms ⋮ Unnamed Item ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ Aspects of Categorical Recursion Theory ⋮ The structure of free closed categories ⋮ An internal language for autonomous categories

This page was built for publication: Why commutative diagrams coincide with equivalent proofs