pozorvlak:Can you please explain the section "Categorical Models of Type Theory" in the wikipedia entry on Intuitionistic Type Theory?
I understand (most) of the words on their own, but the sentences seem to just stop making sense to me as I read it.