Nuprl Definition : extend-to-contraction
extend-to-contraction(Gamma;A;ext) ==
contr-witness(Gamma;ext Gamma 1(Gamma) 0(𝔽) discr(⋅);<>(ext Gamma.A.𝕀 p o p (q=1) (q)p))
Definitions occuring in Statement :
contr-witness: contr-witness(X;c;p),
term-to-path: <>(a),
face-one: (i=1),
face-0: 0(𝔽),
interval-type: 𝕀,
discrete-cubical-term: discr(t),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-id: 1(X),
csm-comp: G o F,
it: ⋅,
apply: f a
Definitions occuring in definition :
contr-witness: contr-witness(X;c;p),
csm-id: 1(X),
face-0: 0(𝔽),
discrete-cubical-term: discr(t),
it: ⋅,
term-to-path: <>(a),
apply: f a,
csm-comp: G o F,
interval-type: 𝕀,
cube-context-adjoin: X.A,
face-one: (i=1),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
extend-to-contraction
Latex:
extend-to-contraction(Gamma;A;ext) ==
contr-witness(Gamma;ext Gamma 1(Gamma) 0(\mBbbF{}) discr(\mcdot{});<>(ext Gamma.A.\mBbbI{} p o p (q=1) (q)p))
Date html generated:
2017_02_21-AM-10_57_59
Last ObjectModification:
2017_01_20-PM-08_22_28
Theory : cubical!type!theory
Home
Index