---

Step * of Lemma sub-cubical-set-and

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

---

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]  |  I,rho.Q[I;rho]  \mequiv{}  X  |  I,rho.P[I;rho]  \mwedge{}  Q[I;rho] 
    supposing  cs-predicate(X;I,rho.P[I;rho])  \mwedge{}  cs-predicate(X;I,rho.Q[I;rho])


By

---

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

---

Home Index