> For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic,

> For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic, and moreover dependent type theory. We emphasize the latter: dependent types are expressive and pervasive, yet underutilized in mathematics. The next step of the article is the realization that a topos[0] has this expressive capability from the get-go. There's a nice list of clarifying examples in the paper[1], starting at the bottom of page 2, for instance, stacks with push and pop, untyped lambda calculus, monad comprehension syntax in Haskell (sort of like a generalization of async/await syntax), and so on. This quote in particular seems exciting: We aim to implement native type theory as a tool which inputs the formal semantics of a language and outputs a type system, which can then be used to condition an entire codebase. Properly integrated, it could introduce expressive type theory directly into everyday programming. To do so, we plan to utilize the progress made in language specification [0] https://en.wikipedia.org/wiki/Topos https://en.wikipedia.org/wiki/Topos [1] https://arxiv.org/pdf/2102.04672.pdf https://arxiv.org/pdf/2102.04672.pdf