Previously: Models of (Dependent) Type Theory. There is a deep connection between mathematics and programming. Computer programs deal with such mathematical objects as numbers, vectors, monoids, fu…