On 03/08/14 06:22, Thomas Streicher wrote:
One should not require all fibrations to be endowed with a cleavage. Rather one should be open to accept some strong choice principles on the meta level which allow one to assume the existence of cleavages whenever convenient. But, definitely, one should give most definitions and constructions in a way not referring to cleavages.
I completely agree with this, it is my own feeling beautifully and synthetically expressed. I only add: "... most definitions and constructions AND proofs in a way ..." Also, that many times the use of cleavages may seem convenient, when in fact it is not. And I also put in the same bag the equivalences (which in general have only one direction. Then one should proceed using the fully-faithfulness and essentially surjectiveness whenever possible, and be free to assume the existence of quasi-inverses only if it is necessary. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]