Step
*
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
⊢ (fst(equiv_comp_apply(<λI.(alpha:G(I) × c𝕌(alpha))
, λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>
>;decode(λI,a.
(A I
(fst(a))));decode(λI,p.
(snd(p)));λH,sigma,phi,u,a0,I,rho.
((snd((A I+new-name(I)
(fst((sigma I+new-name(I)
(s(rho);<new-name(I)>)))))))
I
new-name(I)
1
(phi I rho)
(λI@0,a. (u I@0
(H.𝕀 I+new-name(I) I@0 (iota I@0 a)
(s(rho);<new-name(I)>))))
(a0 I rho));λH,sigma,phi,u,a0,I,rho. ((snd(snd((sigma\000C I+new-name(I)
(s(rho);<new-name(I)>)))))
I
new-name(I)
1
(phi I rho)
(λI@0,a. (u I@0
(H.𝕀 I+new-name(I) I@0
(iota I@0 a)
(s(rho);<new-name(I)>))))
(a0 I
rho));I;λ2x x@0.cube+(I;new-name(I)) \000Cx
x@0(1(1(1(s(1(a))))));...;λ2K f....;...)))
J
f
u ~ 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 ∧ <new-name(J)>> ⋅ 1 (0)<1 ⋅ f> ∨ 0
(λI@1,a@0. (if ((0)<1 ⋅ f ⋅ s ⋅ a@0>==1) then (fst(⋅)) I@1 1 else λu.u fi
((snd((A I@1+new-name(I@1)
cube+(I;new-name(I)) I@1+new-name(I@1)
<1 ⋅ f ⋅ s ⋅ a@0 ⋅ s
, 1 ∧ ¬(dM-lift(I@1+new-name(I@1);I@1;s)
¬(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>) ∧ <new-name(I@1)>)
>(1(1(1(s(1(a)))))))))
I@1
new-name(I@1)
1
0 ∨ dM-to-FL(I@1;¬(¬(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>)))
(λI@0,a@1. ((((u 1 s) 1 a@0) 1 s) 1 a@1))
((u 1 s) 1 a@0))))
((snd((A J+new-name(J) cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, 1 ∧ ¬(1 ∧ <new-name(J)>)>(1(1(1(s(1(a))))\000C))))) J new-name(J) 1 0
(λI@1,a@0. ((u 1 s) 1 a@0))
u)
BY
{ ((RW (AddrC [1] (TagC (mk_tag_term 100))) 0 THEN RW (AddrC [1;1;1;1;1;1;1;1] (LiftC false)) 0)
THEN Reduce 0
THEN RW (AddrC [1;1;1;1;1;1;1] (LiftC false)) 0
THEN Reduce 0
THEN (RW (AddrC [1;1;1;1;1;1] (LiftC false)) 0 THEN Reduce 0)
THEN (RW (AddrC [1;1;1;1;1] (LiftC false)) 0 THEN Reduce 0)
THEN RW (AddrC [1;1;1;1] (LiftC false)) 0
THEN Reduce 0
THEN RW (AddrC [1;1;1] (LiftC false)) 0
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)<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(...)) ... ...(...)[...;...]))) ... ... ... ... ...
...)))
... ~ ...
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{} (fst(equiv\_comp\_apply(<\mlambda{}I.(alpha:G(I) \mtimes{} c\mBbbU{}(alpha))
, \mlambda{}I,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>
>decode(\mlambda{}I,a.
(A I
(fst(a))));decode(\mlambda{}I,p.
(snd(p)));\mlambda{}H,sigma,phi,u,a0,I,rho.
((snd(...))
I
new-name(I)
1
(phi I rho)
(\mlambda{}I@0,a. (u I@0
(H.\mBbbI{} I+new-name(I) I@0
(iota I@0 a)
(s(rho);
<new-name(I)>))))
(a0 I
rho));\mlambda{}H,sigma,phi,u,a0,I,rho.
((snd(snd((sigma
I+new-name(I)
...))))
I
new-name(I)
1
(phi I rho)
(\mlambda{}I@0,a.
(u I@0
(H.\mBbbI{}
I+new-name(I)
I@0
(iota I@0 a)
...)))
(a0 I rho));I;\mlambda{}\msubtwo{}x x@0.cu\000Cbe+(I;new-name(I)) x
x@0(...);...;...;...)))
J
f
u \msim{} 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 \mcdot{} cube+(I;new-name(I)) J+new-name(J) ə \mcdot{} f \mcdot{} s, 1 \mwedge{} <new-name(J)>> \mcdot{} 1 \000C(0)ə \mcdot{} f> \mvee{} 0
(\mlambda{}I@1,a@0. (if ((0)ə \mcdot{} f \mcdot{} s \mcdot{} a@0>==1) then (fst(\mcdot{})) I@1 1 else \mlambda{}u.u fi
((snd((A I@1+new-name(I@1)
cube+(I;new-name(I)) I@1+new-name(I@1)
ə \mcdot{} f \mcdot{} s \mcdot{} a@0 \mcdot{} s
, 1 \mwedge{} \mneg{}(dM-lift(I@1+new-name(I@1);I@1;s)
\mneg{}(dM-lift(I@1;J+new-name(J);a@0)
<new-name(J)>) \mwedge{} <new-name(I@1)>)
>(1(1(1(s(1(a)))))))))
I@1
new-name(I@1)
1
0 \mvee{} dM-to-FL(I@1;\mneg{}(\mneg{}(dM-lift(I@1;J+new-name(J);a@0) <new-name(J)>)))
(\mlambda{}I@0,a@1. ((((u 1 s) 1 a@0) 1 s) 1 a@1))
((u 1 s) 1 a@0))))
((snd((A J+new-name(J)
cube+(I;new-name(I)) J+new-name(J) ə \mcdot{} f \mcdot{} s, 1 \mwedge{} \mneg{}(1 \mwedge{} <new-name(J)>)>(1(1(1(s(1(a\000C)))))))))
J
new-name(J)
1
0
(\mlambda{}I@1,a@0. ((u 1 s) 1 a@0))
u)
By
Latex:
((RW (AddrC [1] (TagC (mk\_tag\_term 100))) 0 THEN RW (AddrC [1;1;1;1;1;1;1;1] (LiftC false)) 0)
THEN Reduce 0
THEN RW (AddrC [1;1;1;1;1;1;1] (LiftC false)) 0
THEN Reduce 0
THEN (RW (AddrC [1;1;1;1;1;1] (LiftC false)) 0 THEN Reduce 0)
THEN (RW (AddrC [1;1;1;1;1] (LiftC false)) 0 THEN Reduce 0)
THEN RW (AddrC [1;1;1;1] (LiftC false)) 0
THEN Reduce 0
THEN RW (AddrC [1;1;1] (LiftC false)) 0
THEN Reduce 0)
Home
Index