Date: Tue, 20 Oct 1998 16:15:27 +0100 From: Lindsay Errington Subject: categories: twisted arrow categories In Chapter IX, Sec 6, Ex 3 of CWM, MacLane defines the twisted arrow category of C such that objects are arrows f : a -> b of C and arrows are pairs of morphisms of C, (l,m) : f -> g, such that g = mfl. The construction is part of a proof of the reduction of ends to limits. I would be grateful for pointers to other occurrences of this construction in the literature. Lindsay Errington Date: Wed, 21 Oct 1998 10:03:33 +1000 From: street@mpce.mq.edu.au (Ross Street) Subject: categories: Re: twisted arrow categories >In Chapter IX, Sec 6, Ex 3 of CWM, MacLane defines the twisted arrow >category of C such that objects are arrows f : a -> b of C and arrows >are pairs of morphisms of C, (l,m) : f -> g, such that g = mfl. The >construction is part of a proof of the reduction of ends to limits. > >I would be grateful for pointers to other occurrences of this construction >in the literature. The twisted arrow category of A is the category of elements of the hom functor A(-,-) : A^op x A --> Set. In internal and variable category theory there is a sense in which the twisted arrow fibration comes first and then can be used to define hom functors and local smallness. For example, see page 292 of my paper Cosmoi of internal categories, Transactions American Math. Soc. 258 (1980) 271-318; MR82a:18007 Regards, Ross www.mpce.mq.edu.au/~street/ Date: Wed, 21 Oct 1998 10:25:09 -0400 From: Charles Wells Subject: categories: Re: twisted arrow categories The twisted arrow category is discussed in my paper "Extension Theories for Categories", available at http://www.cwru.edu/artsci/math/wells/pub/papers.html (it has never been published). > >In Chapter IX, Sec 6, Ex 3 of CWM, MacLane defines the twisted arrow >category of C such that objects are arrows f : a -> b of C and arrows >are pairs of morphisms of C, (l,m) : f -> g, such that g = mfl. The >construction is part of a proof of the reduction of ends to limits. > >I would be grateful for pointers to other occurrences of this construction >in the literature. Charles Wells, Department of Mathematics, Case Western Reserve University, 10900 Euclid Ave., Cleveland, OH 44106-7058, USA. EMAIL: charles@freude.com. OFFICE PHONE: 216 368 2893. FAX: 216 368 5163. HOME PHONE: 440 774 1926. HOME PAGE: URL http://www.cwru.edu/artsci/math/wells/home.html Date: Wed, 28 Oct 1998 17:32:31 +0000 From: Lindsay Errington Subject: categories: twisted systems Following on from my earlier posting Re: twisted arrow categories, the following paper is now available on my home page: http://theory.doc.ic.ac.uk/~le/ . Twisted Systems and the Logic of Imperative Programs Following Burstall, a flow diagram can be represented by a pair consisting of a graph and a functor from the free category to the category of sets and relations. A program is verified by incorporating the assertions of the Floyd-Naur proof method into a second functor and exhibiting a natural transformation to the program. A broader range of properties is obtained by substituting spans for relations and introducing oplaxness into both the functors representing programs and the natural transformations in the morphisms between programs. The apparent complexity of this generalization is overcome by the observation that an oplax functor J -> Sp(C) is essentially the same as a functor Tw(J) -> C where Tw(J) is the twisted arrow category of J. Thus, a program is a presheaf Tw(F(G) -> Set as are the properties of the program. By analogy with categorical models of first-order logic, a program and the properties which pertain to it are subobjects of a suitably chosen base object. In this setting safety and liveness properties are dual in a fibre of subobjects. I welcome any comments and suggestions. Lindsay Errington