This is a reformulation of my question Characterizing triangles unembeddedly.

Motivation 1: There is such a thing as a generic group. In category theory this is done by constructing "theory" of the group, which is a category in a certain doctrine. Functors (in that doctrine) to Set, or more generally to any topos, are groups. The barest such theory (as usually seen) is the Lawverean algebraic theory of groups. This theory is a category containing an object and operations making it a group object in that category, and the theory is the smallest such category that contains all finite limits. There are fancier ones; the fanciest is the classifying topos for groups, which is in some sense the initial topos-with-group object. Since in a topos, you have full-scale first order intuitionistic logic, the classifying topos for groups allows you to reason about the generic group inside the classifying topos and the theorems you prove will be true for all groups. (This is only an approximation of the actual situation.) In particular you can't prove it is abelian and you can't prove it isn't; the logic clearly does not have excluded middle.

Motivation 2: You can prove that a triangle that has two angles that are equal must be isosceles (has two sides that are equal). You can do this with Pappus' proof: Look at the triangle, flip it over the perpendicular from the odd angle to the other side, look at it again, and the side-angle-side theorem shows you that the "two" triangles are congruent, so two sides much be equal. This appears to me to be true without requiring the parallel postulate. So the theorem and the proof must be true not only in Euclidean 2-space but in any surface of constant curvature. (Here I am getting into territory I know very little about, so this particular motivation may be totally misguided.)

So what I want is a classifying space of some sort that contains the generic triangle in such a way that maps of the correct sort to any surface of constant curvature are triangles, and so that Pappus' proof can be carried out in the classifying space. The space doesn't have to be a topos or a category at all. I have no clue as to what sort of structure it would be.

Note 1: Even the Lawvere theory of groups has its own internal logic -- in this case equational logic. You certainly cannot prove the generic group is or is not abelian with equational logic.

Note 2: It does not seem reasonable to me that Pappus' proof would work in a surface with variable curvature. But maybe there is some trick to define "angle mod curvature" that would make it true.