---

Step * 1 of Lemma csm-fill_term

.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
10. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
⊢ (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)][(phi)s |⟶ (u)s+[0]]}
BY
{ (DVar `a0' THEN MemTypeCD) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)]}
7. partial-term-0(Gamma;u) = a0 ∈ {Gamma, phi ⊢ _:(A)[0(𝕀)]}
8. Delta : CubicalSet{j}
9. s : Delta j⟶ Gamma
10. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
11. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
⊢ (a0)s ∈ {Delta ⊢ _:((A)s+)[0(𝕀)]}

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)]}
7. partial-term-0(Gamma;u) = a0 ∈ {Gamma, phi ⊢ _:(A)[0(𝕀)]}
8. Delta : CubicalSet{j}
9. s : Delta j⟶ Gamma
10. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
11. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
⊢ partial-term-0(Delta;(u)s+) = (a0)s ∈ {Delta, (phi)s ⊢ _:((A)s+)[0(𝕀)]}

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ Compositon(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)]}
7. partial-term-0(Gamma;u) = a0 ∈ {Gamma, phi ⊢ _:(A)[0(𝕀)]}
8. Delta : CubicalSet{j}
9. s : Delta j⟶ Gamma
10. Delta.𝕀 ⊢ (((phi)s)p ⇒ ((phi)p)s+)
11. (u)s+ ∈ {Delta.𝕀, ((phi)s)p ⊢ _:(A)s+}
12. a : {Delta ⊢ _:((A)s+)[0(𝕀)]}
⊢ istype(partial-term-0(Delta;(u)s+) = a ∈ {Delta, (phi)s ⊢ _:((A)s+)[0(𝕀)]})

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
4.  cA  :  Gamma.\mBbbI{}  \mvdash{}  Compositon(A)
5.  u  :  \{Gamma.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}
6.  a0  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  u[0]]\}
7.  Delta  :  CubicalSet\{j\}
8.  s  :  Delta  j{}\mrightarrow{}  Gamma
9.  Delta.\mBbbI{}  \mvdash{}  (((phi)s)p  {}\mRightarrow{}  ((phi)p)s+)
10.  (u)s+  \mmember{}  \{Delta.\mBbbI{},  ((phi)s)p  \mvdash{}  \_:(A)s+\}
\mvdash{}  (a0)s  \mmember{}  \{Delta  \mvdash{}  \_:((A)s+)[0(\mBbbI{})][(phi)s  |{}\mrightarrow{}  (u)s+[0]]\}


By

---

Latex:
(DVar  `a0'  THEN  MemTypeCD)

---

Home Index