---

Step * 2 1 of Lemma empty-context-subset-lemma5


1. Gamma : CubicalSet{j}
2. i : {Gamma ⊢ _:𝕀}
3. x : Top × Top
4. y : Top × Top
5. ∀I:fset(ℕ). (¬Gamma, (i=0), (i=1)(I))
⊢ x
= y
∈ (A:I:fset(ℕ) ⟶ Gamma, (i=0), (i=1)(I) ⟶ Type × (I:fset(ℕ)
                                                   ⟶ J:fset(ℕ)
                                                   ⟶ f:J ⟶ I
                                                   ⟶ a:Gamma, (i=0), (i=1)(I)
                                                   ⟶ (A I a)
                                                   ⟶ (A J f(a))))
BY
{ ((DVar `x' THEN DVar `y') THEN EqCD THEN Auto) }

1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. i : {Gamma ⊢ _:𝕀}
3. x1 : Top
4. x2 : Top
5. y1 : Top
6. y2 : Top
7. ∀I:fset(ℕ). (¬Gamma, (i=0), (i=1)(I))
⊢ x1 = y1 ∈ (I:fset(ℕ) ⟶ Gamma, (i=0), (i=1)(I) ⟶ Type)

2
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. i : {Gamma ⊢ _:𝕀}
3. x1 : Top
4. x2 : Top
5. y1 : Top
6. y2 : Top
7. ∀I:fset(ℕ). (¬Gamma, (i=0), (i=1)(I))
⊢ x2 = y2 ∈ (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma, (i=0), (i=1)(I) ⟶ (x1 I a) ⟶ (x1 J f(a)))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  i  :  \{Gamma  \mvdash{}  \_:\mBbbI{}\}
3.  x  :  Top  \mtimes{}  Top
4.  y  :  Top  \mtimes{}  Top
5.  \mforall{}I:fset(\mBbbN{}).  (\mneg{}Gamma,  (i=0),  (i=1)(I))
\mvdash{}  x  =  y


By

---

Latex:
((DVar  `x'  THEN  DVar  `y')  THEN  EqCD  THEN  Auto)

---

Home Index