---

Step * 1 of Lemma comp-to-fill_wf

.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : H:CubicalSet{j}
⟶ sigma:H.𝕀 j⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H, phi.𝕀 ⊢ _:(A)sigma}
⟶ a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⟶ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}
4. H : CubicalSet{j}
5. sigma : H.𝕀 j⟶ Gamma
6. phi : {H ⊢ _:𝔽}
7. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
8. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ u[0]]}
9. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
10. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
⊢ ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:(A)sigma o m}
BY
{ DVar `a0' }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : H:CubicalSet{j}
⟶ sigma:H.𝕀 j⟶ Gamma
⟶ phi:{H ⊢ _:𝔽}
⟶ u:{H, phi.𝕀 ⊢ _:(A)sigma}
⟶ a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⟶ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}
4. H : CubicalSet{j}
5. sigma : H.𝕀 j⟶ Gamma
6. phi : {H ⊢ _:𝔽}
7. u : {H.𝕀, (phi)p ⊢ _:(A)sigma}
8. a0 : {H ⊢ _:((A)sigma)[0(𝕀)]}
9. partial-term-0(H;u) = a0 ∈ {H, phi ⊢ _:((A)sigma)[0(𝕀)]}
10. ((phi)p)m ∈ {H.𝕀.𝕀 ⊢ _:𝔽}
11. (u)m ∈ {H.𝕀.𝕀, ((phi)p)m ⊢ _:((A)sigma)m}
⊢ ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:(A)sigma o m}

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  H:CubicalSet\{j\}
{}\mrightarrow{}  sigma:H.\mBbbI{}  j{}\mrightarrow{}  Gamma
{}\mrightarrow{}  phi:\{H  \mvdash{}  \_:\mBbbF{}\}
{}\mrightarrow{}  u:\{H,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
{}\mrightarrow{}  a0:\{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
{}\mrightarrow{}  \{H  \mvdash{}  \_:((A)sigma)[1(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[1(\mBbbI{})]]\}
4.  H  :  CubicalSet\{j\}
5.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Gamma
6.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
7.  u  :  \{H.\mBbbI{},  (phi)p  \mvdash{}  \_:(A)sigma\}
8.  a0  :  \{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  u[0]]\}
9.  ((phi)p)m  \mmember{}  \{H.\mBbbI{}.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
10.  (u)m  \mmember{}  \{H.\mBbbI{}.\mBbbI{},  ((phi)p)m  \mvdash{}  \_:((A)sigma)m\}
\mvdash{}  ((a0)p)m  \mmember{}  \{H.\mBbbI{}.\mBbbI{},  ((q=0))p  \mvdash{}  \_:(A)sigma  o  m\}


By

---

Latex:
DVar  `a0'

---

Home Index