---

Step * 1 2 1 1 2 of Lemma univ-trans-equiv_path


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. (λtransprt(G.decode(A);(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
8. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] = decode(A) ∈ {G ⊢ _}
9. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)]
= decode(A)
∈ {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
10. Z : {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
11. {G.Z ⊢ _:((equiv-path1(G;decode(A);decode(B);f))p+)[1(𝕀)]} = {G.decode(A) ⊢ _:(decode(B))p} ∈ 𝕌{[i | [j | i]']}
⊢ transprt(G.Z;(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q)
  ∈ {G.Z ⊢ _:((equiv-path1(G;decode(A);decode(B);f))p+)[1(𝕀)]}
BY
{ MemCD }

1
.....subterm..... T:t
1:n
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. (λtransprt(G.decode(A);(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
8. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] = decode(A) ∈ {G ⊢ _}
9. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)]
= decode(A)
∈ {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
10. Z : {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
11. {G.Z ⊢ _:((equiv-path1(G;decode(A);decode(B);f))p+)[1(𝕀)]} = {G.decode(A) ⊢ _:(decode(B))p} ∈ 𝕌{[i | [j | i]']}
⊢ G.Z cubical_set{[j | i]:l}

2
.....implicit subterm..... 
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. (λtransprt(G.decode(A);(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
8. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] = decode(A) ∈ {G ⊢ _}
9. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)]
= decode(A)
∈ {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
10. Z : {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
11. {G.Z ⊢ _:((equiv-path1(G;decode(A);decode(B);f))p+)[1(𝕀)]} = {G.decode(A) ⊢ _:(decode(B))p} ∈ 𝕌{[i | [j | i]']}
⊢ G.Z.𝕀 ⊢ (equiv-path1(G;decode(A);decode(B);f))p+

3
.....subterm..... T:t
2:n
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. (λtransprt(G.decode(A);(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
8. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] = decode(A) ∈ {G ⊢ _}
9. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)]
= decode(A)
∈ {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
10. Z : {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
11. {G.Z ⊢ _:((equiv-path1(G;decode(A);decode(B);f))p+)[1(𝕀)]} = {G.decode(A) ⊢ _:(decode(B))p} ∈ 𝕌{[i | [j | i]']}
⊢ (equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+
  ∈ composition-structure{[j | i]:l, i:l}(G.Z.𝕀; (equiv-path1(G;decode(A);decode(B);f))p+)

4
.....subterm..... T:t
3:n
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. (λtransprt(G.decode(A);(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q))
= trans-equiv-path(G;A;B;f)
∈ {G ⊢ _:(decode(A) ⟶ decode(B))}
8. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] = decode(A) ∈ {G ⊢ _}
9. (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)]
= decode(A)
∈ {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
10. Z : {z:{G ⊢ _}| (z = (equiv-path1(G;decode(A);decode(B);f))[0(𝕀)] ∈ {G ⊢ _}) ∧ (z = decode(A) ∈ {G ⊢ _})} 
11. {G.Z ⊢ _:((equiv-path1(G;decode(A);decode(B);f))p+)[1(𝕀)]} = {G.decode(A) ⊢ _:(decode(B))p} ∈ 𝕌{[i | [j | i]']}
⊢ q ∈ {G.Z ⊢ _:((equiv-path1(G;decode(A);decode(B);f))p+)[0(𝕀)]}

---

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.  equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)
      \mmember{}  G.\mBbbI{}  +\mvdash{}  Compositon(equiv-path1(G;decode(A);decode(B);f))
6.  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))
      \mmember{}  G.\mBbbI{}  \mvdash{}  CompOp(equiv-path1(G;decode(A);decode(B);f))
7.  (\mlambda{}transprt(G.decode(A);(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q))
=  trans-equiv-path(G;A;B;f)
8.  (equiv-path1(G;decode(A);decode(B);f))[0(\mBbbI{})]  =  decode(A)
9.  (equiv-path1(G;decode(A);decode(B);f))[0(\mBbbI{})]  =  decode(A)
10.  Z  :  \{z:\{G  \mvdash{}  \_\}|  (z  =  (equiv-path1(G;decode(A);decode(B);f))[0(\mBbbI{})])  \mwedge{}  (z  =  decode(A))\} 
11.  \{G.Z  \mvdash{}  \_:((equiv-path1(G;decode(A);decode(B);f))p+)[1(\mBbbI{})]\}  =  \{G.decode(A)  \mvdash{}  \_:(decode(B))p\}
\mvdash{}  transprt(G.Z;(equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))p+;q)
    \mmember{}  \{G.Z  \mvdash{}  \_:((equiv-path1(G;decode(A);decode(B);f))p+)[1(\mBbbI{})]\}


By

---

Latex:
MemCD

---

Home Index