---

Step * of Lemma transprt-const_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[a:{G ⊢ _:A}].  (transprt-const(G;cA;a) ∈ {G ⊢ _:A})
BY
{ (Auto
   THEN (InstLemmaIJ `transprt_wf` [⌜G⌝;⌜(A)p⌝;⌜(cA)p⌝]⋅ THENA Auto)
   THEN (Subst' ((A)p)[0(𝕀)] ~ (A)1(G) -1 THENA (CsmUnfolding THEN Auto))
   THEN (Subst' ((A)p)[1(𝕀)] ~ (A)1(G) -1 THENA (CsmUnfolding THEN Auto))
   THEN (InstHyp [⌜a⌝] (-1) ⋅ THENA Auto)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. ∀[a:{G ⊢ _:(A)1(G)}]. (transprt(G;(cA)p;a) ∈ {G ⊢ _:(A)1(G)})
6. transprt(G;(cA)p;a) ∈ {G ⊢ _:(A)1(G)}
⊢ transprt-const(G;cA;a) ∈ {G ⊢ _:A}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[a:\{G  \mvdash{}  \_:A\}].
    (transprt-const(G;cA;a)  \mmember{}  \{G  \mvdash{}  \_:A\})


By

---

Latex:
(Auto
  THEN  (InstLemmaIJ  `transprt\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(cA)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  ((A)p)[0(\mBbbI{})]  \msim{}  (A)1(G)  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (Subst'  ((A)p)[1(\mBbbI{})]  \msim{}  (A)1(G)  -1  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)  \mcdot{}  THENA  Auto))

---

Home Index