---

Step * of Lemma csm-comp-structure_wf

No Annotations
∀[Gamma,Delta:j⊢]. ∀[tau:Delta j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ Compositon(A)].
  ((cA)tau ∈ Delta ⊢ Compositon((A)tau))
BY
{ (Intros THEN Unhide THEN DVar `cA' THEN MemTypeCD) }

1
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. tau : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : composition-function{j:l,i:l}(Gamma;A)
6. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
⊢ (cA)tau ∈ composition-function{j:l,i:l}(Delta;(A)tau)

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. tau : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : composition-function{j:l,i:l}(Gamma;A)
6. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
⊢ uniform-comp-function{j:l, i:l}(Delta; (A)tau; (cA)tau)

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. tau : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : composition-function{j:l,i:l}(Gamma;A)
6. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
7. comp : composition-function{j:l,i:l}(Delta;(A)tau)
⊢ istype(uniform-comp-function{j:l, i:l}(Delta; (A)tau; comp))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[tau:Delta  j{}\mrightarrow{}  Gamma].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  Compositon(A)].
    ((cA)tau  \mmember{}  Delta  \mvdash{}  Compositon((A)tau))


By

---

Latex:
(Intros  THEN  Unhide  THEN  DVar  `cA'  THEN  MemTypeCD)

---

Home Index