Nuprl Definition : cubical-pi-family
cubical-pi-family(X;A;B;I;a) ==
{w:J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))|
∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:A(f(a)).
((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)) ∈ B(g((f(a);u))))}
Wellformedness Lemmas :
cubical-pi-family_wf
Definitions occuring in Statement :
cc-adjoin-cube: (v;u),
cube-context-adjoin: X.A,
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
cube-set-restriction: f(s),
name-comp: (f o g),
name-morph: name-morph(I;J),
coordinate_name: Cname,
list: T List,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
list: T List,
coordinate_name: Cname,
name-morph: name-morph(I;J),
all: ∀x:A. B[x],
equal: s = t ∈ T,
cubical-type-at: A(a),
cube-context-adjoin: X.A,
cc-adjoin-cube: (v;u),
apply: f a,
name-comp: (f o g),
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s)
FDL editor aliases :
cubical-pi-family
cubical-pi-family
Latex:
cubical-pi-family(X;A;B;I;a) ==
\{w:J:(Cname List) {}\mrightarrow{} f:name-morph(I;J) {}\mrightarrow{} u:A(f(a)) {}\mrightarrow{} B((f(a);u))|
\mforall{}J,K:Cname List. \mforall{}f:name-morph(I;J). \mforall{}g:name-morph(J;K). \mforall{}u:A(f(a)).
((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)))\}
Date html generated:
2016_06_16-PM-05_42_05
Last ObjectModification:
2015_09_23-AM-09_30_37
Theory : cubical!sets
Home
Index