---

Step * 1 1 of Lemma app-univ-a


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. app(UA; f) = (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f] ∈ {G ⊢ _:(Path_c𝕌 A B)}
6. EquivPath(G;A;B;f) ∈ {G ⊢ _:Path(c𝕌)}
7. G ⊢ Equiv(decode(A);decode(B))
8. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
9. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
10. ∀[f:{G.Equiv(decode(A);decode(B)) ⊢ _:Equiv(decode((A)p);decode((A)p))}]
      (equiv_path(G.Equiv(decode(A);decode(B));(A)p;(A)p;f) ∈ {G.Equiv(decode(A);decode(B)).𝕀 ⊢ _:c𝕌})
11. ∀[b:{G.Equiv(decode(A);decode(B)).𝕀 ⊢ _:(c𝕌)p}]. ∀[H:ij⊢]. ∀[s:H ij⟶ G.Equiv(decode(A);decode(B))].
      ((cubical-lam(G.Equiv(decode(A);decode(B));b))s = cubical-lam(H;(b)s+) ∈ {H ⊢ _:((𝕀 ⟶ c𝕌))s})
⊢ ((λequiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f] = (λequiv_path(G;A;B;f)) ∈ {G ⊢ _:Path(c𝕌)}
BY
{ D -1 With ⌜equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)⌝  }

1
.....wf..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. app(UA; f) = (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f] ∈ {G ⊢ _:(Path_c𝕌 A B)}
6. EquivPath(G;A;B;f) ∈ {G ⊢ _:Path(c𝕌)}
7. G ⊢ Equiv(decode(A);decode(B))
8. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
9. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
10. ∀[f:{G.Equiv(decode(A);decode(B)) ⊢ _:Equiv(decode((A)p);decode((A)p))}]
      (equiv_path(G.Equiv(decode(A);decode(B));(A)p;(A)p;f) ∈ {G.Equiv(decode(A);decode(B)).𝕀 ⊢ _:c𝕌})
⊢ equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q) ∈ {G.Equiv(decode(A);decode(B)).𝕀 ⊢ _:(c𝕌)p}

2
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. app(UA; f) = (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f] ∈ {G ⊢ _:(Path_c𝕌 A B)}
6. EquivPath(G;A;B;f) ∈ {G ⊢ _:Path(c𝕌)}
7. G ⊢ Equiv(decode(A);decode(B))
8. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
9. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
10. ∀[f:{G.Equiv(decode(A);decode(B)) ⊢ _:Equiv(decode((A)p);decode((A)p))}]
      (equiv_path(G.Equiv(decode(A);decode(B));(A)p;(A)p;f) ∈ {G.Equiv(decode(A);decode(B)).𝕀 ⊢ _:c𝕌})
11. ∀[H:ij⊢]. ∀[s:H ij⟶ G.Equiv(decode(A);decode(B))].
      ((cubical-lam(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))s
      = cubical-lam(H;(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))s+)
      ∈ {H ⊢ _:((𝕀 ⟶ c𝕌))s})
⊢ ((λequiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f] = (λequiv_path(G;A;B;f)) ∈ {G ⊢ _:Path(c𝕌)}

---

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.  app(UA;  f)  =  (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]
6.  EquivPath(G;A;B;f)  \mmember{}  \{G  \mvdash{}  \_:Path(c\mBbbU{})\}
7.  G  \mvdash{}  Equiv(decode(A);decode(B))
8.  (A)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
9.  (B)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
10.  \mforall{}[f:\{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:Equiv(decode((A)p);decode((A)p))\}]
            (equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(A)p;f)
              \mmember{}  \{G.Equiv(decode(A);decode(B)).\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\})
11.  \mforall{}[b:\{G.Equiv(decode(A);decode(B)).\mBbbI{}  \mvdash{}  \_:(c\mBbbU{})p\}].  \mforall{}[H:ij\mvdash{}].
        \mforall{}[s:H  ij{}\mrightarrow{}  G.Equiv(decode(A);decode(B))].
            ((cubical-lam(G.Equiv(decode(A);decode(B));b))s  =  cubical-lam(H;(b)s+))
\mvdash{}  ((\mlambda{}equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f]  =  (\mlambda{}equiv\_path(G;A;B;f))


By

---

Latex:
D  -1  With  \mkleeneopen{}equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)\mkleeneclose{} 

---

Home Index