Contents

# Contents

## Idea

A type theory where types behave like sets, i.e. in which all types are h-sets. Thus, it is a form of set-level foundations. This includes:

Set-level type theory contrasts with higher-level type theory such as homotopy type theory or plain intensional type theory, where types behave (at least potentially) like n-groupoids or even infinity-groupoids. In the other direction, it contrasts with type theories where types behave like propositions (type theories of this sort are often called logics).

## Set-level intensional type theories

In a set-level but intensional type theory, we distinguish definitional and propositional equality (unlike in extensional type theory), but no two terms can be propositionally equal in more than one way (up to propositional equality). In the language of homotopy type theory, this means that all types are h-sets. There are a number of equivalent ways to force this to be true by adding axioms to type theory.

1. We can add as an axiom the “uniqueness of identity proofs” (axiom UIP) property that any two inhabitants of the same identity type $Id_A(x,y)$ are themselves equal (in the corresponding higher identity type).

2. We can add Streicher’s axiom K which says that any inhabitant of a self-equality type $Id_A(x,x)$ is (propositionally) equal to the identity/reflexivity equality $1_x$. (Axiom K is so named because $K$ comes after $J$, and $J$ usually denotes the eliminator for identity types.)

3. In the presence of dependent sum types, we can add an axiom saying that if $(a,b_1)$ and $(a,b_2)$ are pairs in a dependent sum $\sum_{x\colon A} B(x)$ with the same first component, and the identity type $Id_{\sum_{x\colon A} B(x)}((a,b_1), (a,b_2))$ is inhabited, then so is $Id_{B(a)}(b_1,b_2)$.

4. We can allow definition of functions by a strong form of pattern matching, as in unmodified Agda. The relevant “extra strength” is to allow output types of a pattern match which are only well-defined after the pattern has been matched.

5. In cubical type theory (with glue types? removed, since univalence is incompatible with set-level-ness), we can add a boundary separation rule, leading to XTT.