Nuprl Definition : equiv_comp_apply
equiv_comp_apply(H;A;E;cA;cE;I;a;b;c;d) ==
<λJ,f,u@0. (cE <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m x x@0], b[x;m x x@0]>)[1(𝕀)]
(λx,x@0. <a[x;m x <fst(fst(x@0)), snd(x@0)>], b[x;m x <fst(fst(x@0)), snd(x@0)>]>)
(λI,a. c[I;fst(fst(a))] ∨ dM-to-FL(I;¬(snd(fst(a)))))
(λI@0,a@0. (if (c[I@0;fst((m I@0 <fst(fst(a@0)), snd(a@0)>))]==1)
then fst(⋅)
else fst(d[I@0;fst((m I@0 <fst(fst(a@0)), snd(a@0)>))])
fi
I@0
1
(cA <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m x x@0], b[x;m x x@0]>)[1(𝕀)].𝕀
(λx,x@0. <a[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
, b[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
>)
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. (snd(fst((m I rho)))))
(λI,a. (snd(fst(a))))
I@0
<fst(a@0), ¬(snd(a@0))>)))
(λI@0,a@0. ((fst(d[I@0;fst(fst(a@0))])) I@0 1
(cA <λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((A)λx,x@0. <a[x;m x x@0], b[x;m x x@0]>)[1(𝕀)].𝕀
(λx,x@0. <a[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
, b[x;m x <fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
>)
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. (snd(fst((m I rho)))))
(λI,a. (snd(fst(a))))
I@0
<a@0, ¬(0)>)))
J
(f(<1, 1>);u@0))
, λJ,f,u@0.
(cubical-pair(λI@0,a@1.
<cA
<λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.(let x,F = E
in <λJ,c. (x J <a[J;c], b[J;c]>)
, λK,J,f,c,u. (F K J f <a[K;c], b[K;c]> u)
>)[1(𝕀)].𝕀.𝕀
(λx,x@0. <a[x;<fst(fst((m x (m x x@0)))), snd((m x (m x x@0)))>]
, b[x;<fst(fst((m x (m x x@0)))), snd((m x (m x x@0)))>]
>)
(λI,rho.
c
[I;fst(fst(fst(rho)))] ∨ dM-to-FL(I;¬(snd(fst(rho)))) ∨ dM-to-FL(I;¬(...)))\000C
(λI@0,rho.
if (c[I@0;fst(fst(fst((m I@0
rho))))] ∨ dM-to-FL(I@0;¬(snd(fst((m I@0
rho)))))==1)
then fst(if (c[I@0;fst(fst((m I@0 (m I@0 rho))))]==1)
then fst(((snd(⋅)) I@0 1
(cE
<λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.(let x,F = E
in <λJ,c. (x J <a[J;c], b[J;c]>)
, λK,J,f,c,u. (F K J f
<a[K;c], b[K;c]>
u)
>)[1(𝕀)].𝕀
(λx,x@0. <a[x;<fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
, b[x;<fst(fst((m x x@0))), ¬(snd((m x x@0)))>]
>)
(λI,rho. 0 ∨ dM-to-FL(I;¬(snd(rho))))
(λI,rho. (snd(fst((m I rho)))))
(λI,a. (snd(fst(a))))
I@0
<fst((m I@0 (m I@0 rho)))
, ¬(snd((m I@0 (m I@0 rho))))
>)))
else fst(...)
fi )
else ...
fi )
...
...
...
, ...
>;...)
...
...)
>
Definitions occuring in Statement :
csm-m: m,
cubical-fiber: Fiber(w;a),
path-type: (Path_A a b),
face-zero: (i=0),
face-one: (i=1),
face-or: (a ∨ b),
interval-1: 1(𝕀),
interval-type: 𝕀,
cubical-pair: cubical-pair(u;v),
cubical-app: app(w; u),
cubical-fun: (A ⟶ B),
csm-id-adjoin: [u],
cc-snd: q,
cc-fst: p,
cc-adjoin-cube: (v;u),
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
dM-to-FL: dM-to-FL(I;z),
fl-eq: (x==y),
face_lattice: face_lattice(I),
cube-set-restriction: f(s),
nh-comp: g ⋅ f,
nh-id: 1,
names-hom: I ⟶ J,
dM1: 1,
dM0: 0,
dM: dM(I),
names-deq: NamesDeq,
names: names(I),
dma-neg: ¬(x),
dm-neg: ¬(x),
lattice-0: 0,
lattice-1: 1,
lattice-join: a ∨ b,
ifthenelse: if b then t else f fi ,
it: ⋅,
so_apply: x[s1;s2],
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
product: x:A × B[x]
Definitions occuring in definition :
so_apply: x[s1;s2],
pi1: fst(t),
it: ⋅,
face_lattice: face_lattice(I),
lattice-1: 1,
pi2: snd(t),
pair: <a, b>,
csm-m: m,
apply: f a,
fl-eq: (x==y),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
names-deq: NamesDeq,
names: names(I),
dm-neg: ¬(x),
dM-to-FL: dM-to-FL(I;z),
lattice-join: a ∨ b,
csm-ap-type: (AF)s,
interval-1: 1(𝕀),
interval-type: 𝕀,
nh-comp: g ⋅ f,
names-hom: I ⟶ J,
cube-context-adjoin: X.A,
csm-id-adjoin: [u],
nh-id: 1,
dma-neg: ¬(x),
dM: dM(I),
lattice-0: 0,
dM0: 0,
cc-adjoin-cube: (v;u),
cube-set-restriction: f(s),
dM1: 1,
cubical-pair: cubical-pair(u;v),
spread: spread def,
face-one: (i=1),
face-or: (a ∨ b),
face-zero: (i=0),
cubical-fiber: Fiber(w;a),
cubical-fun: (A ⟶ B),
product: x:A × B[x],
cubical-type-at: A(a),
path-type: (Path_A a b),
cc-fst: p,
csm-ap-term: (t)s,
cubical-app: app(w; u),
cc-snd: q,
cubical-type-ap-morph: (u a f)
FDL editor aliases :
equiv_comp_apply
Latex:
equiv\_comp\_apply(H;A;E;cA;cE;I;a;b;c;d) ==
<\mlambda{}J,f,u@0. (cE <\mlambda{}J.J {}\mrightarrow{} I, \mlambda{}I,J,f,g. g \mcdot{} f>.\mBbbI{}.((A)\mlambda{}x,x@0. <a[x;m x x@0], b[x;m x x@0]>)[1(\mBbbI{})]
(\mlambda{}x,x@0. <a[x;m x <fst(fst(x@0)), snd(x@0)>], b[x;m x <fst(fst(x@0)), snd(x@0)>]>)
(\mlambda{}I,a. c[I;fst(fst(a))] \mvee{} dM-to-FL(I;\mneg{}(snd(fst(a)))))
(\mlambda{}I@0,a@0. (if (c[I@0;fst((m I@0 <fst(fst(a@0)), snd(a@0)>))]==1)
then fst(\mcdot{})
else fst(d[I@0;fst((m I@0 <fst(fst(a@0)), snd(a@0)>))])
fi
I@0
1
(cA <\mlambda{}J.J {}\mrightarrow{} I, \mlambda{}I,J,f,g. g \mcdot{} f>.\mBbbI{}.((A)\mlambda{}x,x@0. <a[x;m x x@0], b[x;m x x@0]\000C>)[1(\mBbbI{})].\mBbbI{}
(\mlambda{}x,x@0. <a[x;m x <fst(fst((m x x@0))), \mneg{}(snd((m x x@0)))>]
, b[x;m x <fst(fst((m x x@0))), \mneg{}(snd((m x x@0)))>]
>)
(\mlambda{}I,rho. 0 \mvee{} dM-to-FL(I;\mneg{}(snd(rho))))
(\mlambda{}I,rho. (snd(fst((m I rho)))))
(\mlambda{}I,a. (snd(fst(a))))
I@0
<fst(a@0), \mneg{}(snd(a@0))>)))
(\mlambda{}I@0,a@0. ((fst(d[I@0;fst(fst(a@0))])) I@0 1
(cA <\mlambda{}J.J {}\mrightarrow{} I, \mlambda{}I,J,f,g. g \mcdot{} f>.\mBbbI{}.((A)\mlambda{}x,x@0. <a[x;m x x@0], b[x;m x x@0]\000C>)[1(\mBbbI{})].\mBbbI{}
(\mlambda{}x,x@0. <a[x;m x <fst(fst((m x x@0))), \mneg{}(snd((m x x@0)))>]
, b[x;m x <fst(fst((m x x@0))), \mneg{}(snd((m x x@0)))>]
>)
(\mlambda{}I,rho. 0 \mvee{} dM-to-FL(I;\mneg{}(snd(rho))))
(\mlambda{}I,rho. (snd(fst((m I rho)))))
(\mlambda{}I,a. (snd(fst(a))))
I@0
<a@0, \mneg{}(0)>)))
J
(f(ə, 1>);u@0))
, \mlambda{}J,f,u@0.
(cubical-pair(\mlambda{}I@0,a@1.
<cA
<\mlambda{}J.J {}\mrightarrow{} I, \mlambda{}I,J,f,g. g \mcdot{} f>.(let x,F = E
in <\mlambda{}J,c. (x J <a[J;c], b[J;c]>)
, \mlambda{}K,J,f,c,u. (F K J f
<a[K;c], b[K;c]>
u)
>)[1(\mBbbI{})].\mBbbI{}.\mBbbI{}
(\mlambda{}x,x@0. <a[x;<fst(fst((m x (m x x@0)))), snd((m x (m x x@0)))>\000C]
, b[x;<fst(fst((m x (m x x@0))))
, snd((m x (m x x@0)))
>]
>)
(\mlambda{}I,rho.
c
[I;fst(fst(fst(rho)))] \mvee{} dM-to-FL(I;\mneg{}(snd(...))) \mvee{} ...)\000C
(\mlambda{}I@0,rho.
if (c
[I@0;fst(fst(fst((m I@0
rho))))] \mvee{} ...==1)
then fst(if (c[I@0;fst(fst((m I@0 (m I@0 rho))))]==1)
then fst(((snd(\mcdot{})) I@0 1
(cE
<\mlambda{}J.J {}\mrightarrow{} I
, \mlambda{}I,J,f,g. g \mcdot{} f
>.(let x,F = E
in <\mlambda{}J,c. (x J <a[J;c], b[J;c]>)
, \mlambda{}K,J,f,c,u. (F K J f
<a[K;c]
, b[K;c]
>
u)
>)[1(\mBbbI{})].\mBbbI{}
(\mlambda{}x,x@0. <a[x;<fst(fst((m x x@0)))
, \mneg{}(snd((m x x@0)))
>]
, b[x;<fst(fst((m x x@0)))
, \mneg{}(snd((m x x@0)))
>]
>)
(\mlambda{}I,rho. 0 \mvee{} dM-to-FL(I;\mneg{}(snd(rho))))\000C
(\mlambda{}I,rho. (snd(fst((m I rho)))))
(\mlambda{}I,a. (snd(fst(a))))
I@0
<fst((m I@0 (m I@0 rho)))
, \mneg{}(snd((m I@0 (m I@0 rho))))
>)))
else fst(((snd(d[I@0;fst(fst((m I@0
(m I@0 ...))))]))
...
...
...))
fi )
else ...
fi )
...
...
...
, ...
>...)
...
...)
>
Date html generated:
2018_05_23-PM-01_44_47
Last ObjectModification:
2017_11_24-PM-08_01_54
Theory : cubical!type!theory
Home
Index