---

Step * 1 2 of Lemma 0-comp-cc-fst-comp-m


1. H : CubicalSet{j}
2. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
     f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
3. I : fset(ℕ)
4. a1 : H(I)
5. a2 : 𝕀(a1)
6. x1 : 𝕀(<a1, a2>)
7. ((q=0))p(<<a1, a2>, x1>) = 1 ∈ Point(face_lattice(I))
⊢ <a1, a2 ∧ x1> = <a1, 0> ∈ (alpha:H(I) × 𝕀(alpha))
BY
{ EqCDA }

1
.....subterm..... T:t
2:n
1. H : CubicalSet{j}
2. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
     f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
3. I : fset(ℕ)
4. a1 : H(I)
5. a2 : 𝕀(a1)
6. x1 : 𝕀(<a1, a2>)
7. ((q=0))p(<<a1, a2>, x1>) = 1 ∈ Point(face_lattice(I))
⊢ a2 ∧ x1 = 0 ∈ 𝕀(a1)

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  \mforall{}[A,B:j\mvdash{}].  \mforall{}[f:A  j{}\mrightarrow{}  B].  \mforall{}[g:I:fset(\mBbbN{})  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)].    f  =  g  supposing  f  =  g
3.  I  :  fset(\mBbbN{})
4.  a1  :  H(I)
5.  a2  :  \mBbbI{}(a1)
6.  x1  :  \mBbbI{}(<a1,  a2>)
7.  ((q=0))p(<<a1,  a2>,  x1>)  =  1
\mvdash{}  <a1,  a2  \mwedge{}  x1>  =  <a1,  0>


By

---

Latex:
EqCDA

---

Home Index