# Overview

This arc introduces the setting “a place to do maths”. The “types” that will populated this “place” will have three interpretations:

Proof theoretically, with types as propositions

Type theoretically, with types as programs

Category theoretically (geometrically), with types as objects (spaces) in a category (the space of spaces)

## Terms and Types

Here are some things that we could like to have in a ‘place to do maths’

objects to reason about (E.g.

`ℕ`

)recipes for making things inside objects (E.g.

`n + m`

for`n`

and`m`

in naturals.)propositions to reason with (E.g.

`n = 0`

for`n`

in naturals.)a notion of equality

In proof theory, types are propositions and terms of a type are their proofs. In type theory, types are programs / constructions and terms are algorithms / recipes. In category theory, types are objects (spaces) and terms are generalised elements (points in the space).

## Non-dependent Types

false / empty / initial object

true / unit / terminal object

or / sum / coproduct

and / pairs / product

implication / functions / internal hom

## Dependent Types

predicate / type family / bundle

substitution / substitution / pullback (of bundles)

existence / Σ type / total space of bundles

for all / Π type / space of sections of bundles

## What is ‘the Same’?

The last missing piece is a notion of *equality*.
How HoTT treats equality is where it deviates from its predecessors.