Nuprl Definition : edge-arrows-commute
edge-arrows-commute(C;I;L;E) ==
∀x:name-morph(I;[]). ∀i,j:{i:nameset(I)| (x i) = 0 ∈ ℕ2} .
((¬(i = j ∈ nameset(I)))
⇒ ((cat-comp(C) (L x) (L flip(x;i)) (L flip(flip(x;i);j)) (E i x) (E j flip(x;i)))
= (cat-comp(C) (L x) (L flip(x;j)) (L flip(flip(x;j);i)) (E j x) (E i flip(x;j)))
∈ (cat-arrow(C) (L x) (L flip(flip(x;i);j)))))
Definitions occuring in Statement :
name-morph-flip: flip(f;y),
name-morph: name-morph(I;J),
nameset: nameset(L),
cat-comp: cat-comp(C),
cat-arrow: cat-arrow(C),
nil: [],
int_seg: {i..j-},
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
name-morph: name-morph(I;J),
nil: [],
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
int_seg: {i..j-},
natural_number: $n,
implies: P ⇒ Q,
not: ¬A,
nameset: nameset(L),
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
cat-comp: cat-comp(C),
apply: f a,
name-morph-flip: flip(f;y)
FDL editor aliases :
edge-arrows-commute
Latex:
edge-arrows-commute(C;I;L;E) ==
\mforall{}x:name-morph(I;[]). \mforall{}i,j:\{i:nameset(I)| (x i) = 0\} .
((\mneg{}(i = j))
{}\mRightarrow{} ((cat-comp(C) (L x) (L flip(x;i)) (L flip(flip(x;i);j)) (E i x) (E j flip(x;i)))
= (cat-comp(C) (L x) (L flip(x;j)) (L flip(flip(x;j);i)) (E j x) (E i flip(x;j)))))
Date html generated:
2016_06_16-PM-06_58_06
Last ObjectModification:
2015_09_23-AM-09_33_12
Theory : cubical!sets
Home
Index