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 3659 invoked from network); 4 Feb 2023 13:59:42 -0000 Received: from mail-qt1-x83c.google.com (2607:f8b0:4864:20::83c) by inbox.vuxu.org with ESMTPUTF8; 4 Feb 2023 13:59:42 -0000 Received: by mail-qt1-x83c.google.com with SMTP id i5-20020ac813c5000000b003b86b748aadsf4034213qtj.14 for ; Sat, 04 Feb 2023 05:59:42 -0800 (PST) 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=0AZ5zbPmduOCeiyRDVarfeSCMaHHWrXzsMrYOUFc8xI=; b=Qsq8XEhB/MONtiwSPOzVqBxDUkzkOxSqxbJHZen+KEqTIfgALUgaVmXafO1iSqKL/0 RN5NwexQJMpR1vborhH6qAki/3Ru3gjZwUISP2J5Z27yf/fzoYtnUnBmpbZ2p+5cz1yz ZRzHMKWUca7t+J4V7rBtCkW2pFGDMFvPGFG/Xk3q+F1SYr2qIEWY8rEBQSIN4wMS6NLL fILYBD9o1xo4sL7mGJ7+8oIXPyC0bT4VA8DZLMJL9cC4cV+2xrzC8hJT1ZBbHhcv8KrG Ob5Kd/PMu+vd8D9sEAijDTguGrWdSCYeFOHsnXP1AONNYUdAnsqKC+q/BPzeYhgJjDFt nGJQ== 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=0AZ5zbPmduOCeiyRDVarfeSCMaHHWrXzsMrYOUFc8xI=; b=OtJTognJTHexg9PlczQG8++AgyXVvtESMtoLZD3IwcHsHb5upCJOgIOoB36jGHFsRm AlXSNg718H72TCcRXMDfvLfIJT1JRdyLwUC4V6c594Rel9fT5QT/duecyL689TZHDnS5 gyFI3xnwcACEaND5FtQ12m8PkCJh1I+fFAPhGdVWLi6UcSp8cmwVVvM7yROhAWp+4lXh HiG4RlbGWneile1uqtbWgGjbESjzwap2VTynWbJcsexIdDgEceBnx1yA4eM3y53eBLlF mTqxyO0J6aTyNkroCK+weXSCyzvfBQvwP1OsHwnaAWRGldbwkXk34f3U2KAcFN3nhkwM UNPA== 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=0AZ5zbPmduOCeiyRDVarfeSCMaHHWrXzsMrYOUFc8xI=; b=vigxClZxc3zBRM1v/xPLPNbux9jCcnuQ3IaVjbCs0ZS8Vw2shsQwhWkvYhXm166o/E vO7TOn5rgkfgy+tHdyhSuTYjt6KSZFCY3CWZ2WmikSZktedjwzZCM3vQH/RvMEoEVxf+ s2irWkGcDxG4qpSocfLn3AQj6tcdvtFDSXIrQF4Ob3GXyXa+uVzRW5X579chbcj2Ar9q 7Hj3E4upUJpqUqjSa22SmI3tDHtHC8VN4FG7mALwbmIHuoiJfF1sy2x2IjlZllz00MBa idzqTr48ppOxVJ1nio/xEIK3u0aPN6IHc6YmzStZ+/R3z95HhqAb7Dv5eb3hr7S86Ubj 12kw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKXhN2M89GcHExRQ92v5GYJkqyHz1K3ZlTbIONmk59lh5XK1bsXH OSIZC2UYFQ4ar+C6twAm4nY= X-Google-Smtp-Source: AK7set+dTt9ktV0EHJJ9H4eOaLX96gtldPDeoGBys+tJOPtV8MKR9zIkQXneTdO9+TksaLgxQy3XQQ== X-Received: by 2002:a05:620a:ce5:b0:719:befa:de21 with SMTP id c5-20020a05620a0ce500b00719befade21mr1083611qkj.101.1675519178447; Sat, 04 Feb 2023 05:59:38 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:622a:a17:b0:3b1:7ae:61e4 with SMTP id bv23-20020a05622a0a1700b003b107ae61e4ls8196726qtb.0.-pod-prod-gmail; Sat, 04 Feb 2023 05:59:37 -0800 (PST) X-Received: by 2002:a05:622a:512:b0:3b7:fd8a:fe28 with SMTP id l18-20020a05622a051200b003b7fd8afe28mr1528792qtx.344.1675519177332; Sat, 04 Feb 2023 05:59:37 -0800 (PST) Received: by 2002:a05:620a:3186:b0:6fb:b4b9:8a32 with SMTP id af79cd13be357-72e6e43ec14ms85a; Sat, 4 Feb 2023 05:56:37 -0800 (PST) X-Received: by 2002:ae9:c109:0:b0:729:c6db:6cff with SMTP id z9-20020ae9c109000000b00729c6db6cffmr1076510qki.308.1675518997230; Sat, 04 Feb 2023 05:56:37 -0800 (PST) Date: Sat, 4 Feb 2023 05:56:36 -0800 (PST) From: Madeleine Birchfield To: Homotopy Type Theory Message-Id: <45bf6ae5-b73b-4df2-a8bc-9aca972797e1n@googlegroups.com> Subject: [HoTT] Definitional equality of types as strict bijection MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_4128_680995290.1675518996952" 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_4128_680995290.1675518996952 Content-Type: multipart/alternative; boundary="----=_Part_4129_817006582.1675518996952" ------=_Part_4129_817006582.1675518996952 Content-Type: text/plain; charset="UTF-8" In this thread, I follow the approach in Egbert Rijke's textbook in having a separate type judgment, rather than the HoTT book's judgment in having an infinite tower of universes and no separate type judgment, and I follow Agda in using the bare equals sign for definitional equality. In structural set theories like William Lawvere's ETCS or Mike Shulman's SEAR it is quite common to have equality only for the sorts of elements, functions, and relations, and not have any primitive equality relation for the sort of sets. This means that the only way to compare sets for "equality" is through a bijection of sets. In addition, Mike Shulman's talks on Higher Observational Type Theory back in May of 2022 includes a section where he talks about the right notion of "definitional univalence" is not using the usual notion of definitional equality of types, but rather strict bijection, where there are functions idtoequiv(a, b):Id_U(a, b) -> Equiv_U(a, b) equivtoid(a, b):Equiv_U(a, b) -> Id_U(a, b) between the identity types Id_U(a, b) and the type of equivalences Equiv_U(a, b) of elements a:U and b:U of a universe U, and definitional equalities of elements equivtoid(a, b)(idtoequiv(a, b)(p)) = p:Id_U(a, b) idtoequiv(a, b)(equivtoid(a, b)(R)) = R:Equiv_U(a, b) Using insights from structural set theory, one could go beyond definitional univalence in Mike Shulman's Higher Observational Type Theory and directly modify the structural rules for definitional equality of types so that it behaves not as an equivalence relation a la first order logic with equality, but rather strict bijection of types a la structural set theory, using the following rules: Gamma |- A = B type --------------------------------- Gamma, x:A |- f(x):B Gamma |- A = B type --------------------------------- Gamma, y:B |- g(y):A Gamma |- A = B type --------------------------------- Gamma, x:A |- g(f(x)) = x:A Gamma |- A = B type --------------------------------- Gamma, y:B |- f(g(y)) = y:B The variable conversion rule in dependent type theory then becomes substitution of g(y) for x, Gamma |- A = A' type Gamma, x:A, Delta(x) |- J(x) ------------------------------------------------------------------------------------ Gamma, y:A', Delta(g(y)) |- J(g(y)) The first congruence rule for substitution is the following rule Gamma |- a = a':A Gamma, x:A, Delta(x) |- B(x) type ------------------------------------------------------------------------------------ Gamma, Delta(a) |- B(a) = B(a') type and the strict bijection rules for definitional equality of types implies that f and g for the definitional equality B(a) = B(a') type are judgmental versions of transport. The second congruence rule for substitution becomes merely a judgmental version of application to paths: Gamma |- a = a':A Gamma, x:A, Delta(x) |- b(x):B(x) type ------------------------------------------------------------------------------------------ Gamma, Delta(a) |- b(a) = g(b(a')):B(a) Definitional univalence then becomes under this collection of structural rules the following rule Gamma |- U type Gamma |- A:U Gamma |- B:U ------------------------------------------------------------------------------------------ Gamma |- Id_U(A, B) = Eq_U(A, B) type from which one could derive Mike Shulman's original 4 rules for definitionally univalent universes. 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/45bf6ae5-b73b-4df2-a8bc-9aca972797e1n%40googlegroups.com. ------=_Part_4129_817006582.1675518996952 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In this thread, I follow the approach in Egbert Rijke's textbook in ha= ving a separate type judgment, rather than the HoTT book's judgment in=20 having an infinite tower of universes and no separate type judgment, and I follow Agda in using the bare equals sign for definitional equality.

