So what is J really saying? And why is it valid in homotopy type theory? When there are more proofs of propositional equality than just reflexivity, why can you show something about all of them by just covering the case for reflexivity? An alternative to adding this axiom is to allow the kind of dependent pattern matching present in Agda and Epigram, which allow you to define K. From this, you can prove that any p : Id M M is equal to reflexivity, and from that you can prove that any p q : Id M N are propositionally equal (by reducing one to reflexivity using J). K says that to prove a predicate about Id M M, it suffices to cover the case for reflexivity. UIP can be added as an extra axiom, such as Streicher’s K: K : (A : Set) (M : A) (C : Id M M -> Set) This gives a model of type theory that validates J, but in which UIP does not hold. Here’s where things get confusing: UIP is not a consequence of J, as shown by the first higher-dimensional interpretation of type theory, Hofmann and Streicher’s groupoid interpretation. So, you would expect UIP to be a consequence, right? After all, by analogy, the induction principle for natural numbers tells you that the only natural numbers are zero and successor of a nat. J certainly seems to say that the only proof of Id is reflexivity-it reduces a goal that talks about an arbitrary proof to one that just covers the case of reflexivity. If you can give a branch b that, for each x, covers the case where the two terms are both x and related by reflexivity, then C holds for any two propositionally equal terms. J reads like an induction principle: C is a predicate on on two propositionally equal terms. J : (A : Set) (C : (x y : A) -> Id x y -> Set) Here is a statement of J, in Agda notation, writing Id x y for the identity (propositional equality) type, and Refl for reflexivity. J is the fundamental elimination rule for identity types, present in all (intensional) dependent type theories. What determines whether UIP holds? The answer lies in two elimination rules for identity types, called J and K. On the other hand, Coq does not provide uniqueness of identity proofs (but nor does it allow you to define higher-dimensional types that contract it, except by adding axioms). a universe (type of types), where equality is taken to be isomorphism, and there can be many different isomorphisms between two types. Homotopy type theory generalizes this picture to account for higher-dimensional types, where UIP does not hold–e.g. Several current proof assistants, such as Agda and Epigram, provide uniqueness of identity proofs (UIP): any two proofs of the same propositional equality are themselves propositionally equal.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |