From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.93.83 with SMTP id w80mr4131374ita.30.1498652532199; Wed, 28 Jun 2017 05:22:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.136.94 with SMTP id k91ls3499761iod.42.gmail; Wed, 28 Jun 2017 05:22:11 -0700 (PDT) X-Received: by 10.13.230.74 with SMTP id p71mr4165643ywe.113.1498652531014; Wed, 28 Jun 2017 05:22:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1498652530; cv=none; d=google.com; s=arc-20160816; b=agUZ5VGMWwPbCeSOszODB/sxvZl/1GqWeOuKL0xmh+DbOOH1S1g5N90aB1f+0+CgDf 4v5t3UvUBtqYqp++v/kDGYXlIwC2kalb5o8Onve+eThBNxcB7tfDySxI1FkFbQc8LPB1 /6aR8hbOuiK4cI9R9WK2QddfoFvXRDpxgOC3PjiM00FnkQAMOoordVScErSAPCo9U9Kh x5dO1a20yxV/Idijag83ra4cWNUhKeKz8Y3hrh/We5UCXfEq+pCX5KPIpVM/xNZVyIsv WJiIPOo1ZMKguwrru4dt8ptM7Rfg41EyFasD8mo4/wdvpXAGG/9nFzfqixCDOxqqPbY0 SYjg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature:arc-authentication-results; bh=ZC5BlFuDXFC9EFO46kAr67PITOg5LT9iBc2z1KPuAxg=; b=wtPY1WmhuVVdX+JP2P4rsaxT6PzUzZr3F3CfHAxN/0kpIFDINLeLnMij/ISXZXOE2z 89ku/yYMybuKaHyFZxv3nypjiILHMCy0B03fK9PobEFqbuYAJeV2vuJlph+OyeMeWHnn AcZ0y0XDTqQLprPZf9qLGqkP/0ib7iRth5WknNosIbaPZg6+4uu1TPVlrvDuwH1sqpp3 uUh+zIV6vT5vAWAJMeyFWgeT8vC90fk5HxSN5tW2oHu0WR8kWq9F1WIt+LQgPjYva6RI LMr18O/Rqduz6FfrqJCtJbKJsrvAvj+z3bB4uPLlRxgxtqM1GXkvTjLaoQ/kd+4Mj7R/ GBqg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@googlemail.com header.b=rI57lTZ8; spf=pass (google.com: domain of urs.sc...@googlemail.com designates 2607:f8b0:400e:c05::230 as permitted sender) smtp.mailfrom=urs.sc...@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com Return-Path: Received: from mail-pg0-x230.google.com (mail-pg0-x230.google.com. [2607:f8b0:400e:c05::230]) by gmr-mx.google.com with ESMTPS id l64si470022pfg.13.2017.06.28.05.22.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 28 Jun 2017 05:22:10 -0700 (PDT) Received-SPF: pass (google.com: domain of urs.sc...@googlemail.com designates 2607:f8b0:400e:c05::230 as permitted sender) client-ip=2607:f8b0:400e:c05::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@googlemail.com header.b=rI57lTZ8; spf=pass (google.com: domain of urs.sc...@googlemail.com designates 2607:f8b0:400e:c05::230 as permitted sender) smtp.mailfrom=urs.sc...@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com Received: by mail-pg0-x230.google.com with SMTP id f127so31133737pgc.0 for ; Wed, 28 Jun 2017 05:22:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding; bh=ZC5BlFuDXFC9EFO46kAr67PITOg5LT9iBc2z1KPuAxg=; b=rI57lTZ8hquineQ4bKtLi5J+H04CDx967wA+E3TePBafQqi/JveevFhdSC7P0ghjkz 11n3hRhjPMir7k5D8+ufxVWmPIcN+VnsGEpHHRA3jJVWpUegu4+CYCB11gRT0Q1P3Gc8 U3q/h0l0/zeZV3r6sudD34PwFhX9BkcjlvRTaDW/sMfMRUF4Iu3njnFQ2lx7PkrG+x2Z cL4EJ0zzvMxAfaZZwyg88rsPI7+faWqy0eIERVxbXFG6+NaeMB3rhuMkS17qaC500vEy Yr6AcUvv9y7hyPLddz+AM1gbqq0dIAWysLLTPmumXm+qxccVijagoVmeg1VcNc+YJgvN d5uQ== X-Gm-Message-State: AKS2vOx5AjqzM30RAHtHyVTBLNZkBLmSTHLoz6uSLssUk0Kgo7Sx/vC6 0KvuG+SVhP11FbrRBMOh/J6A1ZSDYA== X-Received: by 10.98.158.139 with SMTP id f11mr10468379pfk.208.1498652530571; Wed, 28 Jun 2017 05:22:10 -0700 (PDT) MIME-Version: 1.0 Received: by 10.100.181.209 with HTTP; Wed, 28 Jun 2017 05:22:10 -0700 (PDT) From: Urs Schreiber Date: Wed, 28 Jun 2017 14:22:10 +0200 Message-ID: Subject: differential geometry in modal HoTT To: homotopytypetheory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Felix Wellen just handed in a PhD thesis that some readers here might find of interest, on the formalization of higher synthetic differential geometry in HoTT: Felix Wellen, "Formalizing Cartan Geometry in Modal Homotopy Type Theory" PhD Thesis, KIT 2017 thesis pdf: http://www.math.kit.edu/iag3/~wellen/media/diss.pdf, talk slides: https://ncatlab.org/schreiber/files/wellenDGinHoTT.pdf HoTT-Agda code: https://github.com/felixwellen/DCHoTT-Agda background links: https://ncatlab.org/schreiber/print/thesis+Wellen The thesis implements a fragment of the axioms of differential cohesion for synthetic differential geometry, formalized in homotopy type theory and implemented in the Agda. Specifically, a modal operator is introduced which is interpreted as an =E2=80=9Cinfinitesimal shape=E2=80=9D modality =E2=84=91. For X a homotopy type the standard inter= pretation of the type =E2=84=91X is the result of =E2=80=9Cidentifying infinitesimall= y close points in X=E2=80=9D. (By synthetic PDE theory the dependent types over =E2=84=91X have the interpretation of being partial differential equations with free variables ranging in X. The linear depenent types over =E2=84=91X are also known as D-modules, as used in geometric representation theory.) Using this infinitesimal shape modality =E2=84=91 the thesis presents a formalization of the concept of manifold in the type theory. Via the homotopy theoretic interpretation of the type theory the interpretation of such =E2=80=9Cmanifold types=E2=80=9D is really as =C3=A9= tale =E2=88=9E-stacks X. The main theorem shows that the infinitesimal disk bundle of any such manifold X is a fiber =E2=88=9E-bundle which is associated to an principal =E2=88=9E-bundle: its frame bundle. Classically, the concept of frame bundle is the foundation of all genuine geometry, via Cartan geometry: Equipping the frame bundle of a manifold X with torsion-free G-structure means to equip X with a flavor of geometry, depending on the choice of G, such as, (pseudo-)Riemannian geometry, conformal geometry, complex geometry, symplectic geometry etc. pp. The moduli stacks of all given G-structures on a given manifold are of central interest in the classical theory, such as the moduli stacks of complex structures, or the moduli stacks of conformal structures. In order to lift classical Cartan geometry from classical manifolds to higher Cartan geometry on =C3=A9tale =E2=88=9E-stacks, the thesis closes by formalizing the concept of torsion-free G-structure on manifold types. Due to the homotopy-theoretic interpretation this is really a formalization of higher (=E2=88=9E-group) G-structures on =C3=A9tale =E2=88= =9E-stacks, including also examples such as string structures or Fivebrane structures. Finally the thesis demonstrates the construction of the (higher) moduli stacks of such torsion-free G-structures This solves the first of the three problems in modal type theory that had been posed in U.S.: "Some thoughts on the future of modal homotopy type theory", talk at Homotopy Type Theory and Univalent Foundations - Mini-Symposium, within the German Mathematical Society meeting Sept 2015, Hamburg https://ncatlab.org/schreiber/files/SchreiberDMV2015b.pdf For more exposition see also here: https://ncatlab.org/schreiber/print/Formalizing+Cartan+Geometry+in+Modal+Ho= TT Best wishes, urs