Nuprl Definition : singleton-contr
singleton-contr(X;A;a) ==  contr-witness(X;singleton-center(X;a);singleton-contraction(X.Singleton(a);q.2))
Definitions occuring in Statement : 
singleton-center: singleton-center(X;a)
, 
singleton-type: Singleton(a)
, 
singleton-contraction: singleton-contraction(X;pth)
, 
contr-witness: contr-witness(X;c;p)
, 
cubical-snd: p.2
, 
cc-snd: q
, 
cube-context-adjoin: X.A
Definitions occuring in definition : 
contr-witness: contr-witness(X;c;p)
, 
singleton-center: singleton-center(X;a)
, 
singleton-contraction: singleton-contraction(X;pth)
, 
cube-context-adjoin: X.A
, 
singleton-type: Singleton(a)
, 
cubical-snd: p.2
, 
cc-snd: q
FDL editor aliases : 
singleton-contr
Latex:
singleton-contr(X;A;a)  ==
    contr-witness(X;singleton-center(X;a);singleton-contraction(X.Singleton(a);q.2))
Date html generated:
2018_05_23-AM-09_45_43
Last ObjectModification:
2017_11_07-PM-05_01_13
Theory : cubical!type!theory
Home
Index