A contrast has been pointed out:
working in a formal system
reasoning about a formal system.
Using both should lead in spiral fashion to both better formal systems and more knowledge about that which they describe. In this spirit we should surely expose the defects of a formal system rather than conceal them. The formal system may need to be changed. It would be one-sided to only “work in” a system, accepting it as a divine condemnation that we have to endure.
The objective necessity that every map has both a domain and a codomain is one of the great principles of category theory. […] Hence the answer to both of the questions
Does topos logic correspond to type theory?
Does topos logic correspond to set theory?
is NO. Both were earlier, partially successful attempts to make explicit some “necessary laws of the development of thinking in all the areas of mathematics”.
[…] For mathematics, freedom came from the recognition of that necessity: the foundational role was thus abandoned in practice by st [set theory] which promoted the “freedom” allegedly deriving from ignoring codomains, while tt [type theory], though recognizing some codomains (as types), gets entangled in the “flexibility” of refusing to declare variables, i.e. to specify domains.
A set in a topos is neither a type nor not a type: there are sets of exactly the right size to be susceptible of being wired up as memory banks which serve as power types or function types (or more specific mathematically-oriented objects) relative to some given sets, the wiring being suitable maps which serve as evaluations, inclusions, etc.
A set in a topos is not a von Neumann “set” either; it has a cohesiveness due to the incidence relations between its elements (right actions, pullbacks) so is a “Menge” not due to an excessive and irrelevant structure but to a structure adapted to the mathematical category of cohesiveness at hand.
We carry the inclusions around only as long as we need them. Already Gauss pointed out that when a subset (i.e. an inclusion map) arises, it may be very significant to study the domain in its own intrinsic self, but this is difficult to make precise in st or tt. Of course “subset” is not a binary relation between sets but a given map, a mathematical necessity that needs to be recognized by any truly flexible formalization in a way coherent enough to work in. Given two inclusion maps b, c with the same codomain A, it is clear what is a proof that “b is included in c” as subsets of A, and given any element x of A (i.e. any map with codomain A), a proof that “x belongs to b” is formally the same kind of thing. Hence by composing proofs we can always conclude that x belongs to c, independently of whether these subsets arose by equalizing some maps P with domain A.
[…] Formal systems are subjective instruments for describing and clarifying such presentations. […]
In the end it will surely be simpler, leading to greater freedom and fewer complications, to explicitly take the objectively necessary into account, rather than to succumb to a naive belief in the “freedom” to neglect some essential ingredient. There need not be an inevitable mismatch between useable formal systems and the mathematical structures they strive to present.