---

Step * of Lemma case-type-comp-partition

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[B:{Gamma, psi ⊢ _}]. ∀[cA:Gamma, phi ⊢ Compositon(A)].
∀[cB:Gamma, psi ⊢ Compositon(B)].
  case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma ⊢ Compositon((if phi then A else B)) 
  supposing Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽)) ∧ Gamma ⊢ (1(𝔽) ⇒ (phi ∨ psi))
BY
{ (InstLemma `case-type-comp-disjoint` []
   THEN RepeatFor 8 ((ParallelLast' THENA Auto))
   THEN DoSubsume
   THEN Try (Trivial)
   THEN BLemma `composition-structure-subset`
   THEN 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. Gamma ⊢ (1(𝔽) ⇒ (phi ∨ psi))
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
= case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
⊢ sub_cubical_set{j:l}(Gamma; Gamma, (phi ∨ psi))

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) ⇒ 0(𝔽))
9. Gamma ⊢ (1(𝔽) ⇒ (phi ∨ psi))
10. case-type-comp(Gamma; phi; psi; A; B; cA; cB) ∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
11. case-type-comp(Gamma; phi; psi; A; B; cA; cB)
= case-type-comp(Gamma; phi; psi; A; B; cA; cB)
∈ Gamma, (phi ∨ psi) ⊢ Compositon((if phi then A else B))
⊢ Gamma, (phi ∧ psi) ⊢ A = B

---

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)].
    case-type-comp(Gamma;  phi;  psi;  A;  B;  cA;  cB)  \mmember{}  Gamma  \mvdash{}  Compositon((if  phi  then  A  else  B)) 
    supposing  Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))  \mwedge{}  Gamma  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (phi  \mvee{}  psi))


By

---

Latex:
(InstLemma  `case-type-comp-disjoint`  []
  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))
  THEN  DoSubsume
  THEN  Try  (Trivial)
  THEN  BLemma  `composition-structure-subset`
  THEN  Auto)

---

Home Index