André Joyal #HoTT : simplicial tribes

« Introduction to simplicial homotopy theory »:

http://hopf.math.purdue.edu/Joyal-Tierney/JT-chap-01.pdf

La définition des tribus simpliciales figure dans cette note :

http://logica.dmi.unisa.it/tacl/wp-content/uploads/2014/08/Joyal-TACL2015.pdf

« Category theory and HoTT »

Page 38 : une tribu simpliciale est une catégorie enrichie sur les ensembles simpliciaux ayant en plus une structure de tribu (avec les conditions de compatibilité)

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/06/t-streicher-a-model-of-type-theory-in-simplicial-sets-a-brief-introduction-to-voevodskys-hott/

Les ensembles simpliciaux (simplicial sets ) forment une catégorie Sset qui est un topos

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/05/highertopostheory-15-fibrations-densembles-simpliciaux/

Dans une catégorie enrichie sur Sset les morphismes entre deux objets ne forment pas un ensemble, un objet de Set, mais un objet de Sset. Sset est Le topos classifiant (classifying topos ) de la théorie des intervalles:

https://ncatlab.org/nlab/show/simplicial+set

Page 35 sont définies les catégoriesde fibration au sens de Brown: il s’agit d’une catégorie munie d’une classe de morphismes appelés « flèches acycliques » dont les propriétés sont indiquées page 35; chaque tribu est une telle catégorie, en prenant pour flèches acycliques les équivalences homotopiques.

