Nuprl Definition : A-face-name
A-face-name(f) == <fst(f), fst(snd(f))>
Definitions occuring in Statement :
pi1: fst(t)
,
pi2: snd(t)
,
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>
,
pi1: fst(t)
,
pi2: snd(t)
FDL editor aliases :
A-face-name
Latex:
A-face-name(f) == <fst(f), fst(snd(f))>
Date html generated:
2016_06_16-PM-05_49_32
Last ObjectModification:
2015_09_23-AM-09_31_15
Theory : cubical!sets
Home
Index