Archives quotidiennes :

Categories, What’s the Point?

Math ∩ Programming

Perhaps primarily due to the prominence of monads in the Haskell programming language, programmers are often curious about category theory. Proponents of Haskell and other functional languages can put category-theoretic concepts on a pedestal or in a mexican restaurant, and their benefits can seem as mysterious as they are magical. For instance, the most common use of a monad in Haskell is to simulate the mutation of immutable data. Others include suspending and backtracking computations, and even untying tangled rope.

Category theory is often mocked (or praised) as the be-all and end-all of mathematical abstraction, and as such (and for other reasons I’ve explored on this blog) many have found it difficult to digest and impossible to master. However, in truth category theory arose from a need for organizing mathematical ideas based on their shared structure. In this post, I want to give a brief overview of what purpose…

Voir l’article original 1 609 mots de plus

#HoTT André Joyal : la notion de typos

Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA ενοσοφια μαθεσις

Voir cet ancien article :⊓-tribus/

et la note de Joyal :

Page 15 sur 52 définition du «  push forward functor » associé à une flèche f : A ? B dans une catégorie C

Le foncteur est noté f!

Et il est dirigé de la slice category C/A vers C/B ( c’est à dire les catégories dont les objets sont les morphismes de C ayant pour cible A ou B)

selon la formule :

f!( X,p) = (X, fp)

( voir le carré Page 15)

Page 17:

Ce foncteur f! a un foncteur adjoint à droite :

f*: C/B ? C/A

Tout ceci étant associé rappelons le à un morphisme f: A ? B dans la catégorie C. Ce foncteur est appelé foncteur changement de base (« base change ») et (voir le diagramme page 17) il envoie un morphisme p sur un morphisme…

Voir l’article original 653 mots de plus