---

Step * of Lemma case-cube_wf

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[B:{Gamma, psi ⊢ _}]. ∀[I:fset(ℕ)].
∀[rho:Gamma, (phi ∨ psi)(I)].
  (case-cube(phi;A;B;I;rho) ∈ Type)
BY
{ (Auto
   THEN RepUR ``context-subset`` -1
   THEN D -1
   THEN RepUR ``face-or cubical-term-at`` -1
   THEN Fold `cubical-term-at` (-1)
   THEN (RWO  "face_lattice-1-join-irreducible" (-1) THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. I : fset(ℕ)
7. rho : Gamma(I)
8. (phi(rho) = 1 ∈ Point(face_lattice(I))) ∨ (psi(rho) = 1 ∈ Point(face_lattice(I)))
⊢ case-cube(phi;A;B;I;rho) ∈ Type

---

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{}[I:fset(\mBbbN{})].
\mforall{}[rho:Gamma,  (phi  \mvee{}  psi)(I)].
    (case-cube(phi;A;B;I;rho)  \mmember{}  Type)


By

---

Latex:
(Auto
  THEN  RepUR  ``context-subset``  -1
  THEN  D  -1
  THEN  RepUR  ``face-or  cubical-term-at``  -1
  THEN  Fold  `cubical-term-at`  (-1)
  THEN  (RWO    "face\_lattice-1-join-irreducible"  (-1)  THENA  Auto))

---

Home Index