---

Step * of Lemma discrete-sigma-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-pair(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-pair(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-pair(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(\mSigma{}  discr(A)  discrete-family(A;a.B[a]);discr(a:A  \mtimes{}  B[a]))\}


By

---

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

---

Home Index