---

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


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

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

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

3
.....eq aux..... 
1. Gamma : CubicalSet{j}
2. x1 : Top
3. x2 : Top
4. y1 : Top
5. y2 : Top
6. ∀I:fset(ℕ). (¬Gamma, 0(𝔽)(I))
7. A : I:fset(ℕ) ⟶ Gamma, 0(𝔽)(I) ⟶ Type
⊢ istype(I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma, 0(𝔽)(I) ⟶ (A I a) ⟶ (A J f(a)))

---

Latex:

---

Latex:

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


By

---

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

---

Home Index