---

Step * of Lemma discrete-pi-equiv

No Annotations
∀A:Type. ∀B:A ⟶ Type. ∀X:j⊢.  {X ⊢ _:Equiv(Πdiscr(A) discrete-family(A;a.B[a]);discr(a:A ⟶ B[a]))}
BY
{ ((Intros) CollapseTHEN (Assert discrete-function(q) ∈ {X.Πdiscr(A) discrete-family(A;a.B[a]) ⊢ _
                                                         :(discr(a:A ⟶ B[a]))p}⋅))⋅ }

1
.....assertion..... 
1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
⊢ discrete-function(q) ∈ {X.Πdiscr(A) discrete-family(A;a.B[a]) ⊢ _:(discr(a:A ⟶ B[a]))p}

2
1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. discrete-function(q) ∈ {X.Πdiscr(A) discrete-family(A;a.B[a]) ⊢ _:(discr(a:A ⟶ B[a]))p}
⊢ {X ⊢ _:Equiv(Πdiscr(A) discrete-family(A;a.B[a]);discr(a:A ⟶ B[a]))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}X:j\mvdash{}.    \{X  \mvdash{}  \_:Equiv(\mPi{}discr(A)  discrete-family(A;a.B[a]);discr(a:A  {}\mrightarrow{}  B[a]))\}


By

---

Latex:
((Intros)  CollapseTHEN  (Assert  discrete-function(q)  \mmember{}  \{X.\mPi{}discr(A)  discrete-family(A;a.B[a])  \mvdash{}  \_
                                                                                                              :(discr(a:A  {}\mrightarrow{}  B[a]))p\}\mcdot{}))\mcdot{}

---

Home Index