## § HoTTesT: Identity types

- lecture .
- We already have judgemental equality. (computational equality: beta eta alpha equality).
- We will next introduce propositional equality.
- Proving an equality => constructing a term of the type of equalities.
- We can prove many judgemental equalities (eg.
`add x 0 =judgement= x`

), but not all the ones we want (eg. `add 0 x =judgement= x`

). - We can't because we need to do induction on
`x`

. - When we use natural number elimination / induction, we must produce a term of a type.
- What type?!
- Type constructors internalize structure. Eg. at a meta level, we can talk about contexts
`x:A, y:B(x), z:C(x,y)`

. - But internally, we will need to be able to talk about contents, we can use sigma types!
`Σ(x:A) Σ(y: Bx) Σ z:C(x, y)`

lets us internalize contexts! - Similarly, we can think about dependent terms as
`meta`

functions. Example, `x:A,y:B(x) |- c(x,y): C(x, y)`

. We can think of this as a function that takes an `x`

and a `y`

and produce a `c(x,y)`

. See that pi types internalize this notion! `c: (x:A) -> (y: B(x)) -> C(x,y)`

. - Bool, Nat, etc. are internalizing the usual booleans, naturals, etc.
- The universe type internalizes the judement
`A is a type`

via `A: Type`

. - The identity type internalizes the meta notion of judgemental equality (how? Doesn't it prove strictly more?)

#### § Identity Type

- $=$-formation: A type
`a: A`

, `b: B`

, then we have a type `a =A b type`

. -
`=`

-intro: `a:A| r_a: a =A a`

. ( `r`

= reflexivity). -
`=`

-elim: `x: A, y: A, z: x =A y |- D(x, y, z) type`

, and given `x:A |- d: D(x, x, r_x)`

, then we have `ind=(d, x, y, z): D(x, y, z)`