Step
*
1
1
of Lemma
transEquiv-trans-sq
1. [G] : Top
2. [A] : Top
3. [p] : Top
4. [I] : Top
5. [a] : Top
6. [J] : Top
7. [f] : Top
8. [u] : Top
⊢ let x,cA = p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 <new-name(I)>
in ((cA)<1>)<cube+(I;new-name(I)) J+new-name(J)
(m J+new-name(J) <fst(fst((s((f(<1, 1>);u));<new-name(J)>))), snd((s((f(<1, 1>);u));<new-name(J)>))>)>
J
new-name(J)
1
λ2K f.(0 ⋅ f)[J;fst(fst((f(<1, 1>);u)))] ∨ dM-to-FL(J;¬(snd(fst((f(<1, 1>);u)))))
(λI@1,a@0.
(if (λ2K f.(0 ⋅ f)[I@1;
fst((m I@1
<fst(fst((<λJ.J ⟶ I
, λI,J,f,g. g ⋅ f
>.𝕀.((decode(λI,a. (A I (fst(a)))))
λx,x@0.
<λ2x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a))))))[x;m x
x@0]
, λ2x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(...)) ...
x
x@0)[x;
m x
x@0]
>)[1(𝕀)].𝕀
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(<1, 1>);u));<new-name(J)>))))
, snd((<λJ.J ⟶ I
, λI,J,f,g. g ⋅ f
>.𝕀.((decode(λI,a. (A I (fst(a)))))
λx,x@0.
<λ2x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a))))))[x;m x x@0]
, λ2x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(...))) ...
x
x@0)[x;
m x
x@0]
>)[1(𝕀)].𝕀
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(<1, 1>);u));<new-name(J)>)))
>))]==1)
then fst(⋅)
else fst(λ2K f.(<λJ,f,u. u
, cubical-id-is-equiv(G;<λI,a. fst((A I a))(1), λI,J,f,a,x. (x 1 f)>) I a
> <(new-name(I)0)(1(1(1(s(1(a))))))
, ((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) (new-name(I)0))
> f)[I@1;
fst((m I@1
<fst(fst((<λJ.J ⟶ I
, λI,J,f,g. g ⋅ f
>.𝕀.((decode(λI,a. (A I (fst(a)))))
λx,x@0.
<λ2x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a))))))[x;m x x@0]
, λ2x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) ...
x
x@0)[x;
m x
x@0]
>)[1(𝕀)].𝕀
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(<1, 1>);u));<new-name(J)>))))
, snd((<λJ.J ⟶ I
, λI,J,f,g. g ⋅ f
>.𝕀.((decode(λI,a. (A I (fst(a)))))
λx,x@0.
<λ2x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a))))))[x;m x x@0]
, λ2x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) cube+(I;...)
x
x@0)[x;m x
x@0]
>)[1(𝕀)].𝕀
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(<1, 1>);u));<new-name(J)>)))
>))])
fi
I@1
1
((snd((A I@1+new-name(I@1) λ2x x@0.cube+(I;new-name(...)) ... ...(...)[...;...]))) ... ... ... ... ...
...)))
... ~ ...
BY
{ (RepUR ``csm-composition csm-ap`` 0
THEN (Subst' <1> J+new-name(J)
(<cube+(I;new-name(I)) J+new-name(J)
(m J+new-name(J) <fst(fst((s((f(<1, 1>);u));<new-name(J)>))), snd((s((f(<1, 1>);u));<new-name(J)>))>)>\000C
J+new-name(J)
1) ~ 1 ⋅ cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, ((1 1 f) 1 ⋅ f s) ∧ <new-name(J)>> ⋅ 1 0
THENA (RepUR ``context-map formal-cube csm-m cube-set-restriction cube-context-adjoin cc-adjoin-cube`` 0
THEN Auto
)
)
THEN RepUR ``so_apply`` 0
THEN (Subst' arrow(<λJ.J ⟶ I
, λI,J,f,g. g ⋅ f
>.𝕀.((decode(λI,a. (A I (fst(a)))))
λx,x@0. <λ2x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a)))))) x (m x x@0)
, λ2x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) cube+(I;new-name(I)) x x@0)
x
(m x x@0)
>)[1(𝕀)].𝕀) ~ λI@0,J,f,p@0. <<<fst(fst(fst(p@0))) ⋅ f, (snd(fst(fst(p@0))) fst(fst(fst(p@0))) f)>
, (snd(fst(p@0)) fst(fst(p@0)) f)
>
, (snd(p@0) fst(p@0) f)
> 0
THENA (RepUR ``cube-context-adjoin`` 0 THEN Auto)
)
THEN Reduce 0) }
1
1. [G] : Top
2. [A] : Top
3. [p] : Top
4. [I] : Top
5. [a] : Top
6. [J] : Top
7. [f] : Top
8. [u] : Top
⊢ let x,cA = p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 <new-name(I)>
in cA J new-name(J) 1 ⋅ cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, ((1 1 f) 1 ⋅ f s) ∧ <new-name(J)>> ⋅ 1
λ2K f.(0 ⋅ f) J (fst(fst((f(<1, 1>);u)))) ∨ dM-to-FL(J;¬(snd(fst((f(<1, 1>);u)))))
(λI@1,a@0.
(if (λ2K f.(0 ⋅ f) I@1
(fst((m I@1
<<fst(fst(fst((s((f(<1, 1>);u));<new-name(J)>)))) ⋅ iota I@1 a@0
, (snd(fst(fst((s((f(<1, 1>);u));<new-name(J)>)))) fst(fst(fst((s((f(<1, 1>);u));
<new-name(J)>)))) iota I@1 a@0)
>
, (snd((s((f(<1, 1>);u));<new-name(J)>)) fst((s((f(<1, 1>);u));<new-name(J)>)) iota I@1 a@0)
>)))==1)
then fst(⋅)
else fst((λ2K f.(<λJ,f,u. u
, cubical-id-is-equiv(G;<λI,a. fst((A I a))(1), λI,J,f,a,x. (x 1 f)>) I a
> <(new-name(I)0)(1(1(1(s(1(a))))))
, ((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) (new-name(I)0))
> f)
I@1
(fst((m I@1
<<fst(fst(fst((s((f(<1, 1>);u));<new-name(J)>)))) ⋅ iota I@1 a@0
, (snd(fst(fst((s((f(<1, 1>);u));<new-name(J)>)))) fst(fst(fst((s((f(<1, 1>);u));
<new-name(J)>)))) iota I@1
a@0)
>
, (snd((s((f(<1, 1>);u));<new-name(J)>)) fst((s((f(<1, 1>);u));<new-name(J)>)) iota I@1 a@0\000C)
>)))))
fi
I@1
1
((snd((A I@1+new-name(I@1)
(λ2x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a)))))) I@1+new-name(I@1)
(m I@1+new-name(I@1)
<fst(fst((m I@1+new-name(I@1)
(s(<<<fst(fst(fst((s((f(<1, 1>);u));<new-name(J)>)))) ⋅ iota I@1 a@0
, (snd(fst(fst((s((f(<1, 1>);u));
<new-name(J)>)))) fst(fst(fst((s((f(<1, 1>);u));
<new-name(J)>)))) iota I@1 a@0)
>
, (snd(fst((s((f(<1, 1>);u));<new-name(J)>))) fst(fst((s((f(<1, 1>);u));
<new-name(J)>))) iota I@1 a@0)
>
, ¬((snd((s((f(<1, 1>);u));<new-name(J)>)) fst((s((f(<1, 1>);u));
<new-name(J)>)) iota I@1 a@0))
>);<new-name(I@1)>))))
, ¬(snd((m I@1+new-name(I@1)
(s(<<<fst(fst(fst((s((f(<1, 1>);u));<new-name(J)>)))) ⋅ iota I@1 a@0
, (snd(fst(fst((s((f(<1, 1>);u));
<new-name(J)>)))) fst(fst(fst((s((f(<1, 1>);u));
<new-name(J)>)))) iota I@1 a@0)
>
, (snd(fst((s((f(<1, 1>);u));<new-name(J)>))) fst(fst((s((f(<1, 1>);u));
<new-name(J)>))) iota I@1 a@0)
>
, ¬((snd((s((f(<1, 1>);u));<new-name(J)>)) fst((s((f(<1, 1>);u));<new-name(J)>)) iota \000CI@1
a@0))
>);<new-name(I@1)>))))
>)))))
I@1
new-name(I@1)
1
0 ∨ dM-to-FL(I@1;¬(¬((snd((s((f(<1, 1>);u));<new-name(J)>)) fst((s((f(<1, 1>);u));<new-name(J)>)) iota I@1\000C
a@0))))
(λI@0,a@1. (snd(fst((m I@0
(<λJ.J ⟶ I, λI,J,f,g. g ⋅ f>.𝕀.((decode(λI,a. (A I (fst(a)))))
λx,x@0. <λ2x x@0.cube+(I;new-name(I)) x
x@0(1(1(1(s(1(a))))))
x
(m x ...)
, ...
>)...........
...
...
...
...))))))
...)))
... ~ ...
Latex:
Latex:
1. [G] : Top
2. [A] : Top
3. [p] : Top
4. [I] : Top
5. [a] : Top
6. [J] : Top
7. [f] : Top
8. [u] : Top
\mvdash{} let x,cA = p I+new-name(I) 1(s(1(a))) I+new-name(I) 1 <new-name(I)>
in ((cA)ə>)<cube+(I;new-name(I)) J+new-name(J)
(m J+new-name(J)
<fst(fst((s((f(ə, 1>);u));<new-name(J)>))), snd((s((f(ə, 1>);u));<new-name(J)>))>)\000C>
J
new-name(J)
1
\mlambda{}\msubtwo{}K f.(0 \mcdot{} f)[J;fst(fst((f(ə, 1>);u)))] \mvee{} dM-to-FL(J;\mneg{}(snd(fst((f(ə, 1>);u)))))
(\mlambda{}I@1,a@0.
(if (\mlambda{}\msubtwo{}K f.(0 \mcdot{} f)[I@1;
fst((m I@1
<fst(fst((<\mlambda{}J.J {}\mrightarrow{} I
, \mlambda{}I,J,f,g. g \mcdot{} f
>.\mBbbI{}.((decode(\mlambda{}I,a. (A I (fst(a)))))
\mlambda{}x,x@0.
<\mlambda{}\msubtwo{}x x@0.cube+(I;new-name(I)) x
x@0(1(1(1(s(1(a))))))[x;m x x@0]
, \mlambda{}\msubtwo{}x x@0.((... 1(1(...)) 1) ... ...
x
x@0)[x;
m x
x@0]
>)[1(\mBbbI{})].\mBbbI{}
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(ə, 1>);u));<new-name(J)>))))
, snd((<\mlambda{}J.J {}\mrightarrow{} I
, \mlambda{}I,J,f,g. g \mcdot{} f
>.\mBbbI{}.((decode(\mlambda{}I,a. (A I (fst(a)))))
\mlambda{}x,x@0.
<\mlambda{}\msubtwo{}x x@0.cube+(I;new-name(I)) x
x@0(1(1(1(s(1(a))))))[x;m x x@0]
, \mlambda{}\msubtwo{}x x@0.((p I+new-name(I) 1(s(1(a)))
I+new-name(I)
1
<new-name(I)> ... 1) ... ...
x
x@0)[x;
m x
x@0]
>)[1(\mBbbI{})].\mBbbI{}
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(ə, 1>);u));<new-name(J)>)))
>))]==1)
then fst(\mcdot{})
else fst(\mlambda{}\msubtwo{}K f.(<\mlambda{}J,f,u. u
, cubical-id-is-equiv(G;<\mlambda{}I,a. fst((A I a))(1), \mlambda{}I,J,f,a,x. (x 1 f)>) I\000C a
> <(new-name(I)0)(1(1(1(s(1(a))))))
, ((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) (new-name(I)0))
> f)[I@1;
fst((m I@1
<fst(fst((<\mlambda{}J.J {}\mrightarrow{} I
, \mlambda{}I,J,f,g. g \mcdot{} f
>.\mBbbI{}.((decode(\mlambda{}I,a. (A I (fst(a)))))
\mlambda{}x,x@0.
<\mlambda{}\msubtwo{}x x@0.cube+(I;new-name(I)) x
x@0(1(1(1(s(1(a))))))[x;m x x@0]
, \mlambda{}\msubtwo{}x x@0.((p I+new-name(I) 1(s(1(a)))
I+new-name(I)
1
<new-name(I)> 1(...) 1) ... ...
x
x@0)[x;
m x
x@0]
>)[1(\mBbbI{})].\mBbbI{}
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(ə, 1>);u));<new-name(J)>))))
, snd((<\mlambda{}J.J {}\mrightarrow{} I
, \mlambda{}I,J,f,g. g \mcdot{} f
>.\mBbbI{}.((decode(\mlambda{}I,a. (A I (fst(a)))))
\mlambda{}x,x@0.
<\mlambda{}\msubtwo{}x x@0.cube+(I;new-name(I)) x
x@0(1(1(1(s(1(a))))))[x;m x x@0]
, \mlambda{}\msubtwo{}x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I)
1
<new-name(I)> 1(1(...)) 1) ... ...
x
x@0)[x;
m x
x@0]
>)[1(\mBbbI{})].\mBbbI{}
J+new-name(J)
I@1
(iota I@1 a@0)
(s((f(ə, 1>);u));<new-name(J)>)))
>))])
fi
I@1
1
((snd((A I@1+new-name(I@1)
\mlambda{}\msubtwo{}x x@0.cube+(I;new-name(I)) x
x@0(1(1(1(s(1(a))))))[I@1+new-name(I@1);
m I@1+new-name(I@1)
<fst(fst((m I@1+new-name(I@1)
(s(<fst((<\mlambda{}J.J {}\mrightarrow{} I
, \mlambda{}I,J,f,g. g \mcdot{} f
>.\mBbbI{}.((decode(\mlambda{}I,a. (A I
(fst(a)))))
\mlambda{}x,x@0. ...).......
...
...
...
...))
, ...
>);...))))
, ...
>])))
...
...
...
...
...
...)))
... \msim{} ...
By
Latex:
(RepUR ``csm-composition csm-ap`` 0
THEN (Subst' ə> J+new-name(J)
(<cube+(I;new-name(I)) J+new-name(J)
(m J+new-name(J)
<fst(fst((s((f(ə, 1>);u));<new-name(J)>))), snd((s((f(ə, 1>);u));<new-name(J)>))>\000C)>
J+new-name(J)
1) \msim{} 1 \mcdot{} cube+(I;new-name(I)) J+new-name(J)
ə \mcdot{} f \mcdot{} s, ((1 1 f) 1 \mcdot{} f s) \mwedge{} <new-name(J)>> \mcdot{} 1 0
THENA (...
THEN Auto
)
)
THEN RepUR ``so\_apply`` 0
THEN (Subst' arrow(<\mlambda{}J.J {}\mrightarrow{} I
, \mlambda{}I,J,f,g. g \mcdot{} f
>.\mBbbI{}.((decode(\mlambda{}I,a. (A I (fst(a)))))
\mlambda{}x,x@0.
<\mlambda{}\msubtwo{}x x@0.cube+(I;new-name(I)) x x@0(1(1(1(s(1(a)))))) x (m x x@0)
, \mlambda{}\msubtwo{}x x@0.((p I+new-name(I) 1(s(1(a))) I+new-name(I) 1
<new-name(I)> 1(1(s(1(a)))) 1) 1(1(1(s(1(a))))) cube+(I;...)
x
x@0)
x
(m x x@0)
>)[1(\mBbbI{})].\mBbbI{}) \msim{} \mlambda{}I@0,J,f,p@0. <<<fst(fst(fst(p@0))) \mcdot{} f
, (snd(fst(fst(p@0))) fst(fst(fst(p@0))) f)
>
, (snd(fst(p@0)) fst(fst(p@0)) f)
>
, (snd(p@0) fst(p@0) f)
> 0
THENA (RepUR ``cube-context-adjoin`` 0 THEN Auto)
)
THEN Reduce 0)
Home
Index