# 1.7 Types and Universes

Lean is a dependently typed system. Every expression has a type, and types themselves are classified by *universes*. Understanding this hierarchy explains why definitions typecheck, how polymorphism works, and why some constructions require explicit universe control.

## Problem

You want to understand what `Type`, `Prop`, and universe levels mean, how Lean prevents paradoxes, and how to write definitions that work uniformly across many types.

## Solution

Use `#check` to inspect universe levels and observe how Lean assigns types to types.

```lean
#check Nat
#check Type
#check Type 1
#check Prop
```

Typical output:

```text
Nat : Type
Type : Type 1
Type 1 : Type 2
Prop : Type
```

This reveals the key structure:

* `Nat` is a type
* `Type` is itself a type, but at a higher level
* universes form a hierarchy `Type 0`, `Type 1`, `Type 2`, ...
* `Prop` is a special sort used for logical statements

## Universe Hierarchy

Lean avoids logical inconsistencies by stratifying types into levels.

The hierarchy is:

```text
Type 0 : Type 1 : Type 2 : Type 3 : ...
```

By convention:

* `Type` means `Type 0`
* `Type 1` is the next universe
* and so on

You can check:

```lean
#check Type 0
#check Type 1
#check Type 2
```

Each level lives in the next.

This prevents self-referential definitions such as "the type of all types that do not contain themselves".

## `Prop` vs `Type`

`Prop` is the universe of logical propositions.

```lean
#check True
#check False
#check 1 = 1
```

Output:

```text
True : Prop
False : Prop
1 = 1 : Prop
```

Key differences:

| Feature         | `Prop`             | `Type`               |
| --------------- | ------------------ | -------------------- |
| Purpose         | logical statements | data and computation |
| Computation     | erased             | retained             |
| Proof relevance | irrelevant         | relevant             |

Proofs in `Prop` are not used for computation. Lean treats them as logically meaningful but computationally irrelevant.

Example:

```lean
def f (n : Nat) (h : n = n) : Nat :=
  n
```

The argument `h` is ignored at runtime.

## Functions Between Types

A function type:

```lean
Nat -> Nat
```

means a function from `Nat` to `Nat`.

More generally:

```lean
α -> β
```

where `α` and `β` are types.

Dependent functions allow the result type to depend on the input:

```lean
(x : Nat) -> Fin (x + 1)
```

This expresses that the result type varies with `x`.

## Polymorphism

Lean supports polymorphic definitions using type parameters.

```lean
def identity (α : Type) (x : α) : α :=
  x
```

Check:

```lean
#check identity
```

Result:

```text
identity : (α : Type) -> α -> α
```

This function works for any type `α`.

Using implicit arguments:

```lean
def identity' {α : Type} (x : α) : α :=
  x
```

Now Lean infers `α`:

```lean
#check identity' 5
#check identity' true
```

## Universe Polymorphism

A more general definition works across universe levels:

```lean
universe u

def id_univ {α : Type u} (x : α) : α :=
  x
```

Here:

* `u` is a universe variable
* `α` may live in any universe

Check:

```lean
#check id_univ
```

Result:

```text
id_univ : {α : Type u} -> α -> α
```

Without universe polymorphism, definitions would be restricted to `Type 0`.

## Example: Polymorphic Container

```lean
universe u

structure Box (α : Type u) where
  val : α
```

Check:

```lean
#check Box
```

Result:

```text
Box : Type u -> Type u
```

This works uniformly for any universe level.

## Dependent Types

Dependent types allow types to depend on values.

```lean
def vector (α : Type) (n : Nat) := Fin n -> α
```

Here the type depends on `n`.

Example usage:

```lean
#check vector Nat 3
```

Result:

```text
vector Nat 3 : Type
```

Dependent types are central to encoding precise specifications.

## Implicit Universe Inference

Lean usually infers universe levels automatically.

```lean
def const {α β : Type} (x : α) (y : β) : α :=
  x
```

Lean assigns universe variables behind the scenes.

Only introduce explicit universes when needed.

## Common Pitfalls

If Lean reports a universe mismatch, the types live in incompatible universe levels.

If a definition works for `Nat` but not for general types, it may be missing polymorphism.

If implicit arguments fail, the universe parameter may need to be explicit.

If types become too large, inspect their universe levels with `#check`.

## Minimal Working Example

```lean
universe u

def pair {α : Type u} (x y : α) : α × α :=
  (x, y)

#check pair 3 4
```

Expected:

```text
pair 3 4 : Nat × Nat
```

## Takeaway

Types in Lean are organized into a hierarchy of universes. `Type` classifies data, `Prop` classifies logical statements, and universe levels prevent inconsistencies. Polymorphism and dependent types allow definitions to work uniformly across many structures. Understanding this system is necessary for writing general, reusable, and correct Lean code.