1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Wednesday October 11, 11:00 am
Djordje Cubric (DPMMS)
We study the ``right adjoint'' fragment of intuitionistic multisorted predicate logic, that is the connectives (T,&,->,forall) with Lambek/Lawvere/Prawitz equality of proofs. The categorical models are forall fibrations - a generalization of hyperdoctrines. In the indexed category language they can be defined as follows: the base has finite products, fibers are cartesian closed categories, pullback functors preserve the structure and the pullback functors along projections have stable right adjoints.
We show that many of the well known properties of cartesian closed categories hold here as well. We organize them in the form of three representation theorems. The first one represents every forall fibration as a classifying fibration for a typed calculus and as a consequence every forall fibration is equivalent to one which is "very strict". Next, we have a Yoneda-like representation of forall fibrations obtained using a variant of Street-Walters Yoneda structure n the 2-category of fibrations. As a corollary, we obtain some conservativness results for our fragment. Our third representation theorem is a Friedman-like completeness for the free forall fibrations with respect to families of Sets. A corollary of this result can be stated as follows: a diagram commutes in every forall fibration if and only if it commutes when interpreted in sets. Also, we will mention some of the syntactic properties of our calculus e.g. a solution of the word problem.