---

Step * 2 2 of Lemma discrete-fun-bijection


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)}
BY
{ (Symmetry THEN (CubicalTermEqual THENA Auto)) }

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

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  b  :  \{()  \mvdash{}  \_:discr(A  {}\mrightarrow{}  B)\}
\mvdash{}  discrete-fun(cubical-lam(();\mlambda{}I,alpha.  (b(fst(alpha))  q(alpha))))  =  b


By

---

Latex:
(Symmetry  THEN  (CubicalTermEqual  THENA  Auto))

---

Home Index