Nuprl Definition : discrete_struct
DS(A) == sort:A ⟶ Type × (a:A ⟶ EqDecider(sort a))
Definitions occuring in Statement :
deq: EqDecider(T),
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
product: x:A × B[x],
universe: Type,
function: x:A ⟶ B[x],
deq: EqDecider(T),
apply: f a
FDL editor aliases :
DS
Latex:
DS(A) == sort:A {}\mrightarrow{} Type \mtimes{} (a:A {}\mrightarrow{} EqDecider(sort a))
Date html generated:
2016_05_14-PM-03_24_10
Last ObjectModification:
2015_09_22-PM-05_59_36
Theory : decidable!equality
Home
Index