---

Step * 1 of Lemma uabeta-type_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. ∀[f:G:CubicalSet{i|j} ⟶ A:{G ⊢ _:c𝕌} ⟶ TransportType(A)]. G ⊢ uabetatype(G;A;B;f)
5. G1 : CubicalSet{i|j}
6. A1 : {G1 ⊢ _:c𝕌}
⊢ λp.PathTransport(p) ∈ TransportType(A1)
BY
{ (All Thin
   THEN RenameVar `G' 1
   THEN RenameVar `A' 2
   THEN (InstLemma `cubical-term_wf` [⌜parm{i|j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜c𝕌⌝]⋅ THENA Auto)
   THEN Unfold `transport-type` 0
   THEN Unfold `uall` 0
   THEN (MemTypeCD THENW Auto)
   THEN (InstLemma `cubical-term_wf` [parm{i|j};⌜parm{i'}⌝;⌜G⌝;⌜(Path_c𝕌 A B)⌝]⋅ THENA Auto)
   THEN MemCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
3.  B  :  \{G  \mvdash{}  \_:c\mBbbU{}\}
4.  \mforall{}[f:G:CubicalSet\{i|j\}  {}\mrightarrow{}  A:\{G  \mvdash{}  \_:c\mBbbU{}\}  {}\mrightarrow{}  TransportType(A)].  G  \mvdash{}  uabetatype(G;A;B;f)
5.  G1  :  CubicalSet\{i|j\}
6.  A1  :  \{G1  \mvdash{}  \_:c\mBbbU{}\}
\mvdash{}  \mlambda{}p.PathTransport(p)  \mmember{}  TransportType(A1)


By

---

Latex:
(All  Thin
  THEN  RenameVar  `G'  1
  THEN  RenameVar  `A'  2
  THEN  (InstLemma  `cubical-term\_wf`  [\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `transport-type`  0
  THEN  Unfold  `uall`  0
  THEN  (MemTypeCD  THENW  Auto)
  THEN  (InstLemma  `cubical-term\_wf`  [parm\{i|j\};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(Path\_c\mBbbU{}  A  B)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MemCD
  THEN  Auto)

---

Home Index