Re: Bottom line to: Does equality between sets contradict the philosophy behind structural set theory?

For categories C internal to a category BB with finite limits equality on objects is given via the diagonal of Ob(C). For split fibrations over BB equality of objects is in general not recognized in the base even in the discrete case. Homotopy Type Theory is a framework where one cannot speak about equality of objects in general. This can be seen very clearly in the groupoid model. Types are groupoids and families of types are isofibrations. Diagonals of groupoids are not isofibration unless the groupoid is discrete. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]