---

Step * of Lemma comp-to-fill_wf2

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ Compositon(A)].  (comp-to-fill(Gamma;cA) ∈ Gamma ⊢ Filling(A))
BY
{ (Auto THEN D -1 THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
⊢ uniform-filling-function{j:l, i:l}(Gamma;A;comp-to-fill(Gamma;cA))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  Compositon(A)].
    (comp-to-fill(Gamma;cA)  \mmember{}  Gamma  \mvdash{}  Filling(A))


By

---

Latex:
(Auto  THEN  D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index