No label defined (Q4487253)

Several generalised type theories allow quantified types \(\forall X.\sigma\), where \(X\) is a type variable. If a term \(M\) has type \(\forall X.\sigma\) \((M:\forall X.\sigma)\), \(M\) can be interpreted as the proof of the quantified formula \(\forall X.\sigma\). If \(M:\forall X.\sigma\) it follows that for any type \(\rho\), \(M\rho:[\rho/X]\sigma\). The author wants to reverse this last procedure by finding an appropriate \(M:\forall X.\sigma\), given \(\sigma\) and \(N:[\rho/X]\sigma\). He defines, for a given type \(\sigma\), a type \(\rho\) to be generic and a term \(N\) to be a prototype proof of \([\rho/X] \sigma\) if there exists a term \(P\) such that \(P:\sigma\) and \([\rho/X] P=N: [\rho/X] \sigma\). (= is an extended \(\beta\eta\) equality and there are some restrictions on \(X\).) Given this generic type and prototype, \(\land X.P\), the abstraction of \(P\) w.r.t. the type variable \(X\), will be the required \(M\). He shows that given \(\sigma,\rho,X\) and \(N\), it is decidable whether \(\rho\) is generic and \(N\) is a prototype proof of \([\rho/X]\sigma\). He also shows that for a generic \(\rho\) and a prototype proof \(N\) of \([\rho/X]\sigma\), \[ [\rho/X] M=N= [\rho/X]M': [\rho/X] \sigma\Leftrightarrow M=M'. \]