§ 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)