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