szany

This is a bit defeatist. Parsing the definition in your head is only the first level of understanding you can have about a mathematical structure. You don't really understand something until you can reinvent it (and in particular give a plausible answer to "why these axioms and not others?")

For example, to motivate groups, you could introduce the concept of a symmetry as a mapping from an object to itself that doesn't change its properties, introduce the idea of an isomorphism as a mapping with an inverse (where f and g being inverse means they compose to identity maps), put them together and postulate that a reasonable formalization of a symmetry is an automorphism (isomorphism from an object to itself), note that isomorphisms are closed under composition, and arrive at the definition of a group by considering sets of symmetries closed under finite composition (thinking of identity maps as the composition of 0 morphisms).

I'm sure there's a similarly conceptual way to motivate monads in functional programming. Hyland and Power have papers on algebraic theories of "effectful" operations and how they give rise to (finitary) monads, as one starting point.

Part of starting this was finding a place and moving in.

This isn't full-time — one of the goals is explicitly "to complement rather than conflict with the tenure of a full-time position elsewhere".

Thanks for raising that question. Actually the house was rented for the purpose of hosting the program, not the other way around.

Of course we're trying not to operate at a loss, but we're willing to accept that if necessary to accomplish the stated goals.

Most true statements are uninteresting.

What makes ambition/creativity/drive/perspective/attitude/inspiration any more intrinsic than intelligence/knowledge?

It's a foundation of mathematics whose native objects are structures fundamental to higher mathematics (∞-groupoids, which are more or less equivalent to topological spaces up to homotopy), rather than awkward encodings (ZFC "sets", which are tree-like things), and where everything is automatically invariant with respect to abstract notions of equivalence (think isomorphism vs. equality).

The point is that it makes it much more realistic to check complicated math using computers, which will become more important as math inevitably gets more complicated.

Oh, and it happens to be a functional programming language. Which says something about functional programming.