---

Step * 1 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)})
⊢ {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]']}
BY
{ (EqCDA
   THEN (InstLemma `csm-path-type`
          [⌜parm{i|j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜G.Equiv(decode(A);decode(B))⌝;⌜p⌝;⌜c𝕌⌝;⌜A⌝;⌜B⌝]⋅
         THENA 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. ((Path_c𝕌 A B))p = (G.Equiv(decode(A);decode(B)) ⊢ Path_(c𝕌)p (A)p (B)p) ∈ {G.Equiv(decode(A);decode(B)) ⊢' _}
⊢ (G.Equiv(decode(A);decode(B)) ⊢ Path_c𝕌 (A)p (B)p) = ((Path_c𝕌 A 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)\})
\mvdash{}  \{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\}


By

---

Latex:
(EqCDA
  THEN  (InstLemma  `csm-path-type`
                [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}G.Equiv(decode(A);decode(B))\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  )

---

Home Index