Step
*
1
of Lemma
transEquiv-trans-eq2
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. J : fset(ℕ)
9. h : J ⟶ I
10. u : decode(A)(h(a))
⊢ ((snd((p(s(a)) I+new-name(I) 1 <new-name(I)>))) J new-name(J) h,new-name(I)=new-name(J) 0 ⋅
(compOp(A) J new-name(J) s(h(a)) 0 ⋅ u))
= ((snd((p J+new-name(J) s(h(a)) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 discr(⋅)
(compOp(A) J new-name(J) s(h(a)) 0 ⋅ u))
∈ decode(B)(h(a))
BY
{ ((InstLemma `cubical-term-at-morph` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝]⋅ THENA Auto)
THEN (InstHyp [⌜I⌝;⌜a⌝;⌜I+new-name(I)⌝; s ] (-1)⋅ THENA Auto)
THEN (RWO "path-type-ap-morph" (-1) THENA Auto)
THEN (Assert s(h(a)) = h ⋅ s(a) ∈ G(J+new-name(J)) BY
Auto)
THEN (InstHyp [⌜I⌝;⌜a⌝;⌜J+new-name(J)⌝; ⌜h ⋅ s⌝ ] (-3)⋅ THENA Auto)
THEN (RWO "path-type-ap-morph" (-1) THENA Auto)
THEN (ApFunToHypEquands `Z' ⌜p(Z)⌝ ⌜(Path_c𝕌 A B)(Z)⌝ (-2)⋅
THENA (Fold `member` 0
THEN ((InstLemma `cubical-term-at_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝]⋅ THENM BHyp -1)
THENA Auto
)
)
)
THEN (ApFunToHypEquands `Z' ⌜(Path_c𝕌 A B)(Z)⌝ ⌜𝕌'⌝ (-3)⋅
THEN Try ((Eq
ORELSE (Fold `member` 0
THEN InstLemma `cubical-type-at_wf` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅
THEN BHyp -1
THEN Auto)
))
)
THEN (Assert (λK,g. (p(a) K h ⋅ s ⋅ g)) = p(s(h(a))) ∈ (Path_c𝕌 A B)(h ⋅ s(a)) BY
Eq)
THEN RepeatFor 4 (Thin (-2))
THEN (RWO "path-type-at" (-2) THENA Auto)
THEN (EqTypeHD (-2) THENA (D -1 THEN Auto))
THEN (EqTypeHD (-3) THENA (D -1 THEN Auto))
THEN (RWO "path-type-at" (-1) THENA Auto)
THEN (EqTypeHD (-1) THENA (D -1 THEN Auto))
THEN (EqTypeHD (-2) THENA (D -1 THEN Auto))
THEN All Reduce) }
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. J : fset(ℕ)
9. h : J ⟶ I
10. u : decode(A)(h(a))
11. ∀[I:fset(ℕ)]. ∀[a:G(I)]. ∀[J:fset(ℕ)]. ∀[f:J ⟶ I]. ((p(a) a f) = p(f(a)) ∈ (Path_c𝕌 A B)(f(a)))
12. (λK,g. (p(a) K s ⋅ g)) = p(s(a)) ∈ (J:fset(ℕ) ⟶ f:J ⟶ I+new-name(I) ⟶ u:Point(dM(J)) ⟶ c𝕌(f(s(a))))
13. ∀J,K:fset(ℕ). ∀f:J ⟶ I+new-name(I). ∀g:K ⟶ J. ∀u:Point(dM(J)).
((p(a) J s ⋅ f u f(s(a)) g) = (p(a) K s ⋅ f ⋅ g (u f(s(a)) g)) ∈ c𝕌(g(f(s(a)))))
14. ((p(a) I+new-name(I) s ⋅ 1 0) = A(s(a)) ∈ c𝕌(s(a))) ∧ ((p(a) I+new-name(I) s ⋅ 1 1) = B(s(a)) ∈ c𝕌(s(a)))
15. (λK,g. (p(a) K h ⋅ s ⋅ g)) = p(s(h(a))) ∈ (J1:fset(ℕ) ⟶ f:J1 ⟶ J+new-name(J) ⟶ u:Point(dM(J1)) ⟶ c𝕌(f(h ⋅ s(a)))\000C)
16. ∀J1,K:fset(ℕ). ∀f:J1 ⟶ J+new-name(J). ∀g:K ⟶ J1. ∀u:Point(dM(J1)).
((p(a) J1 h ⋅ s ⋅ f u f(h ⋅ s(a)) g) = (p(a) K h ⋅ s ⋅ f ⋅ g (u f(h ⋅ s(a)) g)) ∈ c𝕌(g(f(h ⋅ s(a)))))
17. ((p(a) J+new-name(J) h ⋅ s ⋅ 1 0) = A(h ⋅ s(a)) ∈ c𝕌(h ⋅ s(a)))
∧ ((p(a) J+new-name(J) h ⋅ s ⋅ 1 1) = B(h ⋅ s(a)) ∈ c𝕌(h ⋅ s(a)))
⊢ ((snd((p(s(a)) I+new-name(I) 1 <new-name(I)>))) J new-name(J) h,new-name(I)=new-name(J) 0 ⋅
(compOp(A) J new-name(J) s(h(a)) 0 ⋅ u))
= ((snd((p J+new-name(J) s(h(a)) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 discr(⋅)
(compOp(A) J new-name(J) s(h(a)) 0 ⋅ u))
∈ decode(B)(h(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. J : fset(\mBbbN{})
9. h : J {}\mrightarrow{} I
10. u : decode(A)(h(a))
\mvdash{} ((snd((p(s(a)) I+new-name(I) 1 <new-name(I)>))) J new-name(J) h,new-name(I)=new-name(J) 0 \mcdot{}
(compOp(A) J new-name(J) s(h(a)) 0 \mcdot{} u))
= ((snd((p J+new-name(J) s(h(a)) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 discr(\mcdot{})
(compOp(A) J new-name(J) s(h(a)) 0 \mcdot{} u))
By
Latex:
((InstLemma `cubical-term-at-morph` [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(Path\_c\mBbbU{} A B)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstHyp [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}I+new-name(I)\mkleeneclose{}; s ] (-1)\mcdot{} THENA Auto)
THEN (RWO "path-type-ap-morph" (-1) THENA Auto)
THEN (Assert s(h(a)) = h \mcdot{} s(a) BY
Auto)
THEN (InstHyp [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}J+new-name(J)\mkleeneclose{}; \mkleeneopen{}h \mcdot{} s\mkleeneclose{} ] (-3)\mcdot{} THENA Auto)
THEN (RWO "path-type-ap-morph" (-1) THENA Auto)
THEN (ApFunToHypEquands `Z' \mkleeneopen{}p(Z)\mkleeneclose{} \mkleeneopen{}(Path\_c\mBbbU{} A B)(Z)\mkleeneclose{} (-2)\mcdot{}
THENA (Fold `member` 0
THEN ((InstLemma `cubical-term-at\_wf` [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(Path\_c\mBbbU{} A B)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
THENM BHyp -1
)
THENA Auto
)
)
)
THEN (ApFunToHypEquands `Z' \mkleeneopen{}(Path\_c\mBbbU{} A B)(Z)\mkleeneclose{} \mkleeneopen{}\mBbbU{}'\mkleeneclose{} (-3)\mcdot{}
THEN Try ((Eq
ORELSE (Fold `member` 0
THEN InstLemma `cubical-type-at\_wf` [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
THEN BHyp -1
THEN Auto)
))
)
THEN (Assert (\mlambda{}K,g. (p(a) K h \mcdot{} s \mcdot{} g)) = p(s(h(a))) BY
Eq)
THEN RepeatFor 4 (Thin (-2))
THEN (RWO "path-type-at" (-2) THENA Auto)
THEN (EqTypeHD (-2) THENA (D -1 THEN Auto))
THEN (EqTypeHD (-3) THENA (D -1 THEN Auto))
THEN (RWO "path-type-at" (-1) THENA Auto)
THEN (EqTypeHD (-1) THENA (D -1 THEN Auto))
THEN (EqTypeHD (-2) THENA (D -1 THEN Auto))
THEN All Reduce)
Home
Index