---

Step * of Lemma same-cubical-type-0

No Annotations
∀[Gamma:j⊢]. ∀[A,B:{Gamma, 0(𝔽) ⊢ _}].  Gamma, 0(𝔽) ⊢ A = B
BY
{ (Auto
   THEN (Assert ∀I:fset(ℕ). (¬Gamma, 0(𝔽)(I)) BY
               (RepeatFor 2 ((D 0 THENA Auto))
                THEN RepUR ``context-subset`` -1
                THEN D -1
                THEN RepUR ``cubical-term-at face-0`` -1
                THEN InstLemma `face-lattice-0-not-1` [⌜I⌝]⋅
                THEN Auto))
   ) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma, 0(𝔽) ⊢ _}
3. B : {Gamma, 0(𝔽) ⊢ _}
4. ∀I:fset(ℕ). (¬Gamma, 0(𝔽)(I))
⊢ Gamma, 0(𝔽) ⊢ A = B

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A,B:\{Gamma,  0(\mBbbF{})  \mvdash{}  \_\}].    Gamma,  0(\mBbbF{})  \mvdash{}  A  =  B


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}I:fset(\mBbbN{}).  (\mneg{}Gamma,  0(\mBbbF{})(I))  BY
                          (RepeatFor  2  ((D  0  THENA  Auto))
                            THEN  RepUR  ``context-subset``  -1
                            THEN  D  -1
                            THEN  RepUR  ``cubical-term-at  face-0``  -1
                            THEN  InstLemma  `face-lattice-0-not-1`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index