From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 12866 invoked from network); 8 Oct 2022 13:59:27 -0000 Received: from mail-yb1-xb3e.google.com (2607:f8b0:4864:20::b3e) by inbox.vuxu.org with ESMTPUTF8; 8 Oct 2022 13:59:27 -0000 Received: by mail-yb1-xb3e.google.com with SMTP id t6-20020a25b706000000b006b38040b6f7sf7095862ybj.6 for ; Sat, 08 Oct 2022 06:59:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:message-id:to:from:date:sender:from:to:cc:subject:date :message-id:reply-to; bh=BtaBrqy/lBy1HL7fJBcBUtHl+jmR5L/BvsxmPgD1zho=; b=ihjSva3MhEn1fVoQNl1HpXwItHbfB25E5T+LHFDwoOiHs0nsG6wx/hmBPilETvewvd +XQyJkmNaWPrJodPeSTQNkAuUh3HCViTGtzr05E7QsY/BtN2xLDVahwB3T8yHyJecvT2 OChiVY5FtagE3ckE2Aep+wQzC8kaZbR80gi3+kHS4UADcBnAdkkn3ulmP6fG2nuSxktl Dx+0+AX5mWRSzRVwSJmR308chjY/5u3go9VcLCMtgZTvg+nRLTUBtn9flCEqUo2cMLkm L47J9CW9n0LQv4rtOmURglcmYcCXu8e+12GMlrA0bjD9eZpao2LJBbXMo5hmiKoL6nOF GmkQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:message-id:to:from:date:from:to:cc:subject:date:message-id :reply-to; bh=BtaBrqy/lBy1HL7fJBcBUtHl+jmR5L/BvsxmPgD1zho=; b=UWVfV1732b2phCHe+2DXl3GAz8TxjU1j7c48RR1PXEmUGOplGpXVU2BlNet+/vzoky hwdpuIVvOhgrFZix90ZjkhxcmNeSnXirSfJbn8zkflObmRM0Ftk5WJWX1VdVZ/GGrQRr 99w93rkV2a8IrWVjMMNt9TrKzqnjUrboSv7JcbBdhKFLF0RXhRGTIeUnTEWhFZO2KqdT qaywB5ZfAn3mR0EtOGnCWeYK1OOJzJvlfNnepxD7gXs9J3MfzkQxNaQHa+CaXV0AKFvM woit9RGIjqUa3ucE0iEFWiN6ISaDC8L6aPdwfUpih4FaOWjWg2DjmBaq0Z4QDI3j8jAZ dDSQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:message-id:to:from:date:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to; bh=BtaBrqy/lBy1HL7fJBcBUtHl+jmR5L/BvsxmPgD1zho=; b=OvY1SnXQMQXKDZ/ss5F1nWOhV0+X95nOV6ZVWmuFdkE3rX3znqA0RDW4Sq+wumBaPL Zzh0KA2eD2S9srZL63si410NNrnxAZ2b6R3KQ6G5XufdcZDptpQcm0jgpWPvws6G6kDW QaMoGggceoJpR6eJRT/o5Fdw3vhQgm8XK52dWVPrqExU1D608XiLf3DLgZ/uuz0yk9N0 +8jYK1krORo6JWfmGOe3gEv4YBPu/axyrvoTcVmvM20HMHpZTA6iHT67IwbVwE1Eac8L W7/80acxmnCcKpMomyjbQ7nriBnWvGkZcANFtEWgzI4ZGhAGfSuIIVoEJQQCthyAjcB+ oTCg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ACrzQf0gkDg9KwxTOV1Tmv9M+VZ16HCu3PCfxdbvdw5maVJ4uUva3OJK HJuyMD9w9tcyDoXBqG4apqg= X-Google-Smtp-Source: AMsMyM4d6gy2LBlZpTOPcyxi/89CjAmAEM0Yl3iy7nMYwrmzgNyHQEFt6FbQ5xpZb+pkARHXkWHE0w== X-Received: by 2002:a81:54b:0:b0:35d:aa97:6038 with SMTP id 72-20020a81054b000000b0035daa976038mr9024263ywf.269.1665237565118; Sat, 08 Oct 2022 06:59:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:9a4b:0:b0:358:dd81:29f6 with SMTP id r72-20020a819a4b000000b00358dd8129f6ls3018996ywg.10.-pod-prod-gmail; Sat, 08 Oct 2022 06:59:24 -0700 (PDT) X-Received: by 2002:a81:5c7:0:b0:35f:1dbd:c4b6 with SMTP id 190-20020a8105c7000000b0035f1dbdc4b6mr9030007ywf.196.1665237564050; Sat, 08 Oct 2022 06:59:24 -0700 (PDT) Received: by 2002:a81:1350:0:b0:34d:1311:b1ee with SMTP id 00721157ae682-35fb5d44e54ms7b3; Sat, 8 Oct 2022 04:06:04 -0700 (PDT) X-Received: by 2002:a0d:d907:0:b0:355:dace:4214 with SMTP id b7-20020a0dd907000000b00355dace4214mr8311721ywe.400.1665227163623; Sat, 08 Oct 2022 04:06:03 -0700 (PDT) Date: Sat, 8 Oct 2022 04:06:03 -0700 (PDT) From: Madeleine Birchfield To: Homotopy Type Theory Message-Id: <3ff0b19b-0db2-4b63-b75d-3da9101a2f96n@googlegroups.com> Subject: [HoTT] Identity types of types, and univalence for the entire type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2898_873972986.1665227163362" X-Original-Sender: madeleinebirchfield@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , ------=_Part_2898_873972986.1665227163362 Content-Type: multipart/alternative; boundary="----=_Part_2899_2021547069.1665227163362" ------=_Part_2899_2021547069.1665227163362 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I've had an idea that's been bouncing around in my head for a few days, and= =20 I'd thought I'd share it with the rest of the community to see if it it=20 makes sense or if there are any flaws in my thought process.=20 We work in Martin-L=C3=B6f type theory with a separate judgment 'A type' fo= r=20 types, as well as weakly Tarski universes consisting of a type U and a type= =20 family El. The latter means that the type reflection of the internal types= =20 is only equivalent to the corresponding type outside the universe: for=20 example, the type reflection of the internal type of natural numbers N_U := =20 U is only equivalent to the type N, El(N_U) =E2=89=85 N, rather than defini= tionally=20 equal to N. In weakly Tarski universes, we define a type A to be U-small if= =20 there exists a term A_U : U with an equivalence small(A, A_U):El(A_U) =E2= =89=85 A.=20 The univalence axiom on weakly Tarski universes than implies that the=20 identity type A =3D_U B is U-small for all A:U and B:U. This in turn implie= s=20 that in any weakly Tarski universe, it is consistent that there is a=20 function =3D'_U:(U =C3=97 U) -> U and an equivalence small(A =3D'_U B):T(A = =3D'_U B) =E2=89=85=20 (A =3D_U B) for all A:U and B:U. This means that the univalence axiom could= =20 be internalized inside of the the universe U itself as ua:T((A =3D'_U B) = =E2=89=85_U=20 (A =E2=89=85_U B)), and type reflection implies that the type T((A =3D'_U B= ) =E2=89=85_U (A=20 =E2=89=85_U B)) =E2=89=85 (A =3D_U B =E2=89=85 T(A =E2=89=85_U B)) is point= ed for all A:U and B:U.=20 On the level of the type theory itself, one should thus be able to add=20 another type former to the entirety of the type theory: the identity types= =20 of types A =3D B, with the following rules:=20 - The formation rule says that given a judgment 'A type' in context=20 Gamma and a judgment 'B type' in context Gamma, one could form the=20 conclusion 'A =3D B type' in context Gamma.=20 - The introduction rule says that given a judgment 'A type' in context= =20 Gamma, one could form the conclusion 'refl_A:A =3D A' in context Gamma.= =20 - The elimination rule says that given a judgment 'A type' in context=20 Gamma, a judgment 'B type' in context Gamma, a judgment 'C(p) type' in t= he=20 context 'Gamma, p : A =3D B', and a judgment 't:C(refl_A)' in the contex= t=20 'Gamma', one could form the conclusion 'J(t, p): C(p)' in the context=20 'Gamma' - The computation rule says that given a judgment 'A type' in context=20 Gamma, a judgment 'B type' in context Gamma, a judgment 'C(p) type' in t= he=20 context 'Gamma, p : A =3D B', and a judgment 't:C(refl_A)' in the contex= t=20 'Gamma', one could form the conclusion 'J(t, refl_A) =E2=89=A1 t'' in th= e context=20 'Gamma'.=20 The type theory has two notions of propositional equality which all have an= =20 inductive definition, one for the identity types of terms of a type (a =3D_= A=20 b for a:A and b:A), and a second for the identity types of types (A =3D B f= or=20 A type and B type).=20 Provided all of the above is correct, this allows us to define univalence= =20 in the entire type theory without using universes at all. Given types A and= =20 B, one could inductively define the function idtoequiv_{A, B}:(A =3D B) -> = (A=20 =E2=89=85 B) by idtoequiv_{A, A}(refl_A) :=3D id_A. The univalence axiom th= en says=20 that one could form the term ua_{A, B}:isEquiv(idtoequiv_{A, B})) for=20 whatever definition of isEquiv is used.=20 In addition, since there are two identity types, there are now two notions= =20 of UIP and axiom K: one for the identity types of terms and one for the=20 identity types of types: - UIP for terms is the rule that given the judgments 'A type', 'a:A',=20 'b:A', 'p:a =3D_A b', 'q:a =3D_A b' all in context Gamma, one could form= the=20 conclusion 'uip(A, a, b, p, q):p =3D_{a =3D_A b} q' - UIP for types is the rule that given the judgments 'A type', 'B type',= =20 'p:A =3D B', 'q:A =3D B' all in context Gamma, one could form the conclu= sion=20 'uip(A, B, p, q):p =3D_{A =3D B} q' - axiom K for terms is the rule that given the judgments 'A type',=20 'a:A', 'p:a =3D_A a' all in context Gamma, one could form the conclusion= =20 'uip(A, a, p):p =3D_{a =3D_A a} refl_A(a)' - axiom K for types is the rule that given the judgments 'A type', 'p:A= =20 =3D A' all in context Gamma, one could form the conclusion 'uip(A, p):p = =3D_{A=20 =3D A} refl_A' Assuming univalence for the type theory, UIP or axiom K for the identity=20 types of terms implies that every type is a set as usual, but does not=20 necessarily imply UIP or axiom K for the identity types of types. But UIP= =20 or axiom K for the identity types of types implies that every type is a=20 proposition and thus a set, and thus implies UIP and axiom K for the=20 identity types of types. However, both sets of axioms of UIP and axiom K=20 are still inconsistent with the existence of a univalent Tarski universe in= =20 the type theory, even without univalence for the entire type theory.=20 Madeleine Birchfield --=20 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 e= mail 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= . ------=_Part_2899_2021547069.1665227163362 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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.
<= div>
We work in Martin-L=C3=B6f type theory with a separate j= udgment 'A type' for types, as well as weakly Tarski universes consisting o= f 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 natu= ral numbers N_U : U is only equivalent to the type N, El(N_U) =E2=89=85 N, = rather than definitionally equal to N. In weakly Tarski universes, we defin= e 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) =E2=89=85 A.