In structural set theories like William Lawv= ere's ETCS or Mike Shulman's SEAR it is quite common to have equality only for the sorts of=20 elements, functions, and relations, and not have any primitive equality=20 relation for the sort of sets. This means that the only way to compare=20 sets for "equality" is through a bijection of sets.

In add= ition, Mike Shulman's talks on Higher Observational Type Theory back in May= of 2022 includes a section where he talks about the right notion of "defin= itional univalence" is not using the usual notion of definitional equality = of types, but rather strict bijection, where there are functions
idtoequiv(a, b):Id_U(a, b) -> Equiv_U(a, b)
equivtoid(a= , b):Equiv_U(a, b) -> Id_U(a, b)
between the identity t= ypes Id_U(a, b) and the type of equivalences Equiv_U(a, b) of elements a:U = and b:U of a universe U, and definitional equalities of elements
equiv= toid(a, b)(idtoequiv(a, b)(p)) =3D p:Id_U(a, b)
idtoequiv(a, b)(equivt= oid(a, b)(R)) =3D R:Equiv_U(a, b)

Using insights from struc= tural set theory, one could go beyond definitional univalence in Mike Shulm= an's Higher Observational Type Theory and directly modify the structural ru= les for definitional equality of types so that it behaves not as an equival= ence relation a la first order logic with equality, but rather strict bijec= tion of types a la structural set theory, using the following rules:
<= br />
Gamma |- A =3D B type
---------------------= ------------
Gamma, x:A |- f(x):B

