---

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


1. H : CubicalSet{j}
⊢ [0(𝕀)] o p o m = m ∈ H.𝕀.𝕀, ((q=0))p j⟶ H.𝕀
BY
{ (Symmetry
   THEN InstLemma `csm-equal` []
   THEN BHyp -1
   THEN Auto
   THEN RepeatFor 2 ((FunExt THENW Auto))
   THEN RepUR ``context-subset cube-context-adjoin`` -1
   THEN D -1
   THEN D -2
   THEN D -3
   THEN CsmUnfoldingNotInterval
   THEN RepUR ``cube-context-adjoin`` 0) }

1
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, 0> ∈ alpha:H(I) × 𝕀(alpha)

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

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
\mvdash{}  [0(\mBbbI{})]  o  p  o  m  =  m


By

---

Latex:
(Symmetry
  THEN  InstLemma  `csm-equal`  []
  THEN  BHyp  -1
  THEN  Auto
  THEN  RepeatFor  2  ((FunExt  THENW  Auto))
  THEN  RepUR  ``context-subset  cube-context-adjoin``  -1
  THEN  D  -1
  THEN  D  -2
  THEN  D  -3
  THEN  CsmUnfoldingNotInterval
  THEN  RepUR  ``cube-context-adjoin``  0)

---

Home Index