Nuprl Definition : A-face-compatible
A-face-compatible(X;A;I;alpha;f1;f2) ==
let y,b,w = f1 in
let z,c,u = f2 in
(¬(y = z ∈ Cname)) ⇒ ((w (y:=b)(alpha) (z:=c)) = (u (z:=c)(alpha) (y:=b)) ∈ A(((z:=c) o (y:=b))(alpha)))
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
cube-set-restriction: f(s),
name-comp: (f o g),
face-map: (x:=i),
cname_deq: CnameDeq,
coordinate_name: Cname,
list-diff: as-bs,
cons: [a / b],
nil: [],
spreadn: spread3,
not: ¬A,
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
spreadn: spread3,
implies: P ⇒ Q,
not: ¬A,
coordinate_name: Cname,
equal: s = t ∈ T,
cubical-type-at: A(a),
name-comp: (f o g),
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
list-diff: as-bs,
cname_deq: CnameDeq,
cons: [a / b],
nil: [],
face-map: (x:=i)
FDL editor aliases :
A-face-compatible
Latex:
A-face-compatible(X;A;I;alpha;f1;f2) ==
let y,b,w = f1 in
let z,c,u = f2 in
(\mneg{}(y = z)) {}\mRightarrow{} ((w (y:=b)(alpha) (z:=c)) = (u (z:=c)(alpha) (y:=b)))
Date html generated:
2016_06_16-PM-05_49_57
Last ObjectModification:
2015_09_23-AM-09_31_20
Theory : cubical!sets
Home
Index