---

Step * of Lemma cubical-term-at-comp-constant-type

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[I:fset(ℕ)]. ∀[rho:Gamma(I)]. ∀[J:fset(ℕ)]. ∀[f:{f:J ⟶ I| 
                                                                                     phi(f(rho))
                                                                                     = 1
                                                                                     ∈ Point(face_lattice(J))} ].
∀[K:fset(ℕ)]. ∀[g:K ⟶ J].
  (phi(g(f(rho))) = phi(f ⋅ g(rho)) ∈ Point(face_lattice(K)))
BY
{ (Intros THEN (RWW "cubical-term-at-morph< face-type-ap-morph fl-morph-comp" 0⋅ THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. I : fset(ℕ)
4. rho : Gamma(I)
5. J : fset(ℕ)
6. f : {f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} 
7. K : fset(ℕ)
8. g : K ⟶ J
⊢ ((phi(rho))<f>)<g> = ((<g> o <f>) phi(rho)) ∈ Point(face_lattice(K))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[rho:Gamma(I)].  \mforall{}[J:fset(\mBbbN{})].
\mforall{}[f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\}  ].  \mforall{}[K:fset(\mBbbN{})].  \mforall{}[g:K  {}\mrightarrow{}  J].
    (phi(g(f(rho)))  =  phi(f  \mcdot{}  g(rho)))


By

---

Latex:
(Intros  THEN  (RWW  "cubical-term-at-morph<  face-type-ap-morph  fl-morph-comp"  0\mcdot{}  THENA  Auto))

---

Home Index