Proof of Nuprl Lemma : uabeta

Step * 1 of Lemma uabeta_wf

1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _:c𝕌}
3. [B] : {G ⊢ _:c𝕌}
4. G ⊢ decode(A)
5. (A)p ∈ {G.decode(A) ⊢ _:c𝕌}
6. G ⊢ decode(B)
7. (B)p ∈ {G.decode(A) ⊢ _:c𝕌}
8. G ⊢ Equiv(decode(A);decode(B))
9. G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p)
10. ∀[a,b:{G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}].
G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ (Path_((decode(B))p)p a b)
11. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p}
12. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)}
13. equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}
14. app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
15. CompFun((A)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(A))p)
16. CompFun((B)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(B))p)
17. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
18. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
⊢ uabeta(G;A;B) ∈ {G ⊢ _:ΠEquiv(decode(A);decode(B)) Π(decode(A))p (Path_((decode(B))p)p

                                                                         app(PathTransport(app(UA; (q)p)); q)

                                                                         app(equiv-fun((q)p); q))}

BY
{ ((InstLemmaIJ `univ-a_wf`
    [⌜G.Equiv(decode(A);decode(B)).(decode(A))p⌝;⌜((A)p)p⌝;⌜((B)p)p⌝]⋅
    THENA (Repeat (BLemma `cubical-universe-p`) THEN Auto)
    )

   THEN (Assert app(UA; (q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(Path_c𝕌 ((A)p)p ((B)p)p)} BY

               (InstLemma `cubical-app_wf_fun` [⌜parm{i|j}⌝;⌜parm{i'}⌝]⋅
                THEN BHyp -1
                THEN Try (Trivial)

                THEN Try (((RWW "csm-universe-decode" 0 THENA Auto) THEN RWW "csm-universe-decode" (-2) THEN Trivial))

                THEN MemCD
                THEN Repeat (BLemma `cubical-universe-p`)
                THEN Auto))
   THEN (InstLemmaIJ `path-trans_wf`

         [⌜G.Equiv(decode(A);decode(B)).(decode(A))p⌝;⌜((A)p)p⌝;⌜((B)p)p⌝; ⌜app(UA; (q)p)⌝]⋅

         THENA (Repeat (BLemma `cubical-universe-p`) THEN Auto)
         )
   THEN (All (RWW "csm-universe-decode<") THENA Auto)
   THEN (Assert app(PathTransport(app(UA; (q)p)); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _

                                                        :((decode(B))p)p} BY

               Auto)
   THEN Unfold `uabeta` 0
   THEN (RepeatFor 2 ((MemCD THENA Auto))

         THENL [Auto; (Assert q ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:(Equiv(decode(A);decode(B)))p} BY Auto)]

   )) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. G ⊢ decode(A)
5. (A)p ∈ {G.decode(A) ⊢ _:c𝕌}
6. G ⊢ decode(B)
7. (B)p ∈ {G.decode(A) ⊢ _:c𝕌}
8. G ⊢ Equiv(decode(A);decode(B))
9. G.decode(A) ⊢ Equiv((decode(A))p;(decode(B))p)
10. ∀[a,b:{G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}].
      G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ (Path_((decode(B))p)p a b)
11. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((Equiv(decode(A);decode(B)))p)p}
12. (q)p ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:Equiv(((decode(A))p)p;((decode(B))p)p)}
13. equiv-fun((q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}
14. app(equiv-fun((q)p); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
15. CompFun((A)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(A))p)
16. CompFun((B)p) ∈ G.Equiv(decode(A);decode(B)) +⊢ Compositon((decode(B))p)
17. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
18. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
19. UA ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _
          :(Equiv(((decode(A))p)p;((decode(B))p)p) ⟶ (Path_c𝕌 ((A)p)p ((B)p)p))}
20. app(UA; (q)p) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(Path_c𝕌 ((A)p)p ((B)p)p)}

21. PathTransport(app(UA; (q)p)) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(((decode(A))p)p ⟶ ((decode(B))p)p)}

