---

Step * of Lemma uabeta-type_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}].  G ⊢ uabeta-type(G;A;B)
BY
{ (Intros⋅
   THEN (InstLemma `uabetatype_wf` [⌜G⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜λG,A,p. PathTransport(p)⌝] (-1)⋅
   THENM (RepUR ``uabetatype`` -1 THEN RepUR ``uabeta-type`` 0 THEN Try (Eq))
   )
   THEN Auto) }

1
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].    G  \mvdash{}  uabeta-type(G;A;B)


By

---

Latex:
(Intros\mcdot{}
  THEN  (InstLemma  `uabetatype\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}G,A,p.  PathTransport(p)\mkleeneclose{}]  (-1)\mcdot{}
  THENM  (RepUR  ``uabetatype``  -1  THEN  RepUR  ``uabeta-type``  0  THEN  Try  (Eq))
  )
  THEN  Auto)

---

Home Index