Step
*
1
1
of Lemma
transEquiv-trans-eq-path-trans
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,a,J,h,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)) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
7. I : fset(ℕ)
8. a : G(I)
9. J : fset(ℕ)
10. h : J ⟶ I
11. u : decode(A)(h(a))
12. s(h(a)) = s(1(h(a))) ∈ G(J+new-name(J))
13. p(s(h(a))) = p(s(1(h(a)))) ∈ (J1:fset(ℕ) ⟶ f:J1 ⟶ J+new-name(J) ⟶ u:Point(dM(J1)) ⟶ c𝕌(f(s(h(a)))))
14. ∀J1,K:fset(ℕ). ∀f:J1 ⟶ J+new-name(J). ∀g:K ⟶ J1. ∀u:Point(dM(J1)).
((p(s(h(a))) J1 f u f(s(h(a))) g) = (p(s(h(a))) K f ⋅ g (u f(s(h(a))) g)) ∈ c𝕌(g(f(s(h(a))))))
15. ((p(s(h(a))) J+new-name(J) 1 0) = A(s(h(a))) ∈ c𝕌(s(h(a))))
∧ ((p(s(h(a))) J+new-name(J) 1 1) = B(s(h(a))) ∈ c𝕌(s(h(a))))
16. (p(s(h(a))) J+new-name(J) 1 <new-name(J)>)
= (p(s(1(h(a)))) J+new-name(J) 1 <new-name(J)>)
∈ FibrantType(formal-cube(J+new-name(J)))
⊢ ((snd((p(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (λI,alpha. ⋅) (compOp(A) J new-name(J) s(h(a)) 0 \000C⋅ u))
= ((snd((p(s(1(h(a)))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (λI,alpha. ⋅)
(compOp(A) J new-name(J) s(1(h(a))) 0 (λI@0,a@0. ⋅) u))
∈ decode(B)(h(a))
BY
{ (ApFunToHypEquands `Z' ⌜snd(Z)⌝ ⌜formal-cube(J+new-name(J)) ⊢ CompOp(fst(Z))⌝ (-1)⋅ THENA 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,a,J,h,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)) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
7. I : fset(ℕ)
8. a : G(I)
9. J : fset(ℕ)
10. h : J ⟶ I
11. u : decode(A)(h(a))
12. s(h(a)) = s(1(h(a))) ∈ G(J+new-name(J))
13. p(s(h(a))) = p(s(1(h(a)))) ∈ (J1:fset(ℕ) ⟶ f:J1 ⟶ J+new-name(J) ⟶ u:Point(dM(J1)) ⟶ c𝕌(f(s(h(a)))))
14. ∀J1,K:fset(ℕ). ∀f:J1 ⟶ J+new-name(J). ∀g:K ⟶ J1. ∀u:Point(dM(J1)).
((p(s(h(a))) J1 f u f(s(h(a))) g) = (p(s(h(a))) K f ⋅ g (u f(s(h(a))) g)) ∈ c𝕌(g(f(s(h(a))))))
15. ((p(s(h(a))) J+new-name(J) 1 0) = A(s(h(a))) ∈ c𝕌(s(h(a))))
∧ ((p(s(h(a))) J+new-name(J) 1 1) = B(s(h(a))) ∈ c𝕌(s(h(a))))
16. (p(s(h(a))) J+new-name(J) 1 <new-name(J)>)
= (p(s(1(h(a)))) J+new-name(J) 1 <new-name(J)>)
∈ FibrantType(formal-cube(J+new-name(J)))
17. (snd((p(s(h(a))) J+new-name(J) 1 <new-name(J)>)))
= (snd((p(s(1(h(a)))) J+new-name(J) 1 <new-name(J)>)))
∈ formal-cube(J+new-name(J)) ⊢ CompOp(fst((p(s(h(a))) J+new-name(J) 1 <new-name(J)>)))
⊢ ((snd((p(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (λI,alpha. ⋅) (compOp(A) J new-name(J) s(h(a)) 0 \000C⋅ u))
= ((snd((p(s(1(h(a)))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (λI,alpha. ⋅)
(compOp(A) J new-name(J) s(1(h(a))) 0 (λI@0,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. \mlambda{}I,a,J,h,u. ((snd((p(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)) \mmember{} \{G \mvdash{} \_:(decode(A) {}\mrightarrow{} decode(B))\}
7. I : fset(\mBbbN{})
8. a : G(I)
9. J : fset(\mBbbN{})
10. h : J {}\mrightarrow{} I
11. u : decode(A)(h(a))
12. s(h(a)) = s(1(h(a)))
13. p(s(h(a))) = p(s(1(h(a))))
14. \mforall{}J1,K:fset(\mBbbN{}). \mforall{}f:J1 {}\mrightarrow{} J+new-name(J). \mforall{}g:K {}\mrightarrow{} J1. \mforall{}u:Point(dM(J1)).
((p(s(h(a))) J1 f u f(s(h(a))) g) = (p(s(h(a))) K f \mcdot{} g (u f(s(h(a))) g)))
15. ((p(s(h(a))) J+new-name(J) 1 0) = A(s(h(a)))) \mwedge{} ((p(s(h(a))) J+new-name(J) 1 1) = B(s(h(a))))
16. (p(s(h(a))) J+new-name(J) 1 <new-name(J)>) = (p(s(1(h(a)))) J+new-name(J) 1 <new-name(J)>)
\mvdash{} ((snd((p(s(h(a))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (\mlambda{}I,alpha. \mcdot{})
(compOp(A) J new-name(J) s(h(a)) 0 \mcdot{} u))
= ((snd((p(s(1(h(a)))) J+new-name(J) 1 <new-name(J)>))) J new-name(J) 1 0 (\mlambda{}I,alpha. \mcdot{})
(compOp(A) J new-name(J) s(1(h(a))) 0 (\mlambda{}I@0,a@0. \mcdot{}) u))
By
Latex:
(ApFunToHypEquands `Z' \mkleeneopen{}snd(Z)\mkleeneclose{} \mkleeneopen{}formal-cube(J+new-name(J)) \mvdash{} CompOp(fst(Z))\mkleeneclose{} (-1)\mcdot{} THENA Auto)
Home
Index