---

Step * 1 of Lemma compatible-composition_wf

.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ Gamma, (phi ∧ psi)
11. chi : {H ⊢ _:𝔽}
12. u : {H, chi.𝕀 ⊢ _:(A)sigma}
13. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
⊢ (cB H sigma chi u a0) = (cA H sigma chi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]} ∈ ℙ{[j 2 | i]}
BY
{ Assert ⌜(A)sigma = (B)sigma ∈ {H.𝕀 ⊢ _}⌝⋅ }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ Gamma, (phi ∧ psi)
11. chi : {H ⊢ _:𝔽}
12. u : {H, chi.𝕀 ⊢ _:(A)sigma}
13. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
⊢ (A)sigma = (B)sigma ∈ {H.𝕀 ⊢ _}

2
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ Gamma, (phi ∧ psi)
11. chi : {H ⊢ _:𝔽}
12. u : {H, chi.𝕀 ⊢ _:(A)sigma}
13. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
14. (A)sigma = (B)sigma ∈ {H.𝕀 ⊢ _}
⊢ (cB H sigma chi u a0) = (cA H sigma chi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]} ∈ ℙ{[j 2 | i]}

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  A  :  \{Gamma,  phi  \mvdash{}  \_\}
5.  B  :  \{Gamma,  psi  \mvdash{}  \_\}
6.  cA  :  Gamma,  phi  \mvdash{}  Compositon(A)
7.  cB  :  Gamma,  psi  \mvdash{}  Compositon(B)
8.  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  A  =  B
9.  H  :  CubicalSet\{j\}
10.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Gamma,  (phi  \mwedge{}  psi)
11.  chi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
12.  u  :  \{H,  chi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
13.  a0  :  \{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][chi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
\mvdash{}  (cB  H  sigma  chi  u  a0)  =  (cA  H  sigma  chi  u  a0)  \mmember{}  \mBbbP{}\{[j  2  |  i]\}


By

---

Latex:
Assert  \mkleeneopen{}(A)sigma  =  (B)sigma\mkleeneclose{}\mcdot{}

---

Home Index