---

Step * 2 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 ∈ {Gamma, 0(𝔽) ⊢ _}
BY
{ EqTypeCD }

1
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))))

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. x : Top × Top
3. y : Top × Top
4. ∀I:fset(ℕ). (¬Gamma, 0(𝔽)(I))
⊢ let A,F = x 
  in (∀I:fset(ℕ). ∀a:Gamma, 0(𝔽)(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
     ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, 0(𝔽)(I). ∀u:A I a.
          ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. x : Top × Top
3. y : Top × Top
4. ∀I:fset(ℕ). (¬Gamma, 0(𝔽)(I))
5. AF : 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)))
⊢ istype(let A,F = AF 
         in (∀I:fset(ℕ). ∀a:Gamma, 0(𝔽)(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
            ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, 0(𝔽)(I). ∀u:A I a.
                 ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(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:
EqTypeCD

---

Home Index