The univalence axiom on weakly = Tarski universes than implies that the identity type A =3D_U B is U-small f= or all A:U and B:U. This in turn implies that in any weakly Tarski universe= , it is consistent that there is a function =3D'_U:(U =C3=97 U) -> U and= an equivalence small(A =3D'_U B):T(A =3D'_U B) =E2=89=85 (A =3D_U B) for a= ll 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 =3D'_U B) =E2=89=85_U (A =E2= =89=85_U B)), and type reflection implies that the type T((A =3D'_U B) =E2= =89=85_U (A =E2=89=85_U B)) =E2=89=85 (A =3D_U B =E2=89=85 T(A =E2=89=85_U = B)) is pointed for all A:U and B:U.

On the le= vel 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 = =3D 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 =3D B type' in context= Gamma.
  • The introduction rule says that given a judgment 'A ty= pe' in context Gamma, one could form the conclusion 'refl_A:A =3D A' in con= text 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 =3D 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=20 Gamma, a judgment 'C(p) type' in the context 'Gamma, p : A =3D B', and a=20 judgment 't:C(refl_A)' in the context 'Gamma', one could form the conclusio= n 'J(t, refl_A) =E2=89=A1 t'' in the context 'Gamma'. 
T= he 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 =3D_= A b for a:A and b:A), and a second for the identity types of types (A =3D B= for A type and B type).

Provided all of the = above is correct, this allows us to define univalence in the entire type th= eory without using universes at all. Given types A and B, one could inducti= vely define the function idtoequiv_{A, B}:(A =3D B) -> (A =E2=89=85 B) b= y idtoequiv_{A, A}(refl_A) :=3D id_A. The univalence axiom then says that o= ne could form the term ua_{A, B}:isEquiv(idtoequiv_{A, B})) for whatever de= finition of isEquiv is used.

