  More recently, topos theory has been employed to investigate various forms of constructive mathematics or set theory (Joyal &amp; Moerdijk 1995, Taylor 1996, Awodey 2008), recursiveness, and models of higher-order type theories generally. The introduction of the so-called “effective topos” and the search for axioms for synthetic domain theory are worth mentioning (Hyland 1982, Hyland 1988, 1991, Hyland et al. 1990, McLarty 1992, Jacobs 1999, Van Oosten 2008, Van Oosten 2002 and the references therein). Lawvere’s early motivation was to provide a new foundation for differential geometry, a lively research area which is now called “synthetic differential geometry” (Lawvere 2000, 2002, Kock 2006, Bell 1988, 1995, 1998, 2001, Moerdijk &amp; Reyes 1991). This is only the tip of the iceberg; toposes could prove to be for the 21st century what Lie groups were to the 20th century.