From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/413 Path: news.gmane.org!not-for-mail From: categories Newsgroups: gmane.science.mathematics.categories Subject: functions Omega->Omega Date: Mon, 30 Jun 1997 23:37:55 -0300 (ADT) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241016951 25648 80.91.229.2 (29 Apr 2009 14:55:51 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 14:55:51 +0000 (UTC) To: categories Original-X-From: cat-dist Mon Jun 30 23:37:56 1997 Original-Received: by mailserv.mta.ca; id AA07277; Mon, 30 Jun 1997 23:37:55 -0300 Original-Lines: 34 Xref: news.gmane.org gmane.science.mathematics.categories:413 Archived-At: Date: Sun, 29 Jun 1997 19:04:54 +0100 (BST) From: Paul Taylor Richard Wood mentioned an observation about functions Omega->Omega in a topos. In the more abstract situation of a classifier Sigma for some subclass of monos (closed under isomorphisms, composition and pullback along arbitrary maps, and such that the characteristic function of a subobject, where it exists, is unique), the following formula holds: for any function f:Sigma x X -> X and predicate a:X -> Sigma f(a) & a = f(true) & a In fact, along with Sigma being a semilattice, this is necessary and sufficient for Sigma and its powers to form a full subcategory of some category in which Sigma is a classifier. I wonder whether anyone has noticed this formula before? In my construction, the Frobenius law for an existential quantifier is derivable from it. It is also reminiscent of the Berry order in stable domain theory, but I can see no substantial connection. It is easily provable in higher order logic: either way, assume a, so a=true. Curiously, Phoa's Principle (in synthetic domain theory) is the conjunction of the higher order equation above its lattice dual f(a) \/ a = f(false) \/ a and all functions f:Sigma->Sigma are monotone. For the continuation of this story, go to Vancouver ... Paul