Nuprl Definition : name-path-endpoints

name-path-endpoints(X;A;a;b;I;alpha;z;omega) ==

  ((omega iota(z)(alpha) (z:=0)) = (a I alpha) ∈ A(alpha)) ∧ ((omega iota(z)(alpha) (z:=1)) = (b I alpha) ∈ A(alpha))

Definitions occuring in Statement : cubical-type-ap-morph: (u a f), cubical-type-at: A(a), cube-set-restriction: f(s), iota: iota(x), face-map: (x:=i), cons: [a / b], and: P ∧ Q, apply: f a, natural_number: $n, equal: s = t ∈ T
Definitions occuring in definition : and: P ∧ Q, equal: s = t ∈ T, cubical-type-at: A(a), cubical-type-ap-morph: (u a f), face-map: (x:=i), natural_number: $n, cube-set-restriction: f(s), cons: [a / b], iota: iota(x), apply: f a
FDL editor aliases : name-path-endpoints name-path-endpoints

Latex:
name-path-endpoints(X;A;a;b;I;alpha;z;omega) == ((omega iota(z)(alpha) (z:=0)) = (a I alpha)) \mwedge{} ((omega iota(z)(alpha) (z:=1)) = (b I alpha)) Date html generated: 2016_06_16-PM-07_27_24 Last ObjectModification: 2015_09_23-AM-09_33_58 Theory : cubical!sets Home Index