Step
*
1
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))
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))
BY
{ (RepUR ``cubical-universe`` -6
THEN (ApFunToHypEquands `Z' ⌜Z I+new-name(I) 1 <new-name(I)>⌝ ⌜FibrantType(formal-cube(I+new-name(I)))⌝ (-6)⋅
THENA Auto
)
THEN Reduce -1
THEN RepUR ``cubical-universe`` -4
THEN (ApFunToHypEquands `Z' ⌜Z J+new-name(J) 1 <new-name(J)>⌝ ⌜FibrantType(formal-cube(J+new-name(J)))⌝ (-4)⋅
THENA Auto
)
THEN Reduce -1
THEN (Subst' p J+new-name(J) s(h(a)) ~ p(s(h(a))) 0 THENA (Unfold `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. 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)) ⟶ closed-type-to-type(cc𝕌)(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)) ⟶ closed-type-to-type(cc𝕌)(f(h ⋅ s(a))))
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)))
18. (p(a) I+new-name(I) s ⋅ 1 <new-name(I)>)
= (p(s(a)) I+new-name(I) 1 <new-name(I)>)
∈ FibrantType(formal-cube(I+new-name(I)))
19. (p(a) J+new-name(J) h ⋅ s ⋅ 1 <new-name(J)>)
= (p(s(h(a))) J+new-name(J) 1 <new-name(J)>)
∈ FibrantType(formal-cube(J+new-name(J)))
⊢ ((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(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))
11. \mforall{}[I:fset(\mBbbN{})]. \mforall{}[a:G(I)]. \mforall{}[J:fset(\mBbbN{})]. \mforall{}[f:J {}\mrightarrow{} I]. ((p(a) a f) = p(f(a)))
12. (\mlambda{}K,g. (p(a) K s \mcdot{} g)) = p(s(a))
13. \mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I+new-name(I). \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:Point(dM(J)).
((p(a) J s \mcdot{} f u f(s(a)) g) = (p(a) K s \mcdot{} f \mcdot{} g (u f(s(a)) g)))
14. ((p(a) I+new-name(I) s \mcdot{} 1 0) = A(s(a))) \mwedge{} ((p(a) I+new-name(I) s \mcdot{} 1 1) = B(s(a)))
15. (\mlambda{}K,g. (p(a) K h \mcdot{} s \mcdot{} g)) = p(s(h(a)))
16. \mforall{}J1,K:fset(\mBbbN{}). \mforall{}f:J1 {}\mrightarrow{} J+new-name(J). \mforall{}g:K {}\mrightarrow{} J1. \mforall{}u:Point(dM(J1)).
((p(a) J1 h \mcdot{} s \mcdot{} f u f(h \mcdot{} s(a)) g) = (p(a) K h \mcdot{} s \mcdot{} f \mcdot{} g (u f(h \mcdot{} s(a)) g)))
17. ((p(a) J+new-name(J) h \mcdot{} s \mcdot{} 1 0) = A(h \mcdot{} s(a)))
\mwedge{} ((p(a) J+new-name(J) h \mcdot{} s \mcdot{} 1 1) = B(h \mcdot{} s(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:
(RepUR ``cubical-universe`` -6
THEN (ApFunToHypEquands `Z' \mkleeneopen{}Z I+new-name(I) 1 <new-name(I)>\mkleeneclose{}
\mkleeneopen{}FibrantType(formal-cube(I+new-name(I)))\mkleeneclose{} (-6)\mcdot{}
THENA Auto
)
THEN Reduce -1
THEN RepUR ``cubical-universe`` -4
THEN (ApFunToHypEquands `Z' \mkleeneopen{}Z J+new-name(J) 1 <new-name(J)>\mkleeneclose{}
\mkleeneopen{}FibrantType(formal-cube(J+new-name(J)))\mkleeneclose{} (-4)\mcdot{}
THENA Auto
)
THEN Reduce -1
THEN (Subst' p J+new-name(J) s(h(a)) \msim{} p(s(h(a))) 0 THENA (Unfold `cubical-term-at` 0 THEN Auto)))
Home
Index