---

Step * of Lemma compatible-composition-disjoint

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[B:{Gamma, psi ⊢ _}]. ∀[cA:Gamma, phi ⊢ Compositon(A)].
∀[cB:Gamma, psi ⊢ Compositon(B)].
  compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB) supposing Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽))
BY
{ (Intros
   THEN Unfold `compatible-composition` 0
   THEN RepeatFor 3 (Intro)
   THEN (InstLemma `map-to-context-subset-disjoint` [⌜Gamma⌝;⌜phi⌝;⌜psi⌝;⌜H.𝕀⌝;⌜sigma⌝]⋅ 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))
⊢ ∀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(𝕀)]})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  phi  \mvdash{}  \_\}].  \mforall{}[B:\{Gamma,  psi  \mvdash{}  \_\}].
\mforall{}[cA:Gamma,  phi  \mvdash{}  Compositon(A)].  \mforall{}[cB:Gamma,  psi  \mvdash{}  Compositon(B)].
    compatible-composition\{j:l,  i:l\}(Gamma;  phi;  psi;  A;  B;  cA;  cB) 
    supposing  Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))


By

---

Latex:
(Intros
  THEN  Unfold  `compatible-composition`  0
  THEN  RepeatFor  3  (Intro)
  THEN  (InstLemma  `map-to-context-subset-disjoint`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}sigma\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index