---

Step * of Lemma dcff-inj-bijection

No Annotations
∀[A,B:Type]. ∀[X:j⊢]. ∀[I:fset(ℕ)]. ∀[a:X(I)].
  Bij(cubical-fun-family(X; discr(A); discr(B); I; a);A ⟶ B;λw.dcff-inj(I;w))
BY
{ PresheafMLTTInstance Obid: psdcff-inj-bijection⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].
    Bij(cubical-fun-family(X;  discr(A);  discr(B);  I;  a);A  {}\mrightarrow{}  B;\mlambda{}w.dcff-inj(I;w))


By

---

Latex:
PresheafMLTTInstance  Obid:  psdcff-inj-bijection\mcdot{}

---

Home Index