---

Step * 1 of Lemma compU_wf


1. G : CubicalSet{j}
2. H : CubicalSet{j}
3. K : CubicalSet{j}
4. tau : K j⟶ H
5. sigma : H.𝕀 j⟶ G
6. phi : {H ⊢ _:𝔽}
7. {H, phi.𝕀 ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
8. u : {H, phi.𝕀 ⊢ _:c𝕌}
9. {H ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
10. {H, phi ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
⊢ ∀a0:{a:{H ⊢ _:c𝕌}| (u)[0(𝕀)] = a ∈ {H, phi ⊢ _:c𝕌}} 
    ((compU() H sigma phi u a0)tau
    = (compU() K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
    ∈ {a:{K ⊢ _:(c𝕌)tau}| ((u)[1(𝕀)])tau = a ∈ {K, (phi)tau ⊢ _:(c𝕌)tau}} )
BY
{ D 0 }

1
1. G : CubicalSet{j}
2. H : CubicalSet{j}
3. K : CubicalSet{j}
4. tau : K j⟶ H
5. sigma : H.𝕀 j⟶ G
6. phi : {H ⊢ _:𝔽}
7. {H, phi.𝕀 ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
8. u : {H, phi.𝕀 ⊢ _:c𝕌}
9. {H ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
10. {H, phi ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
11. a0 : {a:{H ⊢ _:c𝕌}| (u)[0(𝕀)] = a ∈ {H, phi ⊢ _:c𝕌}} 
⊢ (compU() H sigma phi u a0)tau
= (compU() K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
∈ {a:{K ⊢ _:(c𝕌)tau}| ((u)[1(𝕀)])tau = a ∈ {K, (phi)tau ⊢ _:(c𝕌)tau}} 

2
.....wf..... 
1. G : CubicalSet{j}
2. H : CubicalSet{j}
3. K : CubicalSet{j}
4. tau : K j⟶ H
5. sigma : H.𝕀 j⟶ G
6. phi : {H ⊢ _:𝔽}
7. {H, phi.𝕀 ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
8. u : {H, phi.𝕀 ⊢ _:c𝕌}
9. {H ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
10. {H, phi ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
⊢ istype({a:{H ⊢ _:c𝕌}| (u)[0(𝕀)] = a ∈ {H, phi ⊢ _:c𝕌}} )

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  H  :  CubicalSet\{j\}
3.  K  :  CubicalSet\{j\}
4.  tau  :  K  j{}\mrightarrow{}  H
5.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  G
6.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
7.  \{H,  phi.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}  \mmember{}  \mBbbU{}\{[i'  |  j']\}
8.  u  :  \{H,  phi.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}
9.  \{H  \mvdash{}  \_:c\mBbbU{}\}  \mmember{}  \mBbbU{}\{[i'  |  j']\}
10.  \{H,  phi  \mvdash{}  \_:c\mBbbU{}\}  \mmember{}  \mBbbU{}\{[i'  |  j']\}
\mvdash{}  \mforall{}a0:\{a:\{H  \mvdash{}  \_:c\mBbbU{}\}|  (u)[0(\mBbbI{})]  =  a\} 
        ((compU()  H  sigma  phi  u  a0)tau  =  (compU()  K  sigma  o  tau+  (phi)tau  (u)tau+  (a0)tau))


By

---

Latex:
D  0

---

Home Index