[darzu]

Here I think IT more likely means Intuitionistic Type Theory.