---

Step * 1 1 of Lemma app-univ-a-1


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. G ⊢ Equiv(decode(A);decode(B))
6. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
7. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
8. ∀[X:ij⊢]. ∀[A,B:{X ⊢' _}]. ∀[b:{X.A ⊢ _:(B)p}].  ((λb) ∈ {X ⊢ _:(A ⟶ B)})
9. EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q) ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}
10. ∀[B@0:{G.Equiv(decode(A);decode(B)) ⊢' _}]. ∀[b:{G.Equiv(decode(A);decode(B)) ⊢ _:B@0}].
    ∀[u:{G ⊢ _:Equiv(decode(A);decode(B))}].
      (app((λb); u) = (b)[u] ∈ {G ⊢ _:(B@0)[u]})
⊢ app((λEquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)); f)
= (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]
∈ {G ⊢ _:(Path_c𝕌 A B)}
BY
{ ((D -1 With ⌜(Path_c𝕌 (A)p (B)p)⌝  THENA (MemCD THEN Auto))
   THEN (D -1 With ⌜EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)⌝  THENA Auto)
   THEN (D -1 With ⌜f⌝  THENA Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. G ⊢ Equiv(decode(A);decode(B))
6. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
7. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
8. ∀[X:ij⊢]. ∀[A,B:{X ⊢' _}]. ∀[b:{X.A ⊢ _:(B)p}].  ((λb) ∈ {X ⊢ _:(A ⟶ B)})
9. EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q) ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}
10. app((λEquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)); f)
= (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]
∈ {G ⊢ _:((Path_c𝕌 (A)p (B)p))[f]}
⊢ app((λEquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)); f)
= (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]
∈ {G ⊢ _:(Path_c𝕌 A B)}

---

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.  G  \mvdash{}  Equiv(decode(A);decode(B))
6.  (A)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
7.  (B)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
8.  \mforall{}[X:ij\mvdash{}].  \mforall{}[A,B:\{X  \mvdash{}'  \_\}].  \mforall{}[b:\{X.A  \mvdash{}  \_:(B)p\}].    ((\mlambda{}b)  \mmember{}  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\})
9.  EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)
      \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:(Path\_c\mBbbU{}  (A)p  (B)p)\}
10.  \mforall{}[B@0:\{G.Equiv(decode(A);decode(B))  \mvdash{}'  \_\}].  \mforall{}[b:\{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:B@0\}].
        \mforall{}[u:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].
            (app((\mlambda{}b);  u)  =  (b)[u])
\mvdash{}  app((\mlambda{}EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q));  f)
=  (EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q))[f]


By

---

Latex:
((D  -1  With  \mkleeneopen{}(Path\_c\mBbbU{}  (A)p  (B)p)\mkleeneclose{}    THENA  (MemCD  THEN  Auto))
  THEN  (D  -1  With  \mkleeneopen{}EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q)\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto))

---

Home Index