*[HoTT] Identity types of types, and univalence for the entire type theory@ 2022-10-08 11:06 Madeleine Birchfield2022-10-08 23:41 ` Michael Shulman 0 siblings, 1 reply; 2+ messages in thread From: Madeleine Birchfield @ 2022-10-08 11:06 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 5276 bytes --] I've had an idea that's been bouncing around in my head for a few days, and I'd thought I'd share it with the rest of the community to see if it it makes sense or if there are any flaws in my thought process. We work in Martin-Löf type theory with a separate judgment 'A type' for types, as well as weakly Tarski universes consisting of a type U and a type family El. The latter means that the type reflection of the internal types is only equivalent to the corresponding type outside the universe: for example, the type reflection of the internal type of natural numbers N_U : U is only equivalent to the type N, El(N_U) ≅ N, rather than definitionally equal to N. In weakly Tarski universes, we define a type A to be U-small if there exists a term A_U : U with an equivalence small(A, A_U):El(A_U) ≅ A. The univalence axiom on weakly Tarski universes than implies that the identity type A =_U B is U-small for all A:U and B:U. This in turn implies that in any weakly Tarski universe, it is consistent that there is a function ='_U:(U × U) -> U and an equivalence small(A ='_U B):T(A ='_U B) ≅ (A =_U B) for all A:U and B:U. This means that the univalence axiom could be internalized inside of the the universe U itself as ua:T((A ='_U B) ≅_U (A ≅_U B)), and type reflection implies that the type T((A ='_U B) ≅_U (A ≅_U B)) ≅ (A =_U B ≅ T(A ≅_U B)) is pointed for all A:U and B:U. On the level of the type theory itself, one should thus be able to add another type former to the entirety of the type theory: the identity types of types A = B, with the following rules: - The formation rule says that given a judgment 'A type' in context Gamma and a judgment 'B type' in context Gamma, one could form the conclusion 'A = B type' in context Gamma. - The introduction rule says that given a judgment 'A type' in context Gamma, one could form the conclusion 'refl_A:A = A' in context Gamma. - The elimination rule says that given a judgment 'A type' in context Gamma, a judgment 'B type' in context Gamma, a judgment 'C(p) type' in the context 'Gamma, p : A = B', and a judgment 't:C(refl_A)' in the context 'Gamma', one could form the conclusion 'J(t, p): C(p)' in the context 'Gamma' - The computation rule says that given a judgment 'A type' in context Gamma, a judgment 'B type' in context Gamma, a judgment 'C(p) type' in the context 'Gamma, p : A = B', and a judgment 't:C(refl_A)' in the context 'Gamma', one could form the conclusion 'J(t, refl_A) ≡ t'' in the context 'Gamma'. The type theory has two notions of propositional equality which all have an inductive definition, one for the identity types of terms of a type (a =_A b for a:A and b:A), and a second for the identity types of types (A = B for A type and B type). Provided all of the above is correct, this allows us to define univalence in the entire type theory without using universes at all. Given types A and B, one could inductively define the function idtoequiv_{A, B}:(A = B) -> (A ≅ B) by idtoequiv_{A, A}(refl_A) := id_A. The univalence axiom then says that one could form the term ua_{A, B}:isEquiv(idtoequiv_{A, B})) for whatever definition of isEquiv is used. In addition, since there are two identity types, there are now two notions of UIP and axiom K: one for the identity types of terms and one for the identity types of types: - UIP for terms is the rule that given the judgments 'A type', 'a:A', 'b:A', 'p:a =_A b', 'q:a =_A b' all in context Gamma, one could form the conclusion 'uip(A, a, b, p, q):p =_{a =_A b} q' - UIP for types is the rule that given the judgments 'A type', 'B type', 'p:A = B', 'q:A = B' all in context Gamma, one could form the conclusion 'uip(A, B, p, q):p =_{A = B} q' - axiom K for terms is the rule that given the judgments 'A type', 'a:A', 'p:a =_A a' all in context Gamma, one could form the conclusion 'uip(A, a, p):p =_{a =_A a} refl_A(a)' - axiom K for types is the rule that given the judgments 'A type', 'p:A = A' all in context Gamma, one could form the conclusion 'uip(A, p):p =_{A = A} refl_A' Assuming univalence for the type theory, UIP or axiom K for the identity types of terms implies that every type is a set as usual, but does not necessarily imply UIP or axiom K for the identity types of types. But UIP or axiom K for the identity types of types implies that every type is a proposition and thus a set, and thus implies UIP and axiom K for the identity types of types. However, both sets of axioms of UIP and axiom K are still inconsistent with the existence of a univalent Tarski universe in the type theory, even without univalence for the entire type theory. Madeleine Birchfield -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/3ff0b19b-0db2-4b63-b75d-3da9101a2f96n%40googlegroups.com. [-- Attachment #1.2: Type: text/html, Size: 5605 bytes --] ^ permalink raw reply [flat|nested] 2+ messages in thread

*2022-10-08 11:06 [HoTT] Identity types of types, and univalence for the entire type theory Madeleine BirchfieldRe: [HoTT] Identity types of types, and univalence for the entire type theory@ 2022-10-08 23:41 ` Michael Shulman0 siblings, 0 replies; 2+ messages in thread From: Michael Shulman @ 2022-10-08 23:41 UTC (permalink / raw) To: Madeleine Birchfield;+Cc:Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 1462 bytes --] It's tempting to think that one can define univalence without universes, but I don't think this rule makes sense: On Sat, Oct 8, 2022 at 6:59 AM Madeleine Birchfield < madeleinebirchfield@gmail.com> wrote: > The elimination rule says that given a judgment 'A type' in context Gamma, > a judgment 'B type' in context Gamma, a judgment 'C(p) type' in the context > 'Gamma, p : A = B', and a judgment 't:C(refl_A)' in the context 'Gamma', > one could form the conclusion 'J(t, p): C(p)' in the context 'Gamma' In the ordinary Id-elimination rule, the motive C has to be defined in the context of two *variable* elements of the type and an equality between them, not two *specific* elements. In particular, if A and B are specific types, then it doesn't make sense to substitute refl_A for p in C, because you can't substitute A for B. You can only substitute for a variable. I think in order to do something like this, you have to augment type theory by some kind of "polymorphism" that will allow you to hypothesize a "type variable" in the context. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpwW0jL-EER%2BK3t7qs4_RegaB0CkZz6seMpRBw2SHGsr-Q%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 2231 bytes --] ^ permalink raw reply [flat|nested] 2+ messages in thread

end of thread, other threads:[~2022-10-08 23:42 UTC | newest]Thread overview:2+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2022-10-08 11:06 [HoTT] Identity types of types, and univalence for the entire type theory Madeleine Birchfield 2022-10-08 23:41 ` Michael Shulman

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).