From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 1 Mar 2018 08:22:33 -0800 (PST) From: Victor Porton To: Homotopy Type Theory Message-Id: <1f0cc7d4-23d4-4458-bf0b-428a5cc8dd39@googlegroups.com> Subject: Another variation on the topic of homotopy MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2546_1806093901.1519921353323" ------=_Part_2546_1806093901.1519921353323 Content-Type: multipart/alternative; boundary="----=_Part_2547_1746019708.1519921353324" ------=_Part_2547_1746019708.1519921353324 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I have the following (very preliminary) idea: Replace =E2=80=9Cpath=E2=80=9D in the definition of homotopy with =E2=80=9C= monovalued funcoid with=20 domain [0;1]=E2=80=9D. It enables things like infinitely short paths. (Cons= ider=20 such things as a plane without a point and an infinitely short path around= =20 this point, yet to be formulated precisely.) This "generalized path" is a= =20 mapping from [0;1] to ultrafilters (with certain restriction these=20 ultrafilters conform to). This way we may get another HoTT possibly not equivalent to the =E2=80=9Cma= in=E2=80=9D=20 HoTT. Moreover, we may probably construct several non-equivalent theories= =20 (needs careful consideration). I have not yet formulated this precisely, but call you as soon as the rough= =20 idea appeared, so that you become able for example learn my theory of=20 funcoids and start to ponder about my idea. I am going to write again when= =20 this will be formulated exactly. But you are free to join my research and= =20 race with me who will first have enough time to formulate this in details. This idea uses theory of funcoids=20 (discovered= =20 by me). By the way, please consider to nominate me for Breakthrough Prize= =20 for discovery (and thorough research) of the concept of funcoid. I need=20 money. (Not three millions, I would probably donate two of them to some=20 charity.) Disclaimer: I am in no way an expert in homotopy and HoTT. But this my idea= =20 is probably great. ------=_Part_2547_1746019708.1519921353324 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable

I have= the following (very preliminary) idea:


Replace =E2=80=9Cp= ath=E2=80=9D in the definition of homotopy with =E2=80=9Cmonovalued funcoid= with domain [0;1]=E2=80=9D. It enables things like infinitely short paths.= (Consider such things as a plane without a point and an infinitely short p= ath around this point, yet to be formulated precisely.) This "generali= zed path" is a mapping from [0;1] to ultrafilters (with certain restri= ction these ultrafilters conform to).


This way we may get = another HoTT possibly not equivalent to the =E2=80=9Cmain=E2=80=9D HoTT. Mo= reover, we may probably construct several non-equivalent theories (needs ca= reful consideration).


I have not yet formulated this= precisely, but call you as soon as the rough idea appeared, so that you be= come able for example learn my theory of funcoids and start to ponder about= my idea. I am going to write again when this will be formulated exactly. B= ut you are free to join my research and race with me who will first have en= ough time to formulate this in details.


This idea uses=C2=A0theory of funcoids=C2=A0(discovered = by me). By the way, please consider to nominate me for Breakthrough Prize f= or discovery (and thorough research) of the concept of funcoid. I need mone= y. (Not three millions, I would probably donate two of them to some charity= .)


Disclaimer: I am in no way an expert in homotopy an= d HoTT. But this my idea is probably great.

------=_Part_2547_1746019708.1519921353324-- ------=_Part_2546_1806093901.1519921353323--