---

Step * of Lemma sub-cubical-set_functionality

No Annotations
∀[X:j⊢]. ∀[P,Q:I:fset(ℕ) ⟶ X(I) ⟶ ℙ].
  X | I,rho.P[I;rho] ≡ X | I,rho.Q[I;rho] 
  supposing (∀I:fset(ℕ). ∀rho:X(I).  (P[I;rho] ⇐⇒ Q[I;rho])) ∧ cs-predicate(X;I,rho.P[I;rho])
BY
{ PresheafMLTTInstance Obid: sub-presheaf-set_functionality⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[P,Q:I:fset(\mBbbN{})  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  \mBbbP{}].
    X  |  I,rho.P[I;rho]  \mequiv{}  X  |  I,rho.Q[I;rho] 
    supposing  (\mforall{}I:fset(\mBbbN{}).  \mforall{}rho:X(I).    (P[I;rho]  \mLeftarrow{}{}\mRightarrow{}  Q[I;rho]))  \mwedge{}  cs-predicate(X;I,rho.P[I;rho])


By

---

Latex:
PresheafMLTTInstance  Obid:  sub-presheaf-set\_functionality\mcdot{}

---

Home Index