↓が起源らしい。 Nicolaas G. de Bruijn, Telescopic mappings in typed lambda calculus, Information and Computation 91 (1991), no. 2, 189–204. https://www.win.tue.nl/automath/archive/pdf/aut103.pdf RICHARD GARNER "TWO-DIMENSIONAL MODELS OF TY…