From mboxrd@z Thu Jan  1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/443
Path: news.gmane.org!not-for-mail
From: categories <cat-dist@mta.ca>
Newsgroups: gmane.science.mathematics.categories
Subject: Re: functions Omega->Omega
Date: Mon, 14 Jul 1997 20:25:22 -0300 (ADT)
Message-ID: <Pine.OSF.3.90.970714202504.11822B-100000@mailserv.mta.ca>
NNTP-Posting-Host: main.gmane.org
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
X-Trace: ger.gmane.org 1241016970 25782 80.91.229.2 (29 Apr 2009 14:56:10 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Wed, 29 Apr 2009 14:56:10 +0000 (UTC)
To: categories <categories@mta.ca>
Original-X-From: cat-dist Mon Jul 14 20:26:17 1997
Original-Received: by mailserv.mta.ca; id AA14261; Mon, 14 Jul 1997 20:25:22 -0300
Original-Lines: 29
Xref: news.gmane.org gmane.science.mathematics.categories:443
Archived-At: <http://permalink.gmane.org/gmane.science.mathematics.categories/443>

Date: Mon, 14 Jul 1997 14:24:43 -0400
From: Philip J. Scott <scpsg@matrix.cc.uottawa.ca>

>Date: Fri, 11 Jul 1997 16:56:25 -0400 (EDT)
>From: Andre Scedrov <scedrov@saul.cis.upenn.edu>
>
>
>          >             f(a) & a  =  f(true) & a
>          >
>          > I wonder whether anyone has noticed this formula before?
>
>Similar formulas and their analogs in intuitionistic second-order
>propositional calculus are discussed in my paper in the Annals Pure
>Appl. Logic 27 (1984) 155-164. That paper was motivated by Higgs's
>observation that every monic  Omega -> Omega  in a topos is an involution,
>see Peter Johnstone's paper "Automorphisms of Omega" in Alg. Universalis
>9 (1979) 1-7.
>
> Andre Scedrov

For a logical proof of Higgs' theorem, based on the above observations
of Scedrov, see Lambek-Scott (Introd. to Higher Order Cat. Logic), p.160,
Exercise 4. A further result along these lines is in Lemma 12.3, p. 190 of
our book.

                        Phil Scott