---

Step * 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))
⊢ ((snd((p J+new-name(J) 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 ⋅ u))
= ((snd((p J+new-name(J) 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
{ ((Assert s(h(a)) = s(1(h(a))) ∈ G(J+new-name(J)) BY
          Auto)
   THEN (ApFunToHypEquands `Z' ⌜p(Z)⌝ ⌜(Path_c𝕌 A B)(Z)⌝ (-1)⋅
         THENA (InstLemma `cubical-term-at_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝;⌜J+new-name(J)⌝;⌜Z⌝]⋅
                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 (Subst' p J+new-name(J) s(1(h(a))) ~ p(s(1(h(a)))) 0 THENA (CsmUnfolding THEN Auto))
   THEN (Subst' p J+new-name(J) s(h(a)) ~ p(s(h(a))) 0 THENA (CsmUnfolding THEN Auto))
   THEN (ApFunToHypEquands `Z' ⌜Z J+new-name(J) 1 <new-name(J)>⌝ ⌜FibrantType(formal-cube(J+new-name(J)))⌝ (-3)⋅
         THENA (RepUR ``cubical-universe`` -1 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,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))

---

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))
\mvdash{}  ((snd((p  J+new-name(J)  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  J+new-name(J)  s(1(h(a)))  J+new-name(J)  1  <new-name(J)>)))  J  new-name(J)  1  0  (\mlambda{}I,alpha.  \mcdot{})\000C 
      (compOp(A)  J  new-name(J)  s(1(h(a)))  0  (\mlambda{}I@0,a@0.  \mcdot{})  u))


By

---

Latex:
((Assert  s(h(a))  =  s(1(h(a)))  BY
                Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}p(Z)\mkleeneclose{}  \mkleeneopen{}(Path\_c\mBbbU{}  A  B)(Z)\mkleeneclose{}  (-1)\mcdot{}
              THENA  (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{};
                            \mkleeneopen{}J+new-name(J)\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{}
                            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  (Subst'  p  J+new-name(J)  s(1(h(a)))  \msim{}  p(s(1(h(a))))  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (Subst'  p  J+new-name(J)  s(h(a))  \msim{}  p(s(h(a)))  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  J+new-name(J)  1  <new-name(J)>\mkleeneclose{} 
              \mkleeneopen{}FibrantType(formal-cube(J+new-name(J)))\mkleeneclose{}  (-3)\mcdot{}
              THENA  (RepUR  ``cubical-universe``  -1  THEN  Auto)
              ))

---

Home Index