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