 The first causes the distinction between propositional and judgmental equality to disappear. The second forces identity proofs to be unique. Unlike the rules for the intensional identity type former, the rules for extensional identity types do not fit into the schema for inductively defined types mentioned above.