Nuprl Definition : face_lattice-deq
face_lattice-deq() == deq-fset(deq-fset(sumdeq(NamesDeq;NamesDeq)))
Definitions occuring in Statement :
names-deq: NamesDeq,
deq-fset: deq-fset(eq),
sumdeq: sumdeq(a;b)
Definitions occuring in definition :
deq-fset: deq-fset(eq),
sumdeq: sumdeq(a;b),
names-deq: NamesDeq
FDL editor aliases :
face_lattice-deq
Latex:
face\_lattice-deq() == deq-fset(deq-fset(sumdeq(NamesDeq;NamesDeq)))
Date html generated:
2016_05_18-PM-00_09_08
Last ObjectModification:
2015_10_13-PM-03_47_20
Theory : cubical!type!theory
Home
Index