---

Step * of Lemma discrete-fun_wf

No Annotations
∀[A,B:Type]. ∀[X:j⊢]. ∀[f:{X ⊢ _:(discr(A) ⟶ discr(B))}].  (discrete-fun(f) ∈ {X ⊢ _:discr(A ⟶ B)})
BY
{ (Auto THEN Unfold `discrete-fun` 0) }

1
1. A : Type
2. B : Type
3. X : CubicalSet{j}
4. f : {X ⊢ _:(discr(A) ⟶ discr(B))}
⊢ λI,alpha. (f I alpha I 1) ∈ {X ⊢ _:discr(A ⟶ B)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[X:j\mvdash{}].  \mforall{}[f:\{X  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}].
    (discrete-fun(f)  \mmember{}  \{X  \mvdash{}  \_:discr(A  {}\mrightarrow{}  B)\})


By

---

Latex:
(Auto  THEN  Unfold  `discrete-fun`  0)

---

Home Index