---

Step * 2 of Lemma univ-a_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. G ⊢ Equiv(decode(A);decode(B))
5. (A)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
6. (B)p ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:c𝕌}
7. ∀[X:ij⊢]. ∀[A,B:{X ⊢' _}]. ∀[b:{X.A ⊢ _:(B)p}].  (cubical-lam(X;b) ∈ {X ⊢ _:(A ⟶ B)})
8. {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}
= {G.Equiv(decode(A);decode(B)) ⊢ _:((Path_c𝕌 A B))p}
∈ 𝕌{[i | [j | i]']}
⊢ EquivPath(G.Equiv(decode(A);decode(B));(A)p;(B)p;q) ∈ {G.Equiv(decode(A);decode(B)) ⊢ _:(Path_c𝕌 (A)p (B)p)}
BY
{ (MemCD THEN Try (Trivial) THEN Auto) }

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

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
3.  B  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
4.  G  \mvdash{}  Equiv(decode(A);decode(B))
5.  (A)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
6.  (B)p  \mmember{}  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:c\mBbbU{}\}
7.  \mforall{}[X:ij\mvdash{}].  \mforall{}[A,B:\{X  \mvdash{}'  \_\}].  \mforall{}[b:\{X.A  \mvdash{}  \_:(B)p\}].    (cubical-lam(X;b)  \mmember{}  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\})
8.  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:(Path\_c\mBbbU{}  (A)p  (B)p)\}
=  \{G.Equiv(decode(A);decode(B))  \mvdash{}  \_:((Path\_c\mBbbU{}  A  B))p\}
\mvdash{}  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)\}


By

---

Latex:
(MemCD  THEN  Try  (Trivial)  THEN  Auto)

---

Home Index