Type-theoretic model category

https://ncatlab.org/nlab/show/type-theoretic+model+category

Page citée sur celle ci :

https://ncatlab.org/nlab/show/identity+type

Advertisements
Posted in category theory, Higher category theory, homotopy type theory | Tagged | Leave a comment

Premier contact (2016) : les humains, comme les toxicomanes chez Ernst Junger portent La Croix du temps!

Henosophia Léon BRUNSCHVICG et la philosophie Μαθεσις Universalis

le film peut être vu ici en vf :

https://m.ok.ru/video/216015440503

Cet article de l’an dernier à son sujet:

https://anthroposophiephilosophieetscience.wordpress.com/2016/12/16/premier-contact-arrival-2016-excellent-et-important/

En fait ce que les extraterrestres apportent à l’humanité par l’intermédiaire de leur langage à base de glyphes sur le modèle des anciens hiéroglyphes égyptiens , c’est une compréhension nouvelle, non linéaire, du temps « dont nous sommes tellement  esclaves » comme Louise le note au début du film.

ceci rappelle le propos de Léon Brunschvicg :

https://leonbrunschvicg.wordpress.com/quelques-citations-eparses-de-brunschvicg-particulierement-eclairantes-voire-illuminatrices/

« Nous nous affranchirons du temps simplement vital, dans la mesure où nous en découvrirons la racine intemporelle. La vie, nous savons trop qu’elle est sans pitié pour les vivants. Elle peut se définir comme l’ensemble des forces qui résistent à la mort….. jusqu’à l’inévitable dénouement qui la révèle comme l’ensemble des forces qui acheminent à la mort…..

…il est malaisé de décider si l’armée des vivants peut avoir l’espérance, suivant la magnifique image…

View original post 660 more words

Posted in Cinéma, Cochet-Brunschvicg, Léon Brunschvicg, Ouvert : dualité plan vital-plan spirituel, Philosophie, Physique, Science, mathesis, Science-internelle | Leave a comment

Impredicative Encodings of Inductive Types in HoTT

Homotopy Type Theory

I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here.

Known impredicative encodings of various inductive types in System F, such as the type

$latex forall X. (Xrightarrow X) rightarrow X rightarrow X,$

of natural numbers do not satisfy the relevant $latex eta$-computation rules. The aim of this work is to refine the System F encodings by moving to a system of HoTT with an impredicative universe, so that the relevant $latex eta$-rules are satisfied (along with all the other rules). As a result, the so-determined types have their expected universal properties. The main result is the construction of a type of natural numbers which is the initial algebra for the expected endofunctor $latex Xmapsto X+mathbf{1}$.

For the inductive types treated in the thesis, we do not use the full power of HoTT; we need only postulate $latex Sigma$-types…

View original post 833 more words

Posted in Philosophie | Leave a comment

#HoTT The Book : 1.11 propositions as types

The HoTT Book

https://hott.github.io/book/nightly/hott-online-1075-g3c53219.pdf

Je passe sur ce qui n’est pas essentiel pour aller plus vite car il faut accélérer pour en arriver aux choses sérieuses qui commencent au chapitre 2.

Passons donc Page 41 au 1.11:

Les termes ou éléments d’un type comme proposition sont conçus comme des « évidences », des « témoins » de la vérité de cette proposition.

Ainsi les propositions sont des types particuliers, dont les éléments sont des preuves.

Dans le système de Bolzano:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/08/bolzano-une-theorie-des-idees/

Les propositions sont de nature lectologique comme les autres idées : elles n’existent pas dans le monde comme les étants, objets ou qualités.

Ce sont des idées qui réfèrent à leur valeur de vérité , 1 si elles sont vraies et 0 si elles sont fausses.

Le tableau en deux colonnes page 41 donne la correspondance entre les opérations logiques sur des propositions en langue naturelle et les opérations de la théorie des types.

Ainsi Vrai correspond à 1, faux à 0, «  et » au produit de deux types, « ou «  à la somme, «  si » à A → B, « non » à A → 0

La logique de la théorie des types est constructive ce qui veut dire qu’elle se limite à des constructions qui peuvent être effectivement menées à bout. Des principes comme le tiers exclus’ ou les démonstrations par l’absurde n’y sont pas valides .
Le caractère constructif signifie aussi que les procédures ont un intérêt calculatoire intrinsèque, ce qui intéresse les «  computer scientists »

Page 44 le tableau à deux colonnes de la page 41 se poursuit au delà de la logique propositionnelle, par la logique des prédicats, qui fait intervenir des quantificateurs.

Ainsi une assertion : » pour tout x: A on a P(x) » correspond en théorie des types à :

Πx:A P(x)

Tandis qu’une assertion d’existence «  il existe un x:A tel que P(x) » correspond à :

Σx:AP(x)

À voir aussi:

https://gciruelos.com/propositions-as-types.html

http://math.andrej.com/2004/05/04/propositions-as-types/

http://math.andrej.com/data/bracket_types.pdf

Constructive Validity

https://golem.ph.utexas.edu/category/2012/01/propositions_as_some_types_and.html

https://ncatlab.org/nlab/show/propositions+as+types

Posted in homotopy type theory | Leave a comment

Thèse : towards an (∞,2)-category of coherent monads in an ∞-cosmos

https://infoscience.epfl.ch/record/231037/files/EPFL_TH7748.pdf

Posted in ∞-catégories, ∞-cosmoi, ∞-topoi | Tagged , , | Leave a comment

Fibration categories and Type theory

http://www.lorentzcenter.nl/lc/web/2011/467/presentations/Presentation%20C%20Kapulkin.pdf

Posted in Homotopy, homotopy type theory | Leave a comment

Categories types and structures

https://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf

Posted in ∞-catégories, category theory, Higher category theory, homotopy type theory, Philosophie mathématique, Science, mathesis | Tagged | Leave a comment