Nuprl Definition : face-name-eq
face-name-eq(a;b) == product-deq(ℤ;ℤ;IntDeq;IntDeq) a b
Definitions occuring in Statement :
product-deq: product-deq(A;B;a;b),
int-deq: IntDeq,
apply: f a,
int: ℤ
Definitions occuring in definition :
apply: f a,
int: ℤ
FDL editor aliases :
face-name-eq
Latex:
face-name-eq(a;b) == product-deq(\mBbbZ{};\mBbbZ{};IntDeq;IntDeq) a b
Date html generated:
2016_06_16-PM-05_49_19
Last ObjectModification:
2015_09_23-AM-09_31_13
Theory : cubical!sets
Home
Index