Topos theory is a branch of mathematics which applies what programmers would call an aggressive refactoring to the category of sets and functions - a foundational workspace within which almost all of conventional math is conducted (whether the practitioners realise it or not). Math is refactored in a way reminiscent of how HOL refactors math (but constructively).
Set theory is a legacy platform like MS-DOS (!) with many limitations and anomalies which topos theory can explain and perhaps alleviate. A topos is a "virtual machine, for math ... Definitions, constructions, theorems "run" in a topos just as apps run on a VM, or SQL statements run on a database. The promise of topos theory is to cleanly separate language from implementation (just as webdesigners separate HTML from business logic) A lot of math can easily be "refactored" to apply in a much wider context.
The steps in building this refactoring are:
• Define the concept of category, a workspace of dots and composable arrows between them
• Identify the category Sets as fundamental
• Abstract out the operations and laws that make Sets useful (think CCCs (= cartesian closed categories) with some extras)
• Axiomatise a topos as a category equipped with operations obeying these laws
• Find other naturally occurring examples of topoi
• Via internal categories, understand topoi as a complete foundation for math
• Specify a language for describing constructions and deductions in a topos
Note, if you don't care about foundations, then topos theory gives you nothing new, except labour of re-learning what you already know in a new form that is awkward if you heavily rely on non-constructive reasoning.