Les tribus simpliciale forment une catégorie, qui a une structure de « Brown fibration category » ( théorème page 38 en relation avec le travail de Szumilo cf

http://logica.dmi.unisa.it/tacl/wp-content/uploads/abstracts/invited_paper_7.pdf )

Travail de Szumilo qui est résumé dans l’introduction à cet article écrit avec Kapulkin:

https://arxiv.org/pdf/1709.09519.pdf

Advertisements
Posted in ∞-catégories, category theory, Higher category theory, Higher topos theory, homotopy type theory, Science-internelle | Leave a comment

Dan Licata , Robert Harper :programming in #HoTT

http://dlicata.web.wesleyan.edu/pubs/lh122tttalks/lh12wg2.8.pdf

Posted in homotopy type theory | Leave a comment

Homotopy theories and model categories

Posted in Philosophie | Leave a comment

Correspondance entre Alexandre Grothendieck et Ronald Brown

https://webusers.imj-prg.fr/~georges.maltsiniotis/ps/agrb_web.pdf

Posted in Grothendieck, Philosophie mathématique, Science, mathesis | Leave a comment

Otto Preminger : « Laura » 1944

En anglais vo:

https://m.ok.ru/dk?st.cmd=movieLayer&st.discId=269918407331&st.retLoc=default&st.discType=MOVIE&st.mvId=269918407331&st.stpos=rec_1&_prevCmd=movieLayer&tkn=6767#lst#

J’ai vu le film fin 1967 au cinéma « Studio de l’Etoile » tout près derrière l’Arc de Triomphe, j’allais avoir quinze ans…

C’est un film fascinant à cause de sa tonalité « orphique » , sensible dans le scénario et la musique obsédante composée par David Raksin à l’époque , Raksin a aussi créé les musiques des films de Minnelli « les ensorcelés »(The bad and The beautiful) en 1952:

https://anthroposophiephilosophieetscience.wordpress.com/2016/08/31/vincente-minnelli-the-bad-and-the-beautiful-les-ensorceles-1952/

Et « Quinze jours ailleurs » (Two weeks in another town) en 1962

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/06/vincent-est-minnelli-two-weeks-in-another-town-1962-vo/

Pour Laura en 1944 Raksin n’y arrivait pas, il avait pris beaucoup de retard et devait absolument fournir la musique pour le lundi. le samedi matin il reçut la lettre d’un avocat l’informant que sa femme demandait le divorce. Or Raksin était , ceci explique peut être cela, follement amoureux de sa femme (cela arrive, même à Hollywood, tous les hommes ne sont pas des « libertins » assoifés de conquêtes ou de putes ) . Il passa ce week-end dans le désespoir et la désolation mais ne but pas une goutte d’alcool et ne se suicida pas. Le dimanche soir, il se mit au piano et composa en une heure, comme en se jouant, la musique douce et triste de Laura.

Laura Hunt (Gene Tierney) a été tuée chez elle d’un coup de fusil qui l’a défigurée , l’assassin a pris la fuite et n’a pas été retrouvé. L’inspecteur Mark McPherson (Dana Andreas) est chargé de l’enquête et tombe sous le charme de la morte en regardant son portrait. Le Lundi soir, par une forte pluie, il se rend dans l’appartement pour poursuivre son enquête, fouille les armoires, puis, désespéré, boit copieusement le whisky qu’il trouve dans le bar avant de s’endormir dans le fauteuil face au portrait. Et tard le soir la clef tourne dans la serrure et Laura fait son apparition devant le policier qui se réveille du sommeil de l’ivresse. Rien de surnaturel là dedans : la jeune femme était partie pour sa maison de campagne le vendredi soir, y a passé tout le week end dont le lundi férié sans écouter les actualités et ce n’est pas elle qui a été tuée mais Diane Redfern, une modèle de sa boîte qui y était en tête à tête amoureux avec Shelby Carpenter (Vincent Price) l’amoureux de Laura qu’elle devait, peut être, épouser. Diane Redfern, défigurée par le coup de fusil, a été prise pour Laura (sauf par Carpenter qui connaît bien l’identité de la victime, mais ne dit rien car il croit que Laura est l’assassin). L’histoire continue jusqu’au dénouement, où nous apprenons l’identité du tueur et ses motifs…
Donc un scénario orphique , car dans les premières minutes nous ne savons rien du déroulement des faits et croyons tous que Laura a été tuée . Selon Waldo Lydecker (Clifton Webb, remarquable) le peintre Jacoby qui a réalisé le portrait de Laura était amoureux d’elle mais a été incapable de rendre sa beauté et son charme (« vibrance ») . Nous avons donc l’opposition entre une femme en chair et en os, une femme mortelle et. Que tout le monde croit morte, et son portrait , comme dans « La femme et le portrait » réalisé la même année 1944 par Fritz Lang , ou dans le « Chef d’oeuvre Inconnu » de Balzac

https://anthroposophiephilosophieetscience.wordpress.com/2016/07/03/il-y-a-une-femme-la-dessous-secria-porbus/

« Le vieux lansquenet se joue de nous, dit Poussin en revenant devant le prétendu tableau. Je ne vois là que des couleurs confusément amassées et contenues par une multitude de lignes bizarres qui forment une muraille de peinture.

— Nous nous trompons, voyez ?… reprit Porbus.

En s’approchant, ils aperçurent dans un coin de la toile le bout d’un pied nu qui sortait de ce chaos de couleurs, de tous, de nuances indécises, espèce de brouillard sans forme ; mais un pied délicieux, un pied vivant ! Ils restèrent pétrifiés d’admiration devant ce fragment échappé à une incroyable, à une lente et progressive destruction. Ce pied apparaissait là comme un torse de quelque Vénus en marbre de Paros qui surgirait parmi les décombres d’une ville incendiée.

Il y a une femme là-dessous

, s’écria Porbus en faisant remarquer à Poussin les couches de couleurs que le vieux peintre avait successivement superposées en croyant perfectionner sa peinture.

Les deux peintres se tournèrent spontanément vers Frenhofer, en commençant à s’expliquer, mais vaguement, l’extase dans laquelle il vivait. »

C’est le thème , possiblement platonicien, du rapport de l’image , de la peinture au modèle « réel » , qui est l’objet de toutes ces histoires, très différentes. C’est aussi, si l’on veut, le thème philosophique de ce blog, qui est loin d’être une œuvre d’art, mais l’Idée n’a pas pour fonction ici de se calquer sur une réalité vivante qu’elle reproduirait : l’Idée qui n’est pas est supérieure à la « réalité » qui est . L’Idée n’est pas une représentation du monde sous la forme d’une œuvre d’art , mais une forme mathématique qui n’est pas censée décrire le monde, mais créer « ce qui est plus que le monde fini qui est » : le monde spirituel Infini qui n’est pas.

Plutôt que « Le chef d’oeuvre Inconnu «  c’est « Louis Lambert », la plus grande œuvre de Balzac, qu’il faut ici évoquer

https://balzacabsolu.files.wordpress.com/2015/12/science-totale.pdf

https://www.cairn.info/revue-le-telemaque-2004-2-page-111.htm

Mais nous nous éloignons du film d’Otto Preminger ; le portrait de Laura eut tout aussi bien être détruit que la femme vivante peut être tuée , l’image et l’oeuvre est une réalité du monde elle aussi , et n’est donc pas une Idée platonicienne . Peut on imaginer sur l’appartement et le portrait qu’il abrite soient restés à l’écart de la vie historique, disons pendant prés de 60 ans jusqu’au 11 septembre 2001 , année où la désolation et la mort se sont abattues sur New York. On le peut oui, on a tous les droits avec les rêveries sur une œuvre , qui se situent par définition à l’écart du monde et de sa réalité folle. Tout ceci pour dire que la fascination qu’exerce le film, qui est réelle, est plutôt de l’ordre du mythe que du factuel. Et il n’est donc pas étonnant que l’alcool y joue l’un role important ,et psychromètre, faisant remonter les âmes et les spectres des enfers où Cerbère n’a pas accompli correctement sa mission. Mais je m’égare… et pourtant John Barleycorn (C2H5OH) est loin de moi comme il l’était en cet heureux temps d’innocence de la fin de 1967 : c’était 23 ans après la sortie du film, les hordes barbares de Mai 68 envahiraient les rues 6 mois plus tard. Puisse t’il le rester (loin de moi) jusqu’à ma mort !

La version en vo rend mieux les sonorités de 1967 (telles qu’elles subsistent dans mon souvenir), aussi a t’elle ma faveur. Cependant il existe aussi une version en vf:

https://m.ok.ru/dk?st.cmd=movieLayer&st.discId=80956688930&st.retLoc=default&st.discType=MOVIE&st.mvId=80956688930&st.stpos=rec_8&_prevCmd=movieLayer&tkn=8397&__dp=y

https://m.ok.ru/dk?st.cmd=movieLayer&st.discId=83221219910&st.retLoc=default&st.discType=MOVIE&st.mvId=83221219910&st.stpos=rec_1&_prevCmd=movieLayer&tkn=9398

Posted in Cinéma | Leave a comment

Différentes notes d’André Joyal sur la description catégorique de #HoTT

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/12/andre-joyal-hott-category-theory-and-homotopy-type-theory/

Les deux travaux qui suivent portant sur la notion de tribu:

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

http://www.crm.cat/en/Activities/Documents/joyal-crm-2013.pdf

L’état le plus récent de ces travaux est « Notes on tribes and clans »:

https://arxiv.org/abs/1710.10238

Voir les articles de ce blog:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/28/hott-andre-joyal-tribus-et-clans/

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/15/hott-relation-des-tribes-et-des-comprehension-categories/

Les tribus (tribes) sont le cadre catégorique pour la théorie homotopique des types; les différentes notes d’André Joyal se ressemblent mais avec des différences subtiles :

Celle ci « A categorical description of HoTT » aborde (Page 56)la notion de typos qui est une tribu qui est à la fois une h-tribu et une π-tribu, donc selon la terminologie de Joyal une πh-tribu obéissant à une condition supplémentaire:(Page 56 sur 75)

http://www.crm.cat/en/Activities/Documents/joyal-crm-2013.pdf

Voir aussi

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/22/hott-andre-joyal-la-notion-de-typos/

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/14/andre-joyal-hott-tribus-et-⊓-tribus/

https://anthroposophiephilosophieetscience.wordpress.com/2018/01/09/hott-andre-joyal-π-tribus-et-h-tribus-tribus-de-martin-lof-et-de-voevodsky/

Les deux grandes espèces de tribus, les π-tribus et les h-tribus, sont réunifiées sous la notion de πh-tribu, qui donne ensuite par des propriétés supplémentaires, les tribus de Martin-Lof et les tribus de Voevodsky , dont Joyal donne des exemples précis.

L’autre note d’André Joyal, très précieuse aussi est la suivante, qui est utilisée dans les articles ci dessus:

https://ncatlab.org/homotopytypetheory/files/Joyal.pdf

Page 17 : ce qui est appelé un type dépendant (dependent type) de contexte x: A et noté dans HoTT:

x:A ⊢ E(x): Type

Est en théorie des catégories un objet d’une tribu locale (voir Page 17 sur 81)

Cette note de Joyal aborde (ce que ne fait pas l’autre) en page 29 sur 81, la notion catégorique d’espace de sections pour un objet (E, p) dans une « slice category » C/A

https://math.stackexchange.com/questions/371705/in-a-slice-category-c-a-of-a-category-c-over-a-given-object-a-what-is-the-role

Page 25 sur 81 l’espace total :

E= ∑x:A E(x)

Correspondant à un ∑-Type , est mis en relation avec un foncteur d’oubli « opération de sommation » ce qui donne sur la même page 25 la règle de ∑-formation d’un ∑-Type, correspondance entre HoTT et catégories qui sera explicitée dans l’article suivant.

Parmi les documents fondateurs cités par André Joyal on note « Tripos theory » de Hyland, Johnstone et Pitts:

https://www.dpmms.cam.ac.uk/~martin/Research/Pub71-80/hjp80.pdf

Posted in homotopy type theory | Leave a comment

Combinatorial Species and Finite Sets in HoTT

Homotopy Type Theory

(Post by Brent Yorgey)

My dissertation was on the topic of combinatorial species, and specifically on the idea of using species as a foundation for thinking about generalized notions of algebraic data types. (Species are sort of dual to containers; I think both have intereseting and complementary things to offer in this space.) I didn’t really end up getting very far into practicalities, instead getting sucked into a bunch of more foundational issues.

To use species as a basis for computational things, I wanted to first “port” the definition from traditional, set-theory-based, classical mathematics into a constructive type theory. HoTT came along at just the right time, and seems to provide exactly the right framework for thinking about a constructive encoding of combinatorial species.

For those who are familiar with HoTT, this post will contain nothing all that new. But I hope it can serve as a nice…

View original post 1,485 more words

Posted in Philosophie | Leave a comment