Step
*
1
2
of Lemma
universe-path-type-lemma-1
.....subterm..... T:t
3:n
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. v : G(I+new-name(I))
9. p(v) ∈ (Path_c𝕌 A B)(v)
10. p(v) ∈ J:fset(ℕ) ⟶ f:J ⟶ I+new-name(I) ⟶ u:Point(dM(J)) ⟶ FibrantType(formal-cube(J))
11. ∀J,K:fset(ℕ). ∀f:J ⟶ I+new-name(I). ∀g:K ⟶ J. ∀u:Point(dM(J)).
(let A,cA = p(v) J f u in <(A)<g>, (cA)<g>> = (p(v) K f ⋅ g (u f(v) g)) ∈ FibrantType(formal-cube(K)))
12. (p(v) I+new-name(I) 1 1) = B(v) ∈ FibrantType(formal-cube(I+new-name(I)))
13. let A,cA = p(v) I+new-name(I) 1 <new-name(I)>
in <(A)<(new-name(I)1) ⋅ f>, (cA)<(new-name(I)1) ⋅ f>>
= (p(v) J 1 ⋅ (new-name(I)1) ⋅ f (<new-name(I)> 1(v) (new-name(I)1) ⋅ f))
∈ FibrantType(formal-cube(J))
14. let A,cA = p(v) I+new-name(I) 1 <new-name(I)>
in (A)<(new-name(I)1) ⋅ f>
= (fst((p(v) J 1 ⋅ (new-name(I)1) ⋅ f (<new-name(I)> 1(v) (new-name(I)1) ⋅ f))))
∈ {formal-cube(J) ⊢ _}
15. fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) ⋅ f ⋅ 1)
= fst((p(v) J 1 ⋅ (new-name(I)1) ⋅ f (<new-name(I)> 1(v) (new-name(I)1) ⋅ f)))(1)
∈ Type
⊢ universe-type(B;I+new-name(I);v)((new-name(I)1) ⋅ f)
= fst((p(v) J 1 ⋅ (new-name(I)1) ⋅ f (<new-name(I)> 1(v) (new-name(I)1) ⋅ f)))(1)
∈ Type
BY
{ ((RepeatFor 3 (Thin (-1))
THEN (ApFunToHypEquands `Z' ⌜fst(Z)((new-name(I)1) ⋅ f)⌝ ⌜Type⌝ (-1)⋅
THENA (((D -1 THEN Reduce 0) THEN Auto) THEN RepUR ``formal-cube`` 0 THEN Auto)
)
)
THEN Fold `universe-type` (-1)
THEN NthHypEqTrans (-1)) }
1
.....assertion.....
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. p : {G ⊢ _:(Path_c𝕌 A B)}
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. v : G(I+new-name(I))
9. p(v) ∈ (Path_c𝕌 A B)(v)
10. p(v) ∈ J:fset(ℕ) ⟶ f:J ⟶ I+new-name(I) ⟶ u:Point(dM(J)) ⟶ FibrantType(formal-cube(J))
11. ∀J,K:fset(ℕ). ∀f:J ⟶ I+new-name(I). ∀g:K ⟶ J. ∀u:Point(dM(J)).
(let A,cA = p(v) J f u in <(A)<g>, (cA)<g>> = (p(v) K f ⋅ g (u f(v) g)) ∈ FibrantType(formal-cube(K)))
12. (p(v) I+new-name(I) 1 1) = B(v) ∈ FibrantType(formal-cube(I+new-name(I)))
13. fst((p(v) I+new-name(I) 1 1))((new-name(I)1) ⋅ f) = universe-type(B;I+new-name(I);v)((new-name(I)1) ⋅ f) ∈ Type
⊢ fst((p(v) I+new-name(I) 1 1))((new-name(I)1) ⋅ f)
= fst((p(v) J 1 ⋅ (new-name(I)1) ⋅ f (<new-name(I)> 1(v) (new-name(I)1) ⋅ f)))(1)
∈ Type
Latex:
Latex:
.....subterm..... T:t
3:n
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. I : fset(\mBbbN{})
6. J : fset(\mBbbN{})
7. f : J {}\mrightarrow{} I
8. v : G(I+new-name(I))
9. p(v) \mmember{} (Path\_c\mBbbU{} A B)(v)
10. p(v) \mmember{} J:fset(\mBbbN{}) {}\mrightarrow{} f:J {}\mrightarrow{} I+new-name(I) {}\mrightarrow{} u:Point(dM(J)) {}\mrightarrow{} FibrantType(formal-cube(J))
11. \mforall{}J,K:fset(\mBbbN{}). \mforall{}f:J {}\mrightarrow{} I+new-name(I). \mforall{}g:K {}\mrightarrow{} J. \mforall{}u:Point(dM(J)).
(let A,cA = p(v) J f u in <(A)<g>, (cA)<g>> = (p(v) K f \mcdot{} g (u f(v) g)))
12. (p(v) I+new-name(I) 1 1) = B(v)
13. let A,cA = p(v) I+new-name(I) 1 <new-name(I)>
in <(A)<(new-name(I)1) \mcdot{} f>, (cA)<(new-name(I)1) \mcdot{} f>>
= (p(v) J 1 \mcdot{} (new-name(I)1) \mcdot{} f (<new-name(I)> 1(v) (new-name(I)1) \mcdot{} f))
14. let A,cA = p(v) I+new-name(I) 1 <new-name(I)>
in (A)<(new-name(I)1) \mcdot{} f>
= (fst((p(v) J 1 \mcdot{} (new-name(I)1) \mcdot{} f (<new-name(I)> 1(v) (new-name(I)1) \mcdot{} f))))
15. fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) \mcdot{} f \mcdot{} 1)
= fst((p(v) J 1 \mcdot{} (new-name(I)1) \mcdot{} f (<new-name(I)> 1(v) (new-name(I)1) \mcdot{} f)))(1)
\mvdash{} universe-type(B;I+new-name(I);v)((new-name(I)1) \mcdot{} f)
= fst((p(v) J 1 \mcdot{} (new-name(I)1) \mcdot{} f (<new-name(I)> 1(v) (new-name(I)1) \mcdot{} f)))(1)
By
Latex:
((RepeatFor 3 (Thin (-1))
THEN (ApFunToHypEquands `Z' \mkleeneopen{}fst(Z)((new-name(I)1) \mcdot{} f)\mkleeneclose{} \mkleeneopen{}Type\mkleeneclose{} (-1)\mcdot{}
THENA (((D -1 THEN Reduce 0) THEN Auto) THEN RepUR ``formal-cube`` 0 THEN Auto)
)
)
THEN Fold `universe-type` (-1)
THEN NthHypEqTrans (-1))
Home
Index