↓が起源らしい。
- 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 TYPE THEORY" に書いてあった。
