A cartesian closed category in Martin-Löf's intuitionistic type theory
scientific article; zbMATH DE number 1857112