In addition, since there are two ident= ity types, there are now two notions of UIP and axiom K: one for the identi= ty 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 =3D_A b', 'q:a =3D_A b' all in context Gamma, one could form the con= clusion 'uip(A, a, b, p, q):p =3D_{a =3D_A b} q'
  • UIP for types is t= he rule that given the judgments 'A type', 'B type', 'p:A =3D B', 'q:A =3D = B' all in context Gamma, one could form the conclusion 'uip(A, B, p, q):p=20 =3D_{A =3D B} q'
  • axiom K for terms is the rule that given the judgm= ents 'A type', 'a:A', 'p:a =3D_A a' all in context Gamma, one could form the conclusion 'uip(A, a, p):p=20 =3D_{a =3D_A a} refl_A(a)'
  • axiom K for types is the rule that given= the judgments 'A type', 'p:A =3D A' all in context Gamma, one could form the conclusion 'uip(A, p):p=20 =3D_{A =3D A} refl_A'
Assuming univalence for the type = theory, UIP or axiom K for the identity types of terms implies that every t= ype is a set as usual, but does not necessarily imply UIP or axiom K for th= e identity types of types. But UIP or axiom K for the identity types of typ= es implies that every type is a proposition and thus a set, and thus implie= s UIP and axiom K for the identity types of types. However, both sets of ax= ioms of UIP and axiom K are still inconsistent with the existence of a univ= alent Tarski universe in the type theory, even without univalence for the e= ntire type theory.

Madeleine Birchfield

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/3ff0b19b-0db2-4b63-b75d-3da9101a2f96n%40googl= egroups.com.
------=_Part_2899_2021547069.1665227163362-- ------=_Part_2898_873972986.1665227163362--