---

Step * of Lemma cubical-fun-family-discrete

No Annotations
∀[A,B:Type]. ∀[X:j⊢]. ∀[I:fset(ℕ)]. ∀[a:X(I)].
  (cubical-fun-family(X; discr(A); discr(B); I; a)
  = {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
  ∈ Type)
BY
{ PresheafMLTTInstance Obid: presheaf-fun-family-discrete⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].
    (cubical-fun-family(X;  discr(A);  discr(B);  I;  a)
    =  \{w:J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  u:A  {}\mrightarrow{}  B| 
          \mforall{}J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}u:A.    ((w  J  f  u)  =  (w  K  f  \mcdot{}  g  u))\}  )


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-fun-family-discrete\mcdot{}

---

Home Index