nLab Initiality Project - Type Theory - Pi-types

ΓAtypeΓ,x:ABtypeΓΠ(x:A).Btype ΓAtypeΓ,x:ABtypeΓMΠ(x:A).BΓNAΓApp x:A.B(M,N)B[N/x] ΓAtypeΓ,x:ABtypeΓ,x:AMBΓλ(x:A.B).MΠ(x:A).B ΓAAtypeΓ,x:ABBtypeΓApp x:A.B(λ(x:A.B).M,N)M[N/x]:B[N/x] Γ,y:AApp x:A.B(M,y)App x:A.B(M,y):B[y/x]ΓMM:Π(x:A).B ΓAAtypeΓ,x:ABBtypeΓΠ(x:A)BΠ(x:A)Btype ΓAAtypeΓ,x:ABBtypeΓ,x:AMM:BΓλ(x:A.B).Mλ(x:A.B).M:Π(x:A).B ΓAAtypeΓ,x:ABBtypeΓMM:Π(x:A)BΓNN:AΓApp x:A.B(M,N)App x:A.B(M,N):B[N/x] \begin{gathered} \frac{\Gamma \vdash A \, type \qquad \Gamma, x:A \vdash B\,type}{\Gamma \vdash \Pi(x:A) .B \, type} \\ \\ \frac{\Gamma \vdash A \, type \qquad \Gamma, x:A \vdash B\,type \qquad \Gamma \vdash M \Leftarrow \Pi(x:A). B \qquad \Gamma \vdash N \Leftarrow A}{\Gamma \vdash App^{x:A.B}(M,N) \Rightarrow B[N/x]} \\ \\ \frac{\Gamma \vdash A \, type \qquad \Gamma,x:A \vdash B \,type \qquad \Gamma,x:A \vdash M \Leftarrow B}{\Gamma \vdash \lambda(x:A.B).M \Rightarrow \Pi(x:A). B} \\ \\ \frac{\Gamma\vdash A \equiv A' \, type \qquad \Gamma, x:A \vdash B \equiv B' \, type}{\Gamma \vdash App^{x:A.B}(\lambda(x:A'.B').M,N) \equiv M[N/x] : B[N/x]} \\ \\ \frac{\Gamma, y:A \vdash App^{x:A.B}(M,y) \equiv App^{x:A.B}(M',y) : B[y/x]}{\Gamma \vdash M \equiv M' : \Pi(x:A).B } \\ \\ \frac{\Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type}{\Gamma \vdash \Pi(x:A)B \equiv \Pi(x:A')B' type} \\ \\ \frac{ \Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type \qquad \Gamma, x:A \vdash M \equiv M' : B } {\Gamma \vdash \lambda(x:A.B).M \equiv \lambda(x:A'.B').M' : \Pi(x:A).B} \\ \\ \frac{ \Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type \qquad \Gamma \vdash M \equiv M' : \Pi(x:A)B \qquad \Gamma \vdash N \equiv N' : A } {\Gamma \vdash App^{x:A.B}(M, N) \equiv App^{x:A'.B'}(M', N') : B[N/x]} \end{gathered}

Last revised on November 29, 2018 at 17:25:46. See the history of this page for a list of all contributions to it.