---

Step * 1 of Lemma csm-trans-equiv-path


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. (A)s ∈ {H ⊢ _:c𝕌}
8. (B)s ∈ {H ⊢ _:c𝕌}
9. G ⊢ Equiv(decode(A);decode(B))
10. G ⊢ decode(A)
11. G ⊢ decode(B)
12. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
13. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
⊢ (let tr = λb.transprt-const(G.decode(A);(CompFun(B))p;b) in
    let b = app(equiv-fun((f)p); q) in
    cubical-lam(G;tr (tr b)))s
= let tr = λb.transprt-const(H.decode((A)s);(CompFun((B)s))p;b) in
   let b = app(equiv-fun(((f)s)p); q) in
   cubical-lam(H;tr (tr b))
∈ {H ⊢ _:(decode((A)s) ⟶ decode((B)s))}
BY
{ (RepUR ``let`` 0
   THEN ((Assert G.decode(A) ⊢ (decode(B))p BY
                Auto)
         THEN (Assert (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}
                                        (G.decode(A); (decode(B))p) BY
                     (SubsumeC ⌜composition-structure{[[i | j] | [j | i]]:l, i:l}(G.decode(A); (decode(B))p)⌝⋅
                      THEN Auto
                      THEN MemCD
                      THEN Auto))
         )
   THEN (InstLemmaIJ `csm-cubical-lam` [⌜G⌝;⌜decode(A)⌝;⌜decode(B)⌝;
         ⌜transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p); q)))⌝;
         ⌜H⌝;⌜s⌝]⋅
         THENA Try (Complete (Auto))
         )) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. (A)s ∈ {H ⊢ _:c𝕌}
8. (B)s ∈ {H ⊢ _:c𝕌}
9. G ⊢ Equiv(decode(A);decode(B))
10. G ⊢ decode(A)
11. G ⊢ decode(B)
12. (f)p ∈ {G.decode(A) ⊢ _:Equiv((decode(A))p;(decode(B))p)}
13. q ∈ {G.decode(A) ⊢ _:(decode(A))p}
14. G.decode(A) ⊢ (decode(B))p
15. (CompFun(B))p ∈ composition-structure{[[i | j] | [j | i]]:l, [i | j]:l}(G.decode(A); (decode(B))p)
16. (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun(...);
                                                                                                         q)))))s
= cubical-lam(H;(transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
                                                                                                       q))))s+)
∈ {H ⊢ _:((decode(A) ⟶ decode(B)))s}
⊢ (cubical-lam(G;transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(equiv-fun((f)p);
                                                                                                       q)))))s
= cubical-lam(H;transprt-const(H.decode((A)s);(CompFun((B)s))p;transprt-const(H.decode((A)s);(CompFun((B)s))p;app(...;
                                                                                                                  q))))
∈ {H ⊢ _:(decode((A)s) ⟶ decode((B)s))}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
3.  B  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
4.  f  :  \{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}
5.  H  :  CubicalSet\{j\}
6.  s  :  H  j{}\mrightarrow{}  G
7.  (A)s  \mmember{}  \{H  \mvdash{}  \_:c\mBbbU{}\}
8.  (B)s  \mmember{}  \{H  \mvdash{}  \_:c\mBbbU{}\}
9.  G  \mvdash{}  Equiv(decode(A);decode(B))
10.  G  \mvdash{}  decode(A)
11.  G  \mvdash{}  decode(B)
12.  (f)p  \mmember{}  \{G.decode(A)  \mvdash{}  \_:Equiv((decode(A))p;(decode(B))p)\}
13.  q  \mmember{}  \{G.decode(A)  \mvdash{}  \_:(decode(A))p\}
\mvdash{}  (let  tr  =  \mlambda{}b.transprt-const(G.decode(A);(CompFun(B))p;b)  in
        let  b  =  app(equiv-fun((f)p);  q)  in
        cubical-lam(G;tr  (tr  b)))s
=  let  tr  =  \mlambda{}b.transprt-const(H.decode((A)s);(CompFun((B)s))p;b)  in
      let  b  =  app(equiv-fun(((f)s)p);  q)  in
      cubical-lam(H;tr  (tr  b))


By

---

Latex:
(RepUR  ``let``  0
  THEN  ((Assert  G.decode(A)  \mvdash{}  (decode(B))p  BY
                            Auto)
              THEN  (Assert  (CompFun(B))p  \mmember{}  composition-structure\{[[i  |  j]  |  [j  |  i]]:l,  [i  |  j]:l\}
                                                                            (G.decode(A);  (decode(B))p)  BY
                                      (SubsumeC  \mkleeneopen{}composition-structure\{[[i  |  j]  |  [j  |  i]]:l,  i:l\}(G.decode(A);
                                                                                                                                                                (decode(B))p)\mkleeneclose{}\mcdot{}
                                        THEN  Auto
                                        THEN  MemCD
                                        THEN  Auto))
              )
  THEN  (InstLemmaIJ  `csm-cubical-lam`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}decode(A)\mkleeneclose{};\mkleeneopen{}decode(B)\mkleeneclose{};
              \mkleeneopen{}transprt-const(G.decode(A);(CompFun(B))p;transprt-const(G.decode(A);(CompFun(B))p;app(...;
                                                                                                                                                                                            q)))\mkleeneclose{};
              \mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
              THENA  Try  (Complete  (Auto))
              ))

---

Home Index