§ 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
- 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
- The identity type internalizes the meta notion of judgemental equality (how? Doesn't it prove strictly more?)
§ Identity Type
- -formation: A type
b: B, then we have a type
a =A b type.
a:A| r_a: a =A a. (
r = reflexivity).
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)