functions Omega->Omega

[categories <cat-dist@mta.ca>]

Date: Sun, 29 Jun 1997 19:04:54 +0100 (BST)
From: Paul Taylor <pt@dcs.qmw.ac.uk>

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