The lambda-calculus was invented to formalise arithmetic by encoding numbers and operations as abstract functions. We will introduce the lambda-calculus and present two encodings of modular arithmetic: the first is a recipe to quotient your favourite numeral system, and the second is purpose-built for modular arithmetic. A highlight of the second approach is that it does not require recursion i.e., it is defined without fixed-point operators. If time allows, we will also give an implementation of the Chinese remainder theorem which improves computational efficiency. 

We shall explain how to represent a couple of basic notions in model theory by standard simplicial diagrams from homotopy theory. Namely, we shall see that the notions of a {definable/invariant type}, {convergence}, and {contractibility} are defined by the same simplicial formula, and so are that of a {complete E-M type} and an {idempotent of an oo-category}.  The first reformulation makes precise Hrushovski's point of view that a definable/invariant type is an operation on types rather than a property of a type depending on the choice of a model, and suggests a notion of a type over a {space} of parameters. The second involves the nerve of the category with a single idempotent non-identity morphism, and leads to a reformulation of {non-dividing} somewhat similar to that of lifting idempotents in an oo-category. If time permits, I shall also present simplicial reformulations of distality, NIP, and simplicity.

We do so by associating with a theory the simplicial set of its n-types, n>0. This simplicial set, or rather its symmetrisation, appeared earlier in model theory under the names of {type structure}  (M.Morley. Applications of topology to Lw1w. 1974), {type category} (R.Knight, Topological Spaces and Scattered Theories. 2007), {type space functors} (Haykazyan. Spaces of Types in Positive Model Theory. 2019; M.Kamsma. Type space functors and interpretations in positive logic. 2022).