Here is Leinster’s version of the Category people’s foundation for set theory. Whereas ZFC talks of only sets, XX (as I will call his theory) has two sorts of things: sets and functions. Sets are written in upper case letters and functions in lower case. There is a primitive predicate of a function f and two sets X and Y. It is written “f : X → Y”. That there are two sorts which each use their own set of variables (like Fortran in 1956) is no real problem for first order predicate calculus which usually admits just one sort. Here I describe why two sorted logic is no deal stopper.

There is one more primitive, a function of two functions, yielding another function. (Composition if you must know.) It is well known how to include functions within a strict predicate calculus system: a predicate F which says of three functions f, g, h that f = f°h.

…

Lawvere’s Category Sets, thereon, perspectives