---

Step * 2 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 ∈ {Gamma, (i=0), (i=1) ⊢ _}
BY
{ At ⌜𝕌'⌝ EqTypeCD⋅ }

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

2
.....set predicate..... 
1. Gamma : CubicalSet{j}
2. i : {Gamma ⊢ _:𝕀}
3. x : Top × Top
4. y : Top × Top
5. ∀I:fset(ℕ). (¬Gamma, (i=0), (i=1)(I))
⊢ let A,F = x 
  in (∀I:fset(ℕ). ∀a:Gamma, (i=0), (i=1)(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, (i=0), (i=1)(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. i : {Gamma ⊢ _:𝕀}
3. x : Top × Top
4. y : Top × Top
5. ∀I:fset(ℕ). (¬Gamma, (i=0), (i=1)(I))
6. AF : 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)))
⊢ istype(let A,F = AF 
         in (∀I:fset(ℕ). ∀a:Gamma, (i=0), (i=1)(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, (i=0), (i=1)(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.  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:
At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  EqTypeCD\mcdot{}

---

Home Index