---

Step * 1 of Lemma transprt-const_wf


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}
BY
{ (Fold `transprt-const` (-1) THEN InferEqualType THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Fold  `transprt-const`  (-1)  THEN  InferEqualType  THEN  Auto)

---

Home Index