Nuprl Definition : I-path
I-path(X;A;a;b;I;alpha) == z:{z:Cname| ¬(z ∈ I)} × named-path(X;A;a;b;I;alpha;z)
Definitions occuring in Statement :
named-path: named-path(X;A;a;b;I;alpha;z),
coordinate_name: Cname,
l_member: (x ∈ l),
not: ¬A,
set: {x:A| B[x]} ,
product: x:A × B[x]
Definitions occuring in definition :
product: x:A × B[x],
set: {x:A| B[x]} ,
not: ¬A,
l_member: (x ∈ l),
coordinate_name: Cname,
named-path: named-path(X;A;a;b;I;alpha;z)
FDL editor aliases :
I-path
I-path
Latex:
I-path(X;A;a;b;I;alpha) == z:\{z:Cname| \mneg{}(z \mmember{} I)\} \mtimes{} named-path(X;A;a;b;I;alpha;z)
Date html generated:
2016_06_16-PM-07_28_38
Last ObjectModification:
2015_09_23-AM-09_34_10
Theory : cubical!sets
Home
Index