---

Step * 1 of Lemma same-cubical-type-0


1. Gamma : CubicalSet{j}
2. A : {Gamma, 0(𝔽) ⊢ _}
3. B : {Gamma, 0(𝔽) ⊢ _}
4. ∀I:fset(ℕ). (¬Gamma, 0(𝔽)(I))
⊢ Gamma, 0(𝔽) ⊢ A = B
BY
{ (Unfold `same-cubical-type` 0
   THEN Unhide
   THEN (BLemma `cubical-type-equal2` THENW Auto)
   THEN RepeatFor 2 (DVar `A'⋅)
   THEN RepeatFor 2 (DVar `B'⋅)
   THEN (EqCD THENA Auto)
   THEN Repeat ((FunExt THENA Auto))
   THEN (InstHyp [⌜I⌝] 8⋅ THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma,  0(\mBbbF{})  \mvdash{}  \_\}
3.  B  :  \{Gamma,  0(\mBbbF{})  \mvdash{}  \_\}
4.  \mforall{}I:fset(\mBbbN{}).  (\mneg{}Gamma,  0(\mBbbF{})(I))
\mvdash{}  Gamma,  0(\mBbbF{})  \mvdash{}  A  =  B


By

---

Latex:
(Unfold  `same-cubical-type`  0
  THEN  Unhide
  THEN  (BLemma  `cubical-type-equal2`  THENW  Auto)
  THEN  RepeatFor  2  (DVar  `A'\mcdot{})
  THEN  RepeatFor  2  (DVar  `B'\mcdot{})
  THEN  (EqCD  THENA  Auto)
  THEN  Repeat  ((FunExt  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}I\mkleeneclose{}]  8\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index