---

Step * 1 2 1 1 1 2 2 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 ⊢ _:Π(A)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
8. ((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a] = G ⊢ Contractible(Fiber(equiv-fun(f);a)) ∈ {G ⊢ _}
9. {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
= {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
∈ 𝕌{[i' | j']}
⊢ app(f.2; a) ∈ {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
BY
{ InstLemmaIJ `cubical-app_wf` [⌜G⌝;⌜(A)1(G)⌝;⌜(Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)⌝;⌜f.2⌝;⌜a⌝]⋅ }

1
.....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 ⊢ _:Π(A)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
8. ((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a] = G ⊢ Contractible(Fiber(equiv-fun(f);a)) ∈ {G ⊢ _}
9. {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
= {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
∈ 𝕌{[i' | j']}
⊢ G ij⊢

2
.....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 ⊢ _:Π(A)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
8. ((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a] = G ⊢ Contractible(Fiber(equiv-fun(f);a)) ∈ {G ⊢ _}
9. {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
= {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
∈ 𝕌{[i' | j']}
⊢ G ⊢ (A)1(G)

3
.....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 ⊢ _:Π(A)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
8. ((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a] = G ⊢ Contractible(Fiber(equiv-fun(f);a)) ∈ {G ⊢ _}
9. {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
= {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
∈ 𝕌{[i' | j']}
⊢ G.(A)1(G) ⊢ (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)

4
.....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 ⊢ _:Π(A)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
8. ((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a] = G ⊢ Contractible(Fiber(equiv-fun(f);a)) ∈ {G ⊢ _}
9. {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
= {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
∈ 𝕌{[i' | j']}
⊢ f.2 ∈ {G ⊢ _:Π(A)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}

5
.....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 ⊢ _:Π(A)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
8. ((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a] = G ⊢ Contractible(Fiber(equiv-fun(f);a)) ∈ {G ⊢ _}
9. {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
= {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
∈ 𝕌{[i' | j']}
⊢ a ∈ {G ⊢ _:(A)1(G)}

6
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)1(G) (Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q)}
7. (q)p ∈ {G.(T ⟶ A).(A)p ⊢ _:(((T)p)p ⟶ ((A)p)p)}
8. ((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a] = G ⊢ Contractible(Fiber(equiv-fun(f);a)) ∈ {G ⊢ _}
9. {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
= {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
∈ 𝕌{[i' | j']}
10. app(f.2; a) ∈ {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[a]}
⊢ app(f.2; a) ∈ {G ⊢ _:((Contractible(Fiber((q)p;q)))([equiv-fun(f)] o p;q))[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{}  \_:\mPi{}(A)1(G)  (Contractible(Fiber((q)p;q)))([equiv-fun(f)]  o  p;q)\}
7.  (q)p  \mmember{}  \{G.(T  {}\mrightarrow{}  A).(A)p  \mvdash{}  \_:(((T)p)p  {}\mrightarrow{}  ((A)p)p)\}
8.  ((Contractible(Fiber((q)p;q)))([equiv-fun(f)]  o  p;q))[a]
=  G  \mvdash{}  Contractible(Fiber(equiv-fun(f);a))
9.  \{G  \mvdash{}  \_:((Contractible(Fiber((q)p;q)))([equiv-fun(f)]  o  p;q))[a]\}
=  \{G  \mvdash{}  \_:Contractible(Fiber(equiv-fun(f);a))\}
\mvdash{}  app(f.2;  a)  \mmember{}  \{G  \mvdash{}  \_:((Contractible(Fiber((q)p;q)))([equiv-fun(f)]  o  p;q))[a]\}


By

---

Latex:
InstLemmaIJ  `cubical-app\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(A)1(G)\mkleeneclose{};\mkleeneopen{}(Contractible(Fiber((q)p;q)))([equiv-fun(f)]  o  p;q)\mkleeneclose{};
\mkleeneopen{}f.2\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}

---

Home Index