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.
As a double-check, to get precomposition m : f -> fg like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFswL... ?