---

Step * 1 1 2 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. ∀[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})
12. (cubical-lam(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f]
= cubical-lam(G;(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]+)
∈ {G ⊢ _:((𝕀 ⟶ c𝕌))[f]}
⊢ (cubical-lam(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f]
= cubical-lam(G;equiv_path(G;A;B;f))
∈ {G ⊢ _:Path(c𝕌)}
BY
{ Fold `pathtype` (-1) }

1
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})
12. (cubical-lam(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f]
= cubical-lam(G;(equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]+)
∈ {G ⊢ _:(Path(c𝕌))[f]}
⊢ (cubical-lam(G.Equiv(decode(A);decode(B));equiv_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)))[f]
= cubical-lam(G;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{}[H:ij\mvdash{}].  \mforall{}[s:H  ij{}\mrightarrow{}  G.Equiv(decode(A);decode(B))].
            ((cubical-lam(G.Equiv(decode(A);decode(B));equiv\_path(G.Equiv(decode(A);...);(A)p;(B)p;q)))s
            =  cubical-lam(H;(equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))s+))
12.  (cubical-lam(G.Equiv(decode(A);decode(B));equiv\_path(G.Equiv(decode(A);...);(A)p;(B)p;q)))[f]
=  cubical-lam(G;(equiv\_path(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]+)
\mvdash{}  (cubical-lam(G.Equiv(decode(A);decode(B));equiv\_path(G.Equiv(decode(A);decode(B));(A)p;...;q)))[f]
=  cubical-lam(G;equiv\_path(G;A;B;f))


By

---

Latex:
Fold  `pathtype`  (-1)

---

Home Index