Equality and Identity types [00D1]

    A distinguishing feature of MLTT is the introduction of intentional equality in addition to the strict syntactic definitional equality. This way we can use MLTT to talk about equality just like other propositions that we model using types.

    The formation rule for the family of identity types states that given any two terms we may form the type of identifications between them.

    The introduction rule essentially states that things that are judgementally equal should have a canonical witness of equality inhabiting the identity type. We call this witness . In order words, equality should be reflexive.

    TODO

    TODO

    When doing mathematics using HoTT we will (almost) never talk about definitional equality between things. We can see it more as a mechanism to reduce terms.

    • The difference between judgemental equality and intentional equality

    • MLTT undespecifies the identity types

      • Axiom K

    • Why J does not proof that every path is refl

      • short answer: It would not even typechek