---

Step * of Lemma univ-trans-equiv_path

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].
  (univ-trans(G;equiv_path(G;A;B;f)) = trans-equiv-path(G;A;B;f) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))})
BY
{ (Intros⋅
   THEN Unhide
   THEN (Assert ⌜univ-trans(G;equiv_path(G;A;B;f)) = trans-equiv-path(G;A;B;f) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))}⌝⋅
   THENM (NthHypEqGen (-1) THEN EqCDA THEN Auto)
   )
   THEN (InstLemma `equiv-path2_wf` [⌜G⌝;⌜decode(A)⌝;⌜decode(B)⌝;⌜CompFun(A)⌝;⌜CompFun(B)⌝;⌜f⌝]⋅ THENA Auto)
   THEN RepUR ``univ-trans equiv_path let`` 0
   THEN (InstLemma `comp-fun-to-comp-op_wf` [⌜G.𝕀⌝;⌜equiv-path1(G;decode(A);decode(B);f)⌝;
         ⌜equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)⌝]⋅
         THENA Auto
         )
   THEN (InstLemma `universe-decode-encode` [⌜G.𝕀⌝;⌜equiv-path1(G;decode(A);decode(B);f)⌝;
         ⌜cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
              ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))⌝]⋅
         THENA Auto
         )
   THEN (InstLemma `universe-comp-op-encode` [⌜G.𝕀⌝;⌜equiv-path1(G;decode(A);decode(B);f)⌝;
         ⌜cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
              ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))⌝]⋅
         THENA Auto
         )
   THEN Assert 
   ⌜transprt-fun(G;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))
    = trans-equiv-path(G;A;B;f)
    ∈ {G ⊢ _:(decode(A) ⟶ decode(B))}⌝⋅) }

1
.....assertion..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f) ∈ G.𝕀 +⊢ Compositon(equiv-path1(G;decode(A);decode(B);f))
6. cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))
   ∈ G.𝕀 ⊢ CompOp(equiv-path1(G;decode(A);decode(B);f))
7. decode(encode(equiv-path1(G;decode(A);decode(B);f);cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                          ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))
= equiv-path1(G;decode(A);decode(B);f)
∈ {G.𝕀 ⊢ _}
8. compOp(encode(equiv-path1(G;decode(A);decode(B);f);cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                          ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))
= cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))
∈ G.𝕀 ⊢ CompOp(equiv-path1(G;decode(A);decode(B);f))
⊢ transprt-fun(G;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}

2
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f) ∈ G.𝕀 +⊢ Compositon(equiv-path1(G;decode(A);decode(B);f))
6. cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))
   ∈ G.𝕀 ⊢ CompOp(equiv-path1(G;decode(A);decode(B);f))
7. decode(encode(equiv-path1(G;decode(A);decode(B);f);cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                          ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))
= equiv-path1(G;decode(A);decode(B);f)
∈ {G.𝕀 ⊢ _}
8. compOp(encode(equiv-path1(G;decode(A);decode(B);f);cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                          ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))
= cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))
∈ G.𝕀 ⊢ CompOp(equiv-path1(G;decode(A);decode(B);f))
9. transprt-fun(G;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
⊢ transprt-fun(G;decode(encode(equiv-path1(G;decode(A);decode(B);f);
                               cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                   ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))));cop-to-cfun(
                                                                                                   compOp(encode(...;
                                                                                                                 ...))))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].
    (univ-trans(G;equiv\_path(G;A;B;f))  =  trans-equiv-path(G;A;B;f))


By

---

Latex:
(Intros\mcdot{}
  THEN  Unhide
  THEN  (Assert  \mkleeneopen{}univ-trans(G;equiv\_path(G;A;B;f))  =  trans-equiv-path(G;A;B;f)\mkleeneclose{}\mcdot{}
  THENM  (NthHypEqGen  (-1)  THEN  EqCDA  THEN  Auto)
  )
  THEN  (InstLemma  `equiv-path2\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}decode(A)\mkleeneclose{};\mkleeneopen{}decode(B)\mkleeneclose{};\mkleeneopen{}CompFun(A)\mkleeneclose{};\mkleeneopen{}CompFun(B)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RepUR  ``univ-trans  equiv\_path  let``  0
  THEN  (InstLemma  `comp-fun-to-comp-op\_wf`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}equiv-path1(G;decode(A);decode(B);f)\mkleeneclose{};
              \mkleeneopen{}equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (InstLemma  `universe-decode-encode`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}equiv-path1(G;decode(A);decode(B);f)\mkleeneclose{};
              \mkleeneopen{}cfun-to-cop(G.\mBbbI{};equiv-path1(G;decode(A);decode(B);f)
                        ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (InstLemma  `universe-comp-op-encode`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}equiv-path1(G;decode(A);decode(B);f)\mkleeneclose{};
              \mkleeneopen{}cfun-to-cop(G.\mBbbI{};equiv-path1(G;decode(A);decode(B);f)
                        ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Assert 
  \mkleeneopen{}transprt-fun(G;equiv-path1(G;decode(A);decode(B);f);equiv-path2(G;decode(A);decode(B);...;...;f))
    =  trans-equiv-path(G;A;B;f)\mkleeneclose{}\mcdot{})

---

Home Index