Step
*
1
of Lemma
transEquiv-trans-eq
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. ∀[I:fset(ℕ)]. ∀[a:G(I)]. (p(a) ∈ (Path_c𝕌 A B)(a))
6. I : fset(ℕ)
7. a : G(I)
⊢ (transEquivFun(p) I a)
= (λJ,f,u. ((snd((p(s(a)) I+new-name(I) 1 <new-name(I)>))) J new-name(J) f,new-name(I)=new-name(J) 0 ⋅
(compOp(A) J new-name(J) s(f(a)) 0 ⋅ u)))
∈ (decode(A) ⟶ decode(B))(a)
BY
{ ((Assert transEquivFun(p) I a ∈ (decode(A) ⟶ decode(B))(a) BY
Auto)
THEN (RepUR ``cubical-fun cubical-fun-family`` -1 THEN (MemTypeHD (-1) THENA Auto))
THEN RepUR ``cubical-fun cubical-fun-family`` 0
THEN (MemTypeCD THENA Auto)
THEN RepeatFor 3 ((FunExt THENA Auto))
THEN Reduce 0
THEN (RWO "transEquiv-trans-sq" 0 THENA Auto)
THEN (Subst' (0)<1 ⋅ f> ∨ 0 ~ 0 0 THENA ByComputation 1000)
THEN (GenConcl ⌜(λ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))))
= uu
∈ Top⌝⋅
THENA Auto
)
THEN (Subst' p I+new-name(I) 1(s(1(a))) ~ p(1(s(1(a)))) 0 THENA (Fold `cubical-term-at` 0 THEN Auto))) }
1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. ∀[I:fset(ℕ)]. ∀[a:G(I)]. (p(a) ∈ (Path_c𝕌 A B)(a))
6. I : fset(ℕ)
7. a : G(I)
8. (transEquivFun(p) I a) = (transEquivFun(p) I a) ∈ (J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:decode(A)(f(a)) ⟶ decode(B)(f(a)))
9. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:decode(A)(f(a)).
((transEquivFun(p) I a J f u f(a) g) = (transEquivFun(p) I a K f ⋅ g (u f(a) g)) ∈ decode(B)(g(f(a))))
10. J : fset(ℕ)
11. f : J ⟶ I
12. u : decode(A)(f(a))
13. uu : Top
14. (λ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))))
= uu
∈ Top
⊢ let x,cA = p(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 uu
((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)
= ((snd((p(s(a)) I+new-name(I) 1 <new-name(I)>))) J new-name(J) f,new-name(I)=new-name(J) 0 ⋅
(compOp(A) J new-name(J) s(f(a)) 0 ⋅ u))
∈ decode(B)(f(a))
Latex:
Latex:
1. G : CubicalSet\{j\}
2. A : \{G \mvdash{} \_:c\mBbbU{}\}
3. B : \{G \mvdash{} \_:c\mBbbU{}\}
4. p : \{G \mvdash{} \_:(Path\_c\mBbbU{} A B)\}
5. \mforall{}[I:fset(\mBbbN{})]. \mforall{}[a:G(I)]. (p(a) \mmember{} (Path\_c\mBbbU{} A B)(a))
6. I : fset(\mBbbN{})
7. a : G(I)
\mvdash{} (transEquivFun(p) I a)
= (\mlambda{}J,f,u. ((snd((p(s(a)) I+new-name(I) 1 <new-name(I)>))) J new-name(J) f,new-name(I)=new-name(J)
0
\mcdot{}
(compOp(A) J new-name(J) s(f(a)) 0 \mcdot{} u)))
By
Latex:
((Assert transEquivFun(p) I a \mmember{} (decode(A) {}\mrightarrow{} decode(B))(a) BY
Auto)
THEN (RepUR ``cubical-fun cubical-fun-family`` -1 THEN (MemTypeHD (-1) THENA Auto))
THEN RepUR ``cubical-fun cubical-fun-family`` 0
THEN (MemTypeCD THENA Auto)
THEN RepeatFor 3 ((FunExt THENA Auto))
THEN Reduce 0
THEN (RWO "transEquiv-trans-sq" 0 THENA Auto)
THEN (Subst' (0)ə \mcdot{} f> \mvee{} 0 \msim{} 0 0 THENA ByComputation 1000)
THEN (GenConcl \mkleeneopen{}(\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))))
= uu\mkleeneclose{}\mcdot{}
THENA Auto
)
THEN (Subst' p I+new-name(I) 1(s(1(a))) \msim{} p(1(s(1(a)))) 0
THENA (Fold `cubical-term-at` 0 THEN Auto)
))
Home
Index