He encontrado las notas de las que habla. La idea de un escribiendo es que te gusta expresar qué tipo de cosa es algo. Por ejemplo si en un texto de matemáticas alguien introduce una nueva variable n en una prueba, entonces también le dirán qué tipo de objeto n representa. Por ejemplo, dicen sea n un número natural o sea n un número entero . En el primer caso, la tipificación de $n$ es por ejemplo $n:\mathbb N$ . Las personas que están más en la teoría de conjuntos probablemente querrán escribir $n\in \mathbb N$ pero hay una gran diferencia entre ambos. Un tipo de algo es siempre la respuesta a la pregunta "¿Qué es?". Por ejemplo, alguien podría escribir el símbolo $f$ se preguntará: "¿Qué es $f$ ?" y te dirán "Bueno, $f$ es un morfismo de $A$ a $B$ en esa categoría $\mathbb C$ de la que hablábamos". De ahí que el tipo de $f$ en ese caso es "morfismo de $A$ a $B$ "y a los teóricos de la tipografía les gusta denotar esto por $f:A\to B$ . Esto explica la terminología en su pdf. Realmente no tiene mucho contenido, excepto quizás si quieres formalizar la teoría de categorías en un asistente de pruebas y necesitas decidir si quieres usar tipos dependientes para los morfismos o lo que sea.La única información que te dice la tipificación es qué son el codominio y el dominio de un morfismo.
Hay algunas sutilezas. Ignore el siguiente párrafo si le confunde. El pensamiento de muchos matemáticos está influido por teorías de conjuntos materiales como ZFC. El sistema formal de ZFC es de orden simple. Sólo hay tipos: todo es un conjunto. En lugar de $n:\mathbb N$ a la gente de teoría de conjuntos le gustaría escribir $n\in \mathbb N$ pero hay una diferencia importante entre ambos. La expresión $n\in \mathbb N$ es una afirmación que se puede probar o refutar. Es algo que puede ser falso o verdadero. En cambio, la información que $n$ es un conjunto no es algo que se pueda probar o refutar. (undrr la ssunción de que estás trabajando en ZFC en este momento). Es algo que la persona tiene que decirte cuando escribe el símbolo, de lo contrario está diciendo tonterías. Escribir declaraciones $n:\mathbb N$ no son algo que se pueda refutar o probar dos. Son sólo información adicional que hay que facilitar cuando se escribe el símbolo. Si quieres aprender más sobre esta diferencia, el mejor escenario para observarla es la diferencia entre la lógica formal de primer orden orden múltiple y la lógica formal de primer orden simple.
