Nuprl Definition : church-Nat
cNat == ⋂X:Type. (X ⟶ (X ⟶ X) ⟶ X)
Definitions occuring in Statement :
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
universe: Type
Definitions occuring in definition :
isect: ⋂x:A. B[x],
universe: Type,
function: x:A ⟶ B[x]
FDL editor aliases :
church-Nat
Latex:
cNat == \mcap{}X:Type. (X {}\mrightarrow{} (X {}\mrightarrow{} X) {}\mrightarrow{} X)
Date html generated:
2020_05_20-AM-08_05_08
Last ObjectModification:
2019_11_15-PM-09_48_52
Theory : general
Home
Index