---

Step * 1 1 of Lemma compatible-composition-disjoint


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) ⇒ 0(𝔽))
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ Gamma, (phi ∧ psi)
11. chi : {H ⊢ _:𝔽}
12. ∀[I:fset(ℕ)]. (¬H.𝕀(I))
13. H.𝕀 ⊢ (A)sigma
14. H, chi.𝕀 ⊢ (A)sigma
15. u : {H, chi.𝕀 ⊢ _:(A)sigma}
⊢ ∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
    ((cB H sigma chi u a0) = (cA H sigma chi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]})
BY
{ (D 0 THENA Auto) }

1
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) ⇒ 0(𝔽))
9. H : CubicalSet{j}
10. sigma : H.𝕀 j⟶ Gamma, (phi ∧ psi)
11. chi : {H ⊢ _:𝔽}
12. ∀[I:fset(ℕ)]. (¬H.𝕀(I))
13. H.𝕀 ⊢ (A)sigma
14. H, chi.𝕀 ⊢ (A)sigma
15. u : {H, chi.𝕀 ⊢ _:(A)sigma}
16. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
⊢ (cB H sigma chi u a0) = (cA H sigma chi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]}

---

Latex:

---

Latex:

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  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))
9.  H  :  CubicalSet\{j\}
10.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Gamma,  (phi  \mwedge{}  psi)
11.  chi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
12.  \mforall{}[I:fset(\mBbbN{})].  (\mneg{}H.\mBbbI{}(I))
13.  H.\mBbbI{}  \mvdash{}  (A)sigma
14.  H,  chi.\mBbbI{}  \mvdash{}  (A)sigma
15.  u  :  \{H,  chi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
\mvdash{}  \mforall{}a0:\{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][chi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}.  ((cB  H  sigma  chi  u  a0)  =  (cA  H  sigma  chi  u  a0))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index