El Prólogo de Conjuntos en Matemáticas (segunda sección, titulada " la Organización) contiene el siguiente comentario, acerca de las diferencias entre ETCS y otros fundamentos de las matemáticas:
Cada mapa de las necesidades de un dominio explícita y explícito codominio (no sólo un dominio, como en las anteriores formulaciones de la teoría de conjuntos, y no sólo un codominio, como en el tipo de teoría).
Entiendo que el comentario acerca de la teoría de conjuntos: una función como un conjunto de pares ordenados determina su dominio, pero no de su codominio.
Pero, ¿qué hacen los autores quieren decir cuando dicen una función en el tipo de la teoría tiene una explícita codominio pero no explícito de dominio?
Un término de la simple tipo $A \rightarrow B$ tiene una explícita de dominio y codominio. Un plazo de un dependiente del tipo de $\Pi x:A.B(x)$ podría decirse que tiene un dominio explícita, pero no un codominio (desde su codominio tendría que ser algo como $\bigcup x:A.B(x)$, que no existe como un tipo de Martin-Löf Tipo de Teoría).
