---

Step * 2 of Lemma discrete-fun-bijection


1. [A] : Type
2. [B] : Type
3. b : {() ⊢ _:discr(A ⟶ B)}
⊢ ∃a:{() ⊢ _:(discr(A) ⟶ discr(B))}. (discrete-fun(a) = b ∈ {() ⊢ _:discr(A ⟶ B)})
BY
{ (D 0 With ⌜cubical-lam(();λI,alpha. (b(fst(alpha)) q(alpha)))⌝  THEN Auto) }

1
1. A : Type
2. B : Type
3. b : {() ⊢ _:discr(A ⟶ B)}
⊢ λI,alpha. (b(fst(alpha)) q(alpha)) ∈ {().discr(A) ⊢ _:(discr(B))p}

2
1. A : Type
2. B : Type
3. b : {() ⊢ _:discr(A ⟶ B)}
⊢ discrete-fun(cubical-lam(();λI,alpha. (b(fst(alpha)) q(alpha)))) = b ∈ {() ⊢ _:discr(A ⟶ B)}

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  b  :  \{()  \mvdash{}  \_:discr(A  {}\mrightarrow{}  B)\}
\mvdash{}  \mexists{}a:\{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}.  (discrete-fun(a)  =  b)


By

---

Latex:
(D  0  With  \mkleeneopen{}cubical-lam(();\mlambda{}I,alpha.  (b(fst(alpha))  q(alpha)))\mkleeneclose{}    THEN  Auto)

---

Home Index