---

Step * 2 1 of Lemma discrete-fun-bijection


1. A : Type
2. B : Type
3. b : {() ⊢ _:discr(A ⟶ B)}
⊢ λI,alpha. (b(fst(alpha)) q(alpha)) ∈ {().discr(A) ⊢ _:(discr(B))p}
BY
{ (D -1 THEN (RWO  "csm-discrete-cubical-type" 0 THENA Auto)) }

1
1. A : Type
2. B : Type
3. b : I:fset(ℕ) ⟶ a:()(I) ⟶ discr(A ⟶ B)(a)
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:()(I).  ((b I a a f) = (b J f(a)) ∈ discr(A ⟶ B)(f(a)))
⊢ λI,alpha. (b(fst(alpha)) q(alpha)) ∈ {().discr(A) ⊢ _:discr(B)}

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  b  :  \{()  \mvdash{}  \_:discr(A  {}\mrightarrow{}  B)\}
\mvdash{}  \mlambda{}I,alpha.  (b(fst(alpha))  q(alpha))  \mmember{}  \{().discr(A)  \mvdash{}  \_:(discr(B))p\}


By

---

Latex:
(D  -1  THEN  (RWO    "csm-discrete-cubical-type"  0  THENA  Auto))

---

Home Index