---

Step * of Lemma context-subset_wf

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}].  Gamma, phi j⊢
BY
{ (Auto
   THEN (MemTypeCD THENW Auto)
   THEN RepUR ``context-subset cat-ob cat-arrow op-cat names-cat type-cat cat-id cat-comp`` 0
   THEN ((D 0 THEN Intros THEN FunExt THEN Reduce 0 THEN Auto THEN D -1 THEN EqTypeCD THEN Auto)
   ORELSE ((MemCD THEN Reduce 0) THEN Auto)
   )) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. I : fset(ℕ)
4. rho : Gamma(I)
⊢ phi(rho) = 1 ∈ Point(face_lattice(I)) ∈ 𝕌{j'}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].    Gamma,  phi  j\mvdash{}


By

---

Latex:
(Auto
  THEN  (MemTypeCD  THENW  Auto)
  THEN  RepUR  ``context-subset  cat-ob  cat-arrow  op-cat  names-cat  type-cat  cat-id  cat-comp``  0
  THEN  ((D  0  THEN  Intros  THEN  FunExt  THEN  Reduce  0  THEN  Auto  THEN  D  -1  THEN  EqTypeCD  THEN  Auto)
  ORELSE  ((MemCD  THEN  Reduce  0)  THEN  Auto)
  ))

---

Home Index