Gamm= a |- A =3D B type
---------------------------------
Gamma, y:B |- g(y):A

Gamma |- A =3D B type
---------------------------------
Gamma, x:A |- g(f= (x)) =3D x:A

Gamma |- A =3D B type
---------------------------------
Gamma, y:B |- f(g(y)) =3D y:= B

The variable conversion rule in dependent type theory then bec= omes substitution of g(y) for x,

Gam= ma |- A =3D A' type =C2=A0=C2=A0 Gamma, x:A, Delta(x) |- J(x)
------------------------------------------------------------------------= ------------
Gamma, y:A', Delta(g(y)) |- J(g(y))

The first congruence rule for substitution is the following rule

Gamma |- a =3D a':A=C2=A0=C2=A0=C2=A0 Gamma, x:A, Delta(x) |- B(x) t= ype
-------------------------------------------------------= -----------------------------
Gamma, Delta(a) |- B(a) =3D B(a') type
and the strict bijection rules for definitional equality of types= implies that f and g for the definitional equality B(a) =3D B(a') type are= judgmental versions of transport. The second congruence rule for substitut= ion becomes merely a judgmental version of application to paths:

Gamma |- a =3D a':A=C2=A0=C2=A0=C2=A0 Gamma, x:A, Delta(x) |- b(x):B(x) ty= pe
--------------------------------------------------------= ----------------------------------
Gamma, Delta(a) |- b(a) =3D g(b(a')= ):B(a)

Definitional univalence then becomes under this collectio= n of structural rules the following rule

Gamma |- U type=C2= =A0=C2=A0=C2=A0 Gamma |- A:U=C2=A0=C2=A0 Gamma |- B:U
-----= ---------------------------------------------------------------------------= ----------
Gamma |- Id_U(A, B) =3D Eq_U(A, B) type

from whi= ch one could derive Mike Shulman's original 4 rules for definitionally univ= alent universes.

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/45bf6ae5-b73b-4df2-a8bc-9aca972797e1n%40googl= egroups.com.
------=_Part_4129_817006582.1675518996952-- ------=_Part_4128_680995290.1675518996952--