Nuprl Definition : path-type
(Path_A a b) == {p:Path(A) | ∀I,alpha. ((p I 1 0) = a(alpha) ∈ A(alpha)) ∧ ((p I 1 1) = b(alpha) ∈ A(alpha))}
Definitions occuring in Statement :
pathtype: Path(A),
cubical-subset: {t:T | ∀I,alpha. psi[I; alpha; t]},
cubical-term-at: u(a),
cubical-type-at: A(a),
nh-id: 1,
dM1: 1,
dM0: 0,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
cubical-subset: {t:T | ∀I,alpha. psi[I; alpha; t]},
pathtype: Path(A),
and: P ∧ Q,
dM0: 0,
equal: s = t ∈ T,
cubical-type-at: A(a),
apply: f a,
nh-id: 1,
dM1: 1,
cubical-term-at: u(a)
FDL editor aliases :
path-type
path-type
Latex:
(Path\_A a b) == \{p:Path(A) | \mforall{}I,alpha. ((p I 1 0) = a(alpha)) \mwedge{} ((p I 1 1) = b(alpha))\}
Date html generated:
2016_06_16-PM-01_42_48
Last ObjectModification:
2016_06_03-AM-08_19_04
Theory : cubical!type!theory
Home
Index