Nuprl Definition : singleton-type
Singleton(a) == Σ A (Path_(A)p (a)p q)
Wellformedness Lemmas :
singleton-type_wf
Definitions occuring in Statement :
path-type: (Path_A a b),
cubical-sigma: Σ A B,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s
Definitions occuring in definition :
cubical-sigma: Σ A B,
path-type: (Path_A a b),
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
singleton-type
Latex:
Singleton(a) == \mSigma{} A (Path\_(A)p (a)p q)
Date html generated:
2018_05_23-AM-09_44_24
Last ObjectModification:
2017_11_07-PM-04_01_09
Theory : cubical!type!theory
Home
Index