22. app(PathTransport(app(UA; (q)p)); q) ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:((decode(B))p)p}
23. q ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:(Equiv(decode(A);decode(B)))p}
⊢ uabeta_aux(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)

  ∈ {G.Equiv(decode(A);decode(B)).(decode(A))p ⊢ _:(Path_((decode(B))p)p app(PathTransport(app(UA; (q)p)); q)

                                                         app(equiv-fun((q)p); q))}

Latex:

Latex:
1. [G] : CubicalSet\{j\} 2. [A] : \{G \mvdash{} \_:c\mBbbU{}\} 3. [B] : \{G \mvdash{} \_:c\mBbbU{}\} 4. G \mvdash{} decode(A) 5. (A)p \mmember{} \{G.decode(A) \mvdash{} \_:c\mBbbU{}\} 6. G \mvdash{} decode(B) 7. (B)p \mmember{} \{G.decode(A) \mvdash{} \_:c\mBbbU{}\} 8. G \mvdash{} Equiv(decode(A);decode(B)) 9. G.decode(A) \mvdash{} Equiv((decode(A))p;(decode(B))p) 10. \mforall{}[a,b:\{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:((decode(B))p)p\}]. G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} (Path\_((decode(B))p)p a b) 11. (q)p \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:((Equiv(decode(A);decode(B)))p)p\} 12. (q)p \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:Equiv(((decode(A))p)p;((decode(B))p)p)\} 13. equiv-fun((q)p) \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_ :(((decode(A))p)p {}\mrightarrow{} ((decode(B))p)p)\} 14. app(equiv-fun((q)p); q) \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_:((decode(B))p)p\} 15. CompFun((A)p) \mmember{} G.Equiv(decode(A);decode(B)) +\mvdash{} Compositon((decode(A))p) 16. CompFun((B)p) \mmember{} G.Equiv(decode(A);decode(B)) +\mvdash{} Compositon((decode(B))p) 17. (A)p \mmember{} \{G.Equiv(decode(A);decode(B)) \mvdash{} \_:c\mBbbU{}\} 18. (B)p \mmember{} \{G.Equiv(decode(A);decode(B)) \mvdash{} \_:c\mBbbU{}\} \mvdash{} uabeta(G;A;B) \mmember{} \{G \mvdash{} \_:\mPi{}Equiv(decode(A);decode(B)) \mPi{}(decode(A))p (Path\_((decode(B))p)p app(PathTransport(app(UA; (q)p)); q) app(equiv-fun((q)p); q))\} By Latex: ((InstLemmaIJ `univ-a\_wf` [\mkleeneopen{}G.Equiv(decode(A);decode(B)).(decode(A))p\mkleeneclose{};\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((B)p)p\mkleeneclose{}]\mcdot{} THENA (Repeat (BLemma `cubical-universe-p`) THEN Auto) ) THEN (Assert app(UA; (q)p) \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_ :(Path\_c\mBbbU{} ((A)p)p ((B)p)p)\} BY (InstLemma `cubical-app\_wf\_fun` [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{} THEN BHyp -1 THEN Try (Trivial) THEN Try (((RWW "csm-universe-decode" 0 THENA Auto) THEN RWW "csm-universe-decode" (-2) THEN Trivial)) THEN MemCD THEN Repeat (BLemma `cubical-universe-p`) THEN Auto)) THEN (InstLemmaIJ `path-trans\_wf` [\mkleeneopen{}G.Equiv(decode(A);decode(B)).(decode(A))p\mkleeneclose{};\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((B)p)p\mkleeneclose{}; \mkleeneopen{}app(UA; (q)p)\mkleeneclose{}]\mcdot{} THENA (Repeat (BLemma `cubical-universe-p`) THEN Auto) ) THEN (All (RWW "csm-universe-decode<") THENA Auto) THEN (Assert app(PathTransport(app(UA; (q)p)); q) \mmember{} \{G.Equiv(decode(A);decode(B)).(decode(A))p \mvdash{} \_ :((decode(B))p)p\} BY Auto) THEN Unfold `uabeta` 0 THEN (RepeatFor 2 ((MemCD THENA Auto)) THENL [Auto ; (Assert q \mmember{} \{G.Equiv(decode(A);decode(B)) \mvdash{} \_:(Equiv(decode(A);decode(B)))p\} BY Auto)] )) Home Index