---

Step * 1 of Lemma dataflow-valueall-type


1. A : 𝕌'
2. B : Type
3. ↓A
4. A1 : 𝕌'@i 2
5. B1 : 𝕌'@i 2
6. A1 ≡ B1@i'
⊢ A ─→ (A1 × B) ≡ A ─→ (B1 × B)
BY
{ (D -1 THEN D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  Type
3.  \mdownarrow{}A
4.  A1  :  \mBbbU{}'@i  2
5.  B1  :  \mBbbU{}'@i  2
6.  A1  \mequiv{}  B1@i'
\mvdash{}  A  {}\mrightarrow{}  (A1  \mtimes{}  B)  \mequiv{}  A  {}\mrightarrow{}  (B1  \mtimes{}  B)


By

---

Latex:
(D  -1  THEN  D  0  THEN  Auto)

---

Home Index