---

Step * 1 of Lemma csm-canonical-section-face-type


1. I : fset(ℕ)
2. K : fset(ℕ)
3. f : K ⟶ I
4. phi : 𝔽(I)
5. J : fset(ℕ)
6. g : J ⟶ K
⊢ ((phi)<f>)<g> = (phi)<(<f>)g> ∈ 𝔽(g)
BY
{ (RepUR ``face-presheaf`` -3
   THEN (Subst' (<f>)g ~ f ⋅ g 0 THENA (RepUR ``context-map formal-cube functor-arrow csm-ap`` 0 THEN Auto))
   ) }

1
1. I : fset(ℕ)
2. K : fset(ℕ)
3. f : K ⟶ I
4. phi : Point(face_lattice(I))
5. J : fset(ℕ)
6. g : J ⟶ K
⊢ ((phi)<f>)<g> = (phi)<f ⋅ g> ∈ 𝔽(g)

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  K  :  fset(\mBbbN{})
3.  f  :  K  {}\mrightarrow{}  I
4.  phi  :  \mBbbF{}(I)
5.  J  :  fset(\mBbbN{})
6.  g  :  J  {}\mrightarrow{}  K
\mvdash{}  ((phi)<f>)<g>  =  (phi)<(<f>)g>


By

---

Latex:
(RepUR  ``face-presheaf``  -3
  THEN  (Subst'  (<f>)g  \msim{}  f  \mcdot{}  g  0
              THENA  (RepUR  ``context-map  formal-cube  functor-arrow  csm-ap``  0  THEN  Auto)
              )
  )

---

Home Index