---

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

∀[I,K:fset(ℕ)]. ∀[f:K ⟶ I]. ∀[phi:𝔽(I)].
  (canonical-section(();𝔽;K;⋅;f(phi)) = (canonical-section(();𝔽;I;⋅;phi))<f> ∈ {formal-cube(K) ⊢ _:𝔽})
BY
{ (Auto
   THEN BLemma `cubical-term-equal2`
   THEN Try ((InferEqualType THENL [(RWO  "csm-face-type" 0 THEN Auto); Auto]))
   THEN Auto
   THEN RenameVar `J' (-2)
   THEN RenameVar `g' (-1)
   THEN RepUR ``formal-cube`` -1
   THEN RepUR ``canonical-section csm-ap-term`` 0
   THEN (RWO  "face-type-ap-morph" 0 THENA Auto)
   THEN RepUR ``face-presheaf`` 0) }

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

---

Latex:

---

Latex:
\mforall{}[I,K:fset(\mBbbN{})].  \mforall{}[f:K  {}\mrightarrow{}  I].  \mforall{}[phi:\mBbbF{}(I)].
    (canonical-section(();\mBbbF{};K;\mcdot{};f(phi))  =  (canonical-section(();\mBbbF{};I;\mcdot{};phi))<f>)


By

---

Latex:
(Auto
  THEN  BLemma  `cubical-term-equal2`
  THEN  Try  ((InferEqualType  THENL  [(RWO    "csm-face-type"  0  THEN  Auto);  Auto]))
  THEN  Auto
  THEN  RenameVar  `J'  (-2)
  THEN  RenameVar  `g'  (-1)
  THEN  RepUR  ``formal-cube``  -1
  THEN  RepUR  ``canonical-section  csm-ap-term``  0
  THEN  (RWO    "face-type-ap-morph"  0  THENA  Auto)
  THEN  RepUR  ``face-presheaf``  0)

---

Home Index