---

Step * 1 of Lemma equiv-contr_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:Σ (T ⟶ A) IsEquiv((T)p;(A)p;q)}
5. a : {G ⊢ _:A}
6. f.2 ∈ {G ⊢ _:(IsEquiv((T)p;(A)p;q))[equiv-fun(f)]}
⊢ equiv-contr(f;a) ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
BY
{ (Unfold `is-cubical-equiv` -1 THEN Assert ⌜(q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}⌝⋅) }

1
.....assertion..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:Σ (T ⟶ A) IsEquiv((T)p;(A)p;q)}
5. a : {G ⊢ _:A}
6. f.2 ∈ {G ⊢ _:(Π(A)p Contractible(Fiber((q)p;q)))[equiv-fun(f)]}
⊢ (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}

2
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:Σ (T ⟶ A) IsEquiv((T)p;(A)p;q)}
5. a : {G ⊢ _:A}
6. f.2 ∈ {G ⊢ _:(Π(A)p Contractible(Fiber((q)p;q)))[equiv-fun(f)]}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
⊢ equiv-contr(f;a) ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  T  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:\mSigma{}  (T  {}\mrightarrow{}  A)  IsEquiv((T)p;(A)p;q)\}
5.  a  :  \{G  \mvdash{}  \_:A\}
6.  f.2  \mmember{}  \{G  \mvdash{}  \_:(IsEquiv((T)p;(A)p;q))[equiv-fun(f)]\}
\mvdash{}  equiv-contr(f;a)  \mmember{}  \{G  \mvdash{}  \_:Contractible(Fiber(equiv-fun(f);a))\}


By

---

Latex:
(Unfold  `is-cubical-equiv`  -1  THEN  Assert  \mkleeneopen{}(q)p  \mmember{}  \{G.(T  {}\mrightarrow{}  A).(A)p  \mvdash{}  \_:(((T)p)p  {}\mrightarrow{}  ((A)p)p)\}\mkleeneclose{}\mcdot{})

---

Home Index