Nuprl Definition : id-fiber-contraction
id-fiber-contraction(X;T) == (singleton-contraction(X.T.(T)p.(Path_((T)p)p (q)p q);q))SigmaElim
Definitions occuring in Statement :
singleton-contraction: singleton-contraction(X;pth),
path-type: (Path_A a b),
sigma-elim-csm: SigmaElim,
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 :
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
cube-context-adjoin: X.A,
path-type: (Path_A a b),
singleton-contraction: singleton-contraction(X;pth),
sigma-elim-csm: SigmaElim
FDL editor aliases :
id-fiber-contraction
Latex:
id-fiber-contraction(X;T) == (singleton-contraction(X.T.(T)p.(Path\_((T)p)p (q)p q);q))SigmaElim
Date html generated:
2017_01_10-AM-09_01_01
Last ObjectModification:
2016_12_14-PM-02_13_48
Theory : cubical!type!theory
Home
Index