Step * of Lemma transEquiv-trans_wf

No Annotations
[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[p:{G ⊢ _:(Path_c𝕌 B)}].  (transEquivFun(p) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))})
BY
ProveWfLemma }


Latex:


Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[p:\{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}].
    (transEquivFun(p)  \mmember{}  \{G  \mvdash{}  \_:(decode(A)  {}\mrightarrow{}  decode(B))\})


By


Latex:
ProveWfLemma




Home Index