Tremendo gracias, me sirvió sí. Y estuve leyendo otras cosas en internet a ver si sacaba alguna intuición. Y me siento un poco más cómodo con el tema o al menos cómodo con mi falta de conocimiento, jaja. Cuando veamos Prop en el curso veré mejor.
Olvidándonos del tema de Prop, igual me resulta muy raro por ejemplo que tengamos < Type_i, Set, Set > en lugar de < Type_i, Set, Type_i >. Sobre todo pensando en analogía con teoría de conjuntos.
Gracias, nos vemos el martes. Saludos. :D