That works for any function f that is precomposed by a bijection. Then the bijection and its inverse cancel out, so that is correct. Many of these examples with regards to precomposition and postcomposition might be embedded in other categories, such as slice categories: C/f or f/C. However, of all the different categories you can use to make a model of functions I have singled out Sets^(->) because it forms a topos.
The property that Sets^(->) is a topos gives us a lot to work with. All impredicative constructive mathematics can be defined internal to Sets^(->). This is interesting because it means almost all mathematics can be done internal to Sets^(->), with functions instead of sets as its first class logical objects.
Secondly, the fact that it is a topos gives us an internal logic in Sets^(->). The internal logic of Sets^(->) is a trivalent logic with three values: true, false, and half truth that fails to satisfy the law of excluded middle. Sets^(->) has its own distinct system of logical operators and connectives which generalize those in classical logic and that can be used on all subobjects.
All aside from that, Sets^(->) has an incredibly remarkable logic of quotients. It has been shown that the dual logic of quotients in Sets^(->) is intuitively similar to the partition pairs construction of Hartmanis and Stearns in Algebraic Structure Theory of Sequential Machines (1966). So the immense power of the topos Sets^(->) is enough to capture their central construction for creating a computational structure theory, and mine.
All this demonstrates that Sets^(->) by itself has an incredibly rich theory which is worthy of further exploration. The theory of Sets^(->) is really the functional counterpart of set theoretic foundations, a foundation for a different kind of function-based mathematics, and the means by which we can create a system of logical reasoning for functional programs.
The property that Sets^(->) is a topos gives us a lot to work with. All impredicative constructive mathematics can be defined internal to Sets^(->). This is interesting because it means almost all mathematics can be done internal to Sets^(->), with functions instead of sets as its first class logical objects.
Secondly, the fact that it is a topos gives us an internal logic in Sets^(->). The internal logic of Sets^(->) is a trivalent logic with three values: true, false, and half truth that fails to satisfy the law of excluded middle. Sets^(->) has its own distinct system of logical operators and connectives which generalize those in classical logic and that can be used on all subobjects.
All aside from that, Sets^(->) has an incredibly remarkable logic of quotients. It has been shown that the dual logic of quotients in Sets^(->) is intuitively similar to the partition pairs construction of Hartmanis and Stearns in Algebraic Structure Theory of Sequential Machines (1966). So the immense power of the topos Sets^(->) is enough to capture their central construction for creating a computational structure theory, and mine.
All this demonstrates that Sets^(->) by itself has an incredibly rich theory which is worthy of further exploration. The theory of Sets^(->) is really the functional counterpart of set theoretic foundations, a foundation for a different kind of function-based mathematics, and the means by which we can create a system of logical reasoning for functional programs.
[1] https://ncatlab.org/nlab/show/topos
[2] https://ncatlab.org/nlab/show/internalization
[3] https://ncatlab.org/nlab/show/internal+logic
[4] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.