---

Step * 2 of Lemma comp-to-fill_wf


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}
11. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:(A)sigma o m}
⊢ cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) ((u)m ∨ ((a0)p)m) (a0)p ∈ {H.𝕀 ⊢ _:(A)sigma[(phi)p |⟶ u]}
BY
{ Assert ⌜((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}⌝⋅ }

1
.....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}
11. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:(A)sigma o m}
⊢ ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}

2
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}
11. ((a0)p)m ∈ {H.𝕀.𝕀, ((q=0))p ⊢ _:(A)sigma o m}
12. ((A)sigma o m)[1(𝕀)] = (A)sigma ∈ {H.𝕀 ⊢ _}
⊢ cA H.𝕀 sigma o m ((phi)p ∨ (q=0)) ((u)m ∨ ((a0)p)m) (a0)p ∈ {H.𝕀 ⊢ _:(A)sigma[(phi)p |⟶ u]}

---

Latex:

---

Latex:

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\}
11.  ((a0)p)m  \mmember{}  \{H.\mBbbI{}.\mBbbI{},  ((q=0))p  \mvdash{}  \_:(A)sigma  o  m\}
\mvdash{}  cA  H.\mBbbI{}  sigma  o  m  ((phi)p  \mvee{}  (q=0))  ((u)m  \mvee{}  ((a0)p)m)  (a0)p  \mmember{}  \{H.\mBbbI{}  \mvdash{}  \_:(A)sigma[(phi)p  |{}\mrightarrow{}  u]\}


By

---

Latex:
Assert  \mkleeneopen{}((A)sigma  o  m)[1(\mBbbI{})]  =  (A)sigma\mkleeneclose{}\mcdot{}

---

Home Index