---

Step * of Lemma transEquivbeta-type_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}].  G ⊢ transEquivbeta-type{i:l}(G;A;B)
BY
{ (Intros⋅
   THEN (InstLemma `uabetatype_wf` [⌜G⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜λG,A,p. transEquivFun(p)⌝] (-1)⋅
   THENM (RepUR ``uabetatype`` -1 THEN RepUR ``transEquivbeta-type`` 0 THEN Try (Eq))
   )
   THEN (MemCD THENL [Id; Auto])
   THEN (MemCD THENL [(All Thin THEN RenameVar `G' 1 THEN RenameVar `A' 2); Auto])) }

1
1. G : CubicalSet{i|j}
2. A : {G ⊢ _:c𝕌}
⊢ λp.transEquivFun(p) ∈ TransportType(A)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].    G  \mvdash{}  transEquivbeta-type\{i:l\}(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.  transEquivFun(p)\mkleeneclose{}]  (-1)\mcdot{}
  THENM  (RepUR  ``uabetatype``  -1  THEN  RepUR  ``transEquivbeta-type``  0  THEN  Try  (Eq))
  )
  THEN  (MemCD  THENL  [Id;  Auto])
  THEN  (MemCD  THENL  [(All  Thin  THEN  RenameVar  `G'  1  THEN  RenameVar  `A'  2);  Auto]))

---

Home Index