---

Step * of Lemma cubical-term-at-comp-is-1

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

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. I : fset(ℕ)
4. rho : Gamma(I)
5. J : fset(ℕ)
6. f : J ⟶ I
7. K : fset(ℕ)
8. g : K ⟶ J
9. (phi(rho) rho f) = 1 ∈ Point(face_lattice(J))
⊢ (phi(rho) rho f ⋅ g) = 1 ∈ 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:J  {}\mrightarrow{}  I].
\mforall{}[K:fset(\mBbbN{})].  \mforall{}[g:K  {}\mrightarrow{}  J].
    ((phi(f(rho))  =  1)  {}\mRightarrow{}  (phi(f  \mcdot{}  g(rho))  =  1))


By

---

Latex:
(Intros
  THEN  (RWO    "cubical-term-at-morph<"  (-1)  THENA  Auto)
  THEN  (RWO    "cubical-term-at-morph<"  0  THENA  Auto))

---

Home Index