Proof of Nuprl Lemma : transEquiv-trans-eq2

Step * 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))
⊢ ((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

{ ((InstLemma `cubical-term-at-morph` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝]⋅ THENA Auto)

   THEN (InstHyp [⌜I⌝;⌜a⌝;⌜I+new-name(I)⌝; s ] (-1)⋅ THENA Auto)
   THEN (RWO  "path-type-ap-morph" (-1) THENA Auto)
   THEN (Assert s(h(a)) = h ⋅ s(a) ∈ G(J+new-name(J)) BY
               Auto)
   THEN (InstHyp [⌜I⌝;⌜a⌝;⌜J+new-name(J)⌝; ⌜h ⋅ s⌝ ] (-3)⋅ THENA Auto)
   THEN (RWO  "path-type-ap-morph" (-1) THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜p(Z)⌝ ⌜(Path_c𝕌 A B)(Z)⌝ (-2)⋅
         THENA (Fold `member` 0

                THEN ((InstLemma `cubical-term-at_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝;⌜p⌝]⋅ THENM BHyp -1)

                      THENA Auto
                      )
                )
         )
   THEN (ApFunToHypEquands `Z' ⌜(Path_c𝕌 A B)(Z)⌝ ⌜𝕌'⌝ (-3)⋅
         THEN Try ((Eq
                   ORELSE (Fold `member` 0

                           THEN InstLemma `cubical-type-at_wf` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅

                           THEN BHyp -1
                           THEN Auto)
                   ))
         )
   THEN (Assert (λK,g. (p(a) K h ⋅ s ⋅ g)) = p(s(h(a))) ∈ (Path_c𝕌 A B)(h ⋅ s(a)) BY
               Eq)
   THEN RepeatFor 4 (Thin (-2))
   THEN (RWO "path-type-at" (-2) THENA Auto)
   THEN (EqTypeHD (-2) THENA (D -1 THEN Auto))
   THEN (EqTypeHD (-3) THENA (D -1 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 All Reduce) }

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)) ⟶ 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))

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)) \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: ((InstLemma `cubical-term-at-morph` [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(Path\_c\mBbbU{} A B)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{} THENA Auto) THEN (InstHyp [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}I+new-name(I)\mkleeneclose{}; s ] (-1)\mcdot{} THENA Auto) THEN (RWO "path-type-ap-morph" (-1) THENA Auto) THEN (Assert s(h(a)) = h \mcdot{} s(a) BY Auto) THEN (InstHyp [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}J+new-name(J)\mkleeneclose{}; \mkleeneopen{}h \mcdot{} s\mkleeneclose{} ] (-3)\mcdot{} THENA Auto) THEN (RWO "path-type-ap-morph" (-1) THENA Auto) THEN (ApFunToHypEquands `Z' \mkleeneopen{}p(Z)\mkleeneclose{} \mkleeneopen{}(Path\_c\mBbbU{} A B)(Z)\mkleeneclose{} (-2)\mcdot{} THENA (Fold `member` 0 THEN ((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{}]\mcdot{} THENM BHyp -1 ) THENA Auto ) ) ) THEN (ApFunToHypEquands `Z' \mkleeneopen{}(Path\_c\mBbbU{} A B)(Z)\mkleeneclose{} \mkleeneopen{}\mBbbU{}'\mkleeneclose{} (-3)\mcdot{} THEN Try ((Eq ORELSE (Fold `member` 0 THEN InstLemma `cubical-type-at\_wf` [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{} THEN BHyp -1 THEN Auto) )) ) THEN (Assert (\mlambda{}K,g. (p(a) K h \mcdot{} s \mcdot{} g)) = p(s(h(a))) BY Eq) THEN RepeatFor 4 (Thin (-2)) THEN (RWO "path-type-at" (-2) THENA Auto) THEN (EqTypeHD (-2) THENA (D -1 THEN Auto)) THEN (EqTypeHD (-3) THENA (D -1 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 All Reduce) Home Index