[Aldor-l] [open-axiom-devel] [#428] 'Domain' in 'SetCategory'?

[Jacques Carette]

root wrote:
> I think part of the struggle is the attempt to unify the ideas of
> type theory with the ideas of category theory. Being able to do so
> would be deeply interesting but I don't think there is a "correct"
> way to do it in any theoretical sense. 
Sure there is - read Bart Jacobs's book "Categorical Logic and Type 
Theory".

Jacques