---

Step * of Lemma cubical-term-at-comp

No Annotations
∀Gamma:j⊢. ∀T:{Gamma ⊢ _}. ∀t:{Gamma ⊢ _:T}. ∀I:fset(ℕ). ∀rho:Gamma(I). ∀J:fset(ℕ). ∀f:J ⟶ I. ∀K:fset(ℕ). ∀g:K ⟶ J.
  (t(f ⋅ g(rho)) = t(g(f(rho))) ∈ T(g(f(rho))))
BY
{ PresheafMLTTInstance Obid: presheaf-term-at-comp⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}T:\{Gamma  \mvdash{}  \_\}.  \mforall{}t:\{Gamma  \mvdash{}  \_:T\}.  \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.
    (t(f  \mcdot{}  g(rho))  =  t(g(f(rho))))


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-term-at-comp\mcdot{}

---

Home Index