Authors: Došen, Kosta 
Affiliations: Mathematical Institute of the Serbian Academy of Sciences and Arts 
Title: Cut elimination in adjuncion
Journal: Bulletin of the Section of Logic
Volume: 28
Issue: 2
First page: 61
Last page: 73
Issue Date: 1-Jan-1999
ISSN: 0138-0680
The notion of adjunction is formulated so that for every arrow in freely gener-ated adjunctions there is a composition-free term for this arrow, which can be brought into a normal form unique for the arrow. In this formulation, natural transformations are not conceived as families of arrows, but as operations on arrows. Composition elimination is the form Gentzen's cut elimination takes in categories. The composition-free normal form serves to obtain simple geometri-cal decision procedures for the commuting of diagrams. It serves also to show that adding to the notion of adjunction any new equality between arrows in the language of free adjunctions would trivialize this notion.
Publisher: University of Lodz

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.