Step
*
1
of Lemma
universe-path-type-lemma-1
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)))
⊢ universe-type(B;I+new-name(I);v)((new-name(I)1) ⋅ f)
= fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) ⋅ f)
∈ Type
BY
{ ((InstHyp [⌜I+new-name(I)⌝;⌜J⌝;⌜1⌝;⌜(new-name(I)1) ⋅ f⌝;⌜<new-name(I)>⌝] (-2)⋅ THENA Auto)
THEN (ApFunToHypEquands `Z' ⌜fst(Z)⌝ ⌜{formal-cube(J) ⊢ _}⌝ (-1)⋅ THENA Auto)
THEN Unfold `pi1` -1
THEN (RW (SweepUpC (LiftC false)) (-1) THENA Auto)
THEN Reduce (-1)
THEN Fold `pi1` (-1)
THEN (ApFunToHypEquands `Z' ⌜Z(1)⌝ ⌜Type⌝ (-1)⋅ THENA (Auto THEN RepUR ``formal-cube`` 0 THEN Auto))
THEN (Subst' let A,cA = p(v) I+new-name(I) 1 <new-name(I)>
in (A)<(new-name(I)1) ⋅ f>(1) ~ fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) ⋅ f ⋅ 1) -1
THENA (((GenConclTerm ⌜p(v) I+new-name(I) 1 <new-name(I)>⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0⋅)
THEN (RWW "csm-ap-type-at csm-ap-context-map" 0 THENA Auto)
THEN RepUR ``formal-cube`` 0
THEN Auto)
)
THEN Symmetry
THEN NthHypEqGen (-1)
THEN EqCDA) }
1
.....subterm..... T:t
2: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
⊢ fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) ⋅ f)
= fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) ⋅ f ⋅ 1)
∈ Type
2
.....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
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. 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)
\mvdash{} universe-type(B;I+new-name(I);v)((new-name(I)1) \mcdot{} f)
= fst((p(v) I+new-name(I) 1 <new-name(I)>))((new-name(I)1) \mcdot{} f)
By
Latex:
((InstHyp [\mkleeneopen{}I+new-name(I)\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}(new-name(I)1) \mcdot{} f\mkleeneclose{};\mkleeneopen{}<new-name(I)>\mkleeneclose{}] (-2)\mcdot{} THENA Auto)
THEN (ApFunToHypEquands `Z' \mkleeneopen{}fst(Z)\mkleeneclose{} \mkleeneopen{}\{formal-cube(J) \mvdash{} \_\}\mkleeneclose{} (-1)\mcdot{} THENA Auto)
THEN Unfold `pi1` -1
THEN (RW (SweepUpC (LiftC false)) (-1) THENA Auto)
THEN Reduce (-1)
THEN Fold `pi1` (-1)
THEN (ApFunToHypEquands `Z' \mkleeneopen{}Z(1)\mkleeneclose{} \mkleeneopen{}Type\mkleeneclose{} (-1)\mcdot{}
THENA (Auto THEN RepUR ``formal-cube`` 0 THEN Auto)
)
THEN (Subst' let A,cA = p(v) I+new-name(I) 1 <new-name(I)>
in (A)<(new-name(I)1) \mcdot{} f>(1) \msim{} fst((p(v) I+new-name(I) 1
<new-name(I)>))((new-name(I)1) \mcdot{} f \mcdot{} 1) -1
THENA (((GenConclTerm \mkleeneopen{}p(v) I+new-name(I) 1 <new-name(I)>\mkleeneclose{}\mcdot{} THENA Auto)
THEN D -2
THEN Reduce
0\mcdot{})
THEN (RWW "csm-ap-type-at csm-ap-context-map" 0 THENA Auto)
THEN RepUR ``formal-cube`` 0
THEN Auto)
)
THEN Symmetry
THEN NthHypEqGen (-1)
THEN EqCDA)
Home
Index