nLab Initiality Project - Raw Syntax - Pi-types

operatorsortvarstype argsterm argsscopingsugared syntax
Π\PitytyxxAA, BBBxB\lhd xΠ(x:A).B\Pi(x:A).B
λ\lambdatmtmxxAA, BBMMBxB\lhd x, MxM\lhd xλ(x:A.B).M\lambda(x:A.B).M
AppApptmtmxxAA, BBMM, NNBxB\lhd xApp (x:A).B(M,N)App^{(x:A).B}(M,N)

Last revised on November 10, 2018 at 01:23:01. See the history of this page for a list of all contributions to it.