From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x237.google.com (mail-oi1-x237.google.com [IPv6:2607:f8b0:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6db579de for ; Thu, 28 Nov 2019 20:34:01 +0000 (UTC) Received: by mail-oi1-x237.google.com with SMTP id n30sf13305935oij.9 for ; Thu, 28 Nov 2019 12:34:01 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=MnWcdN2SrdQzb9iiwzf/vMRjMWQIy5j5LBJ+/YaE/aM=; b=X/b+grGAZ4KtNGs6FbmdZX5U/gLMl/TrTLzQYZWF0KZL7NyWUuncvrFflybtNoyY80 E8X8w+RoWkhLEL9k+iKgoyysOPMTlfZuDKb3e3i67L67tsCmKMcrQxVgb5f1iYk3habt JsBcPVf/KeVRrx/CBwQjLZc2EDoMV2a/SIR4sWLu/w69y67scJ/d/uM9S3qLljHteJ5m dxj5jjT4eTFkUxZUETyvBPhr+8UtzIc1LMGkOY06JM8XLuO9hcKgv0i78H+T00U/Nmao tTeQL/8YTgBzS7qnzMZ5aJUV+tpU88kMabwTAR3AhtNmgZBlkSG2IKMl8f7GugVbQZro GfLg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=MnWcdN2SrdQzb9iiwzf/vMRjMWQIy5j5LBJ+/YaE/aM=; b=pg9WduHROIrZgosE63+RSCbmPh5np2wYKbIwGewJbCWIcM2mg05HpAuIDQuUew08Uf WlUVeQ91zvXsZXXiVIDA7ALv0txyyr6rNrVwAmYBph48TXidsRWXU5vTCbgWHrQblgKu R9r7n34wn4sgtygsbjQR4+K2zcKosYoEKpNhtFZ+wVVQ3pEKtFhCbY++umJkGpWfFYdc wQSStDhdDpM3C7JbsX5voJHkJvCCa+Vq1kh2sbKfdGA62rspIGO5kAFcMWz7AjwpDEQd y86ANm7aQHSZvAppcxp7ZB0F2vgwNKd7j4+MAY0QLt4i6iXXPDqzJFs7KLw8O7aSMlat 0SZg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=MnWcdN2SrdQzb9iiwzf/vMRjMWQIy5j5LBJ+/YaE/aM=; b=jQmyKs5fJr9pU0xKMAf93UAsQ+5IDt4jClYu1EWV5jMJbHk6n0yYl8gmprgan+VBeb 5ZWXaEA9ueZuCoMiT+qXYuzPXYHnlfWc7Fxk19xmUOweBWPeMGacSb0bwDlSLVSh8rEN VdmxqOH56dxyoaaShjv0l67cNkJAZfhJFzWoNpVpoDOCqm1x3XrFzNx/BQNAUSO2u2tL jzW/2tHhlsCl+5o/eKG+zLJVt3jpNxBoomMNgZ1I8WXcLIIrWdVm/avgGRq1v56IwTIF 1J68UNdn2DoGB5eawUo1BurIW8iJz8rTznrfC0JL/xeEj2VqRbj/MO2uU8P0Geb4NnR5 ddcg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV1Rb8rHGEu/BTVObZ2wa5hphoo28uZf/mQ+3IWFijWrDO5EjdH DLFvanUy3dmFP9vRPukVqYg= X-Google-Smtp-Source: APXvYqzeyV2Uc4sxIvDIIWHztEFTg8s5bacthCHidU+wtOZSem0ayYMWsZIgDHYbpaJPzt11pBA1Jg== X-Received: by 2002:a9d:4c17:: with SMTP id l23mr8370160otf.112.1574973239537; Thu, 28 Nov 2019 12:33:59 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d10:: with SMTP id 16ls4576619oin.7.gmail; Thu, 28 Nov 2019 12:33:59 -0800 (PST) X-Received: by 2002:aca:c74e:: with SMTP id x75mr10167399oif.140.1574973238719; Thu, 28 Nov 2019 12:33:58 -0800 (PST) Date: Thu, 28 Nov 2019 12:33:58 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: Subject: [HoTT] Type factorials MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2761_1896701578.1574973238243" X-Original-Sender: escardo.martin@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: , ------=_Part_2761_1896701578.1574973238243 Content-Type: multipart/alternative; boundary="----=_Part_2762_1032503400.1574973238244" ------=_Part_2762_1032503400.1574973238244 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Probably just for amusement only. (1) In the category of topological spaces (not up to homotopy), if X and Y= =20 are exponentiable and we topologize the space (X =E2=89=83 Y) of homeomorph= isms of=20 X and Y with the subspace topology, we get that co-derived-set (Y+1) =C3=97 (X =E2=89=83 Y) =E2=89=83 (X+1 =E2=89=83 Y= +1). The proof relies on classical logic. Exponentiability is only needed to make sense of (X =E2=89=83 Y) as a space= , and=20 hence we could alternatively work with compactly generated spaces, which=20 have all exponentials, but I haven't checked the above in that case (yet). The derived set, in the sense of Cantor, is the set of limit points. Here= =20 we consider its complement, with the subspace topology, which of course is= =20 the discrete topology. When X is the same space as Y, the above specializes to=20 co-derived-set (X+1) =C3=97 Aut X =E2=89=83 Aut (X+1), where Aut X is the space of auto (homeo)morphisms of X. Hence when X is discrete, so that it is its own coderived set, the above=20 specializes to the "factorial equation" (X+1) =C3=97 Aut X =E2=89=83 Aut (X+1). But if X is perfect in the sense of Cantor (has no isolated points), then= =20 instead we get=20 Aux X =3D Aut (X+1) because the coderived set of X+1 is homeomorphic to 1. (2) The above holds if we replace "space" by "homotopy type" and can be=20 proved in HoTT/UF, *this time without appealing to classical logic* (and I= =20 doubt appealing to classical logic can simplify the argument, because the= =20 argument seems to be as simple and direct as it can be). For this, we need the following definitions in HoTT/UF: * A point x is *isolated* if the type x=3Dy is decidable for all y:X. (Counter-example: any point of the circle.) * A type is *discrete* if all its points are isolated. (Example: natural numbers, the finite type Fin n with n elements.) * A space is *perfect* if it has no isolated points. (Example: the circle.) There is also a notion that doesn't arise above but that does arise in the= =20 proofs/constructions: * A point x is *h(omotopy)-isolated* if the type x=3Dy is a proposition,= =20 or a subsingleton, for every point y.=20 By local Hedberg, every isolated point is h-isolated. (3) In particular, if Fin n is the type with n elements,=20 Fin (n+1) =C3=97 Aut (Fin n) =E2=89=83 Aut (Fin (n+1)) from which we get Fin (n!) =E2=89=83 Aut (Fin n) by induction on n, as expected. (4) Although the above development uses HoTT/UF ideas crucially, only=20 function extensionality is needed to carry out the constructions and proofs= =20 (in particular, propositional extensionality and univalence are not needed)= . I had fun formalizing the above ideas in Agda: https://www.cs.bham.ac.uk/~mhe/agda-new/UF-Factorial.html https://www.cs.bham.ac.uk/~mhe/agda-new/ArithmeticViaEquivalence.html and so I wanted to share it here. Best, Martin =20 --=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/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com. ------=_Part_2762_1032503400.1574973238244 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Probably just for amusement only.

(1) In the category of topological spaces (not up to homotopy), if X = and Y are exponentiable and we topologize the space (X =E2=89=83 Y) of home= omorphisms of X and Y with the subspace topology, we get that
=C2=A0 =C2=A0co-derived-set (Y+1) =C3=97 (X =E2=89=83 Y)=C2=A0 = =E2=89=83=C2=A0 (X+1 =E2=89=83 Y+1).

The proof rel= ies on classical logic.

Exponentiability is only n= eeded to make sense of (X =E2=89=83 Y) as a space, and hence we could alter= natively work with compactly generated spaces, which have all exponentials,= but I haven't checked the above in that case (yet).

The derived set, in the sense of Cantor, is the set of limit points.= Here we consider its complement, with the subspace topology, which of cour= se is the discrete topology.

When X is the same sp= ace as Y, the above specializes to=C2=A0

=C2=A0 co= -derived-set (X+1) =C3=97 Aut X=C2=A0 =E2=89=83=C2=A0 Aut (X+1),
=
where Aut X is the space of auto (homeo)morphisms of X.

Hence when X is discrete, so that it is its own coderi= ved set, the above specializes to the "factorial equation"
<= div>
=C2=A0(X+1) =C3=97 Aut X=C2=A0 =E2=89=83=C2=A0 Aut (X+1)= .

But if X is perfect in the sense of Cantor (has = no isolated points), then instead we get=C2=A0

=C2= =A0Aux X =3D Aut (X+1)

because the coderived set o= f X+1 is homeomorphic to 1.

(2) The above holds if= we replace "space" by "homotopy type" and can be prove= d in HoTT/UF, *this time without appealing to classical logic* (and I doubt= appealing to classical logic can simplify the argument, because the argume= nt seems to be as simple and direct as it can be).

For this, we need the following definitions in HoTT/UF:

=C2=A0* A point x is *isolated* if the type x=3Dy is decidable for a= ll y:X.
=C2=A0 =C2=A0(Counter-example: any point of the circle.)<= /div>

=C2=A0* A type is *discrete* if all its points are= isolated.
=C2=A0 =C2=A0(Example: natural numbers, the finite typ= e Fin n with n elements.)

=C2=A0* A space is *perf= ect* if it has no isolated points.
=C2=A0 =C2=A0(Example: the cir= cle.)

There is also a notion that doesn't aris= e above but that does arise in the proofs/constructions:

=C2=A0* A point x is *h(omotopy)-isolated* if the type x=3Dy is a pr= oposition,=C2=A0
=C2=A0 =C2=A0or a subsingleton, for every point = y.=C2=A0

=C2=A0 =C2=A0By local Hedberg, every isol= ated point is h-isolated.


(3) In pa= rticular, if Fin n is the type with n elements,=C2=A0

<= div>=C2=A0 =C2=A0 Fin (n+1) =C3=97 Aut (Fin n)=C2=A0 =E2=89=83=C2=A0 Aut (F= in (n+1))

from which we get

=C2=A0 =C2=A0 Fin (n!) =E2=89=83 Aut (Fin n)

by= induction on n, as expected.

(4) Although the abo= ve development uses HoTT/UF ideas crucially, only function extensionality i= s needed to carry out the constructions and proofs (in particular, proposit= ional extensionality and univalence are not needed).

I had fun formalizing the above ideas in Agda:

= =C2=A0 https://www.cs.bham.ac.uk/~mhe/agda-new/UF-Factorial.html
= =C2=A0 https://www.cs.bham.ac.uk/~mhe/agda-new/ArithmeticViaEquivalence.htm= l

and so I wanted to share it here.

=
Best,
Martin


= =C2=A0 =C2=A0=C2=A0

--
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.co= m/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googleg= roups.com.
------=_Part_2762_1032503400.1574973238244-- ------=_Part_2761_1896701578.1574973238243--