Step
*
1
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)
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))
BY
{ (Assert ∀J:fset(ℕ). ∀f:J ⟶ I. ∀x:Point(dM(J+new-name(J))).
((cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, x>)
= (λi.if (i =z new-name(I)) then x else f i fi )
∈ formal-cube(I+new-name(I))(J+new-name(J))) BY
(All Thin
THEN Intros
THEN RepUR ``formal-cube names-hom cube+ nc-e\'`` 0
THEN (FunExt THENA Auto)
THEN Reduce 0
THEN AutoSplit
THEN FLemma `not-added-name` [-1]
THEN Auto
THEN Subst' 1 ⋅ f ⋅ s = f ⋅ s ∈ J+new-name(J) ⟶ I 0
THEN Auto
THEN RepUR ``nh-comp nc-s dma-lift-compose`` 0
THEN Fold `dM` 0
THEN Fold `dM-lift` 0
THEN BLemma `dM-lift-is-id2`
THEN Auto
THEN MemTypeCD
THEN EAuto 1)) }
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
15. ∀J:fset(ℕ). ∀f:J ⟶ I. ∀x:Point(dM(J+new-name(J))).
((cube+(I;new-name(I)) J+new-name(J) <1 ⋅ f ⋅ s, x>) = (λi.if (i =z new-name(I)) then x else f i fi ) ∈ formal-cub\000Ce(I+new-name(I))(J+new-name(J)))
⊢ 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)
8. (transEquivFun(p) I a) = (transEquivFun(p) I a)
9. \mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:decode(A)(f(a)).
((transEquivFun(p) I a J f u f(a) g) = (transEquivFun(p) I a K f \mcdot{} g (u f(a) g)))
10. J : fset(\mBbbN{})
11. f : J {}\mrightarrow{} I
12. u : decode(A)(f(a))
13. uu : Top
14. (\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
\mvdash{} let x,cA = p(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 0 uu\000C
((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)>)>\000C(1(1(1(s(1(a))))))))) J
new-name(J)
1
0
(\mlambda{}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 \mcdot{}
(compOp(A) J new-name(J) s(f(a)) 0 \mcdot{} u))
By
Latex:
(Assert \mforall{}J:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I. \mforall{}x:Point(dM(J+new-name(J))).
((cube+(I;new-name(I)) J+new-name(J) ə \mcdot{} f \mcdot{} s, x>) = (\mlambda{}i.if (i =\msubz{} new-name(I)) then x el\000Cse f i fi )) BY
(All Thin
THEN Intros
THEN RepUR ``formal-cube names-hom cube+ nc-e\mbackslash{}'`` 0
THEN (FunExt THENA Auto)
THEN Reduce 0
THEN AutoSplit
THEN FLemma `not-added-name` [-1]
THEN Auto
THEN Subst' 1 \mcdot{} f \mcdot{} s = f \mcdot{} s 0
THEN Auto
THEN RepUR ``nh-comp nc-s dma-lift-compose`` 0
THEN Fold `dM` 0
THEN Fold `dM-lift` 0
THEN BLemma `dM-lift-is-id2`
THEN Auto
THEN MemTypeCD
THEN EAuto 1))
Home
Index