Peter Freyd says,
Colin's candidate for "weak topos" is only missing one of the uniqueness conditions, so I would hesitate to use the term. How about "near topos"?
Two counterarguments to this (without intending to express a definitive view): (1) There's always a danger of proliferating prefixes for "inferior" forms of things - pseudo, quasi, pre, weak, near, etc. Are you, Peter, willing to propose a definitive meaning for "near" analogous to your (& Sammy & Sauders') meaning for "weak"? Do you think we should use up one of these words for this purpose? (2) You say that a weak topos should be something satisfying the definition of a topos with uniqueness deleted *everywhere*. The first clause of this definition is that it's a category; do you intend it to be a weak category? What is that? Something (like homotopies, perhaps) which has non-unique composition? I suspect this leads us to a structure bearing little relationship to simple type theory or higher order predicate calculus. We often think of categorical definitions such as toposes in a hierarchical way, eg "A TOPOS is a cartesian category in which each object has a powerobject" (Categories, Allegories, 1.9). Here "cartesian category" is a background definition (genus in philosphical jargon) and "... powerobject" is the distinguishing property we have in mind (species) (cf bounded comprehension) So, if we want to weaken the definition, we do so by weakening the distinguishing property. n'est ce pas? Maybe this is a question that should be answered by examining what interesting phenomena arise in the literature. Raymond Hoofman's thesis ("Non-stable Models of Linear Logic", R.U. Utrecht, 1992) might be a good place to start. He considers weak cartesian closed categories - useful for modelling beta without eta in the lambda calculus. Exactly what to weaken is not, a priori, a clear cut issue. Paul ==============================================================================