---

Step * 1 of Lemma discrete-fun-at


1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. I : fset(ℕ)
5. a : ()(I)
⊢ (f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a)
BY
{ (PromoteHyp 4 3 THEN PromoteHyp 5 4) }

1
1. A : Type
2. B : Type
3. I : fset(ℕ)
4. a : ()(I)
5. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
⊢ (f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
4.  I  :  fset(\mBbbN{})
5.  a  :  ()(I)
\mvdash{}  (f  I  a)  =  (\mlambda{}J,h,u.  (f  \{\}  \mcdot{}  \{\}  1  u))


By

---

Latex:
(PromoteHyp  4  3  THEN  PromoteHyp  5  4)

---

Home Index