---

Step * of Lemma cube-set-map-is

No Annotations
∀[A,B:j⊢].
  (A j⟶ B ~ {trans:I:fset(ℕ) ⟶ A(I) ⟶ B(I)| 
              ∀I,J:fset(ℕ). ∀g:J ⟶ I.  ((λs.g(trans I s)) = (λs.(trans J g(s))) ∈ (A(I) ⟶ B(J)))} )
BY
{ PresheafMLTTInstance Obid: psc-map-is⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:j\mvdash{}].
    (A  j{}\mrightarrow{}  B  \msim{}  \{trans:I:fset(\mBbbN{})  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)| 
                            \mforall{}I,J:fset(\mBbbN{}).  \mforall{}g:J  {}\mrightarrow{}  I.    ((\mlambda{}s.g(trans  I  s))  =  (\mlambda{}s.(trans  J  g(s))))\}  )


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-map-is\mcdot{}

---

Home Index