Category Archives: Type theory

Relations entre #HoTT et la théorie des catégories : page du Nlab

Cette page plus générale porte sur les liens entre la théorie des types et la théorie des catégories : https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory Il s’agit d’un exemple de dualité entre syntaxe et sémantique : https://ncatlab.org/nlab/show/syntax-semantics+duality la théorie des catégories  pouvant être considérée comme … Continue reading

Posted in Science, mathesis, category theory, Higher category theory, Science-internelle, homotopy type theory, Type theory, HTTUF

Hegel : science de la logique dans ncatlab

Ici : https://ncatlab.org/nlab/show/Science+of+Logic#Phen760 « Hence we formalize Wesen by ∞-topos «  un cadre mathématique pour la doctrine hégélienne de l’Essence (Wesen) est choisi dans #HoTT et #HigherToposTheory : »In (homotopy) type theory the appearance of a reflection of the type system in itself is a type universe Type∈H here) see … Continue reading

Posted in ∞-catégories, ∞-cosmoi, ∞-topoi, category theory, Hegel, Higher category theory, Higher topos theory, homotopy type theory, opposition monde véritable-monde imaginaire, Philosophie, Science, mathesis, Science-internelle, Théorie des topoi (topos theory), Type theory

Categorical structures for Type theory in univalent foundations

https://hal.inria.fr/hal-01579271/document

Posted in category theory, EHTT, Higher category theory, homotopy type theory, Type theory

Internal type theory

http://www.cse.chalmers.se/~coquand/int.html https://pdfs.semanticscholar.org/eb9b/b4767cd3c226b7cb96b434980a0d6ed644b6.pdf

Posted in Type theory