---

Step * 1 of Lemma bij-contr_wf


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. B : {X ⊢ _}
4. f : {X ⊢ _:(A ⟶ B)}
5. g : {X ⊢ _:(B ⟶ A)}
6. cA : X +⊢ Compositon(A)
7. b : {X.A ⊢ _:(Path_(A)p app((g)p; app((f)p; q)) q)}
8. c : {X ⊢ _:Contractible(B)}
9. {X.A ⊢ _:((A ⟶ B))p} = {X.A ⊢ _:((A)p ⟶ (B)p)} ∈ 𝕌{[i' | j']}
10. {X.A ⊢ _:((B ⟶ A))p} = {X.A ⊢ _:((B)p ⟶ (A)p)} ∈ 𝕌{[i' | j']}
11. (f)p ∈ {X.A ⊢ _:((A)p ⟶ (B)p)}
12. (g)p ∈ {X.A ⊢ _:((B)p ⟶ (A)p)}
13. app(g; contr-center(c)) ∈ {X ⊢ _:A}
⊢ map-path(X.A;(g)p;contr-path((c)p;app((f)p; q)))
  ∈ {X.A ⊢ _:(Path_(A)p (app(g; contr-center(c)))p app((g)p; app((f)p; q)))}
BY
{ (InstLemmaIJ `map-path_wf` [⌜X.A⌝;⌜(B)p⌝;⌜(A)p⌝;⌜(g)p⌝;⌜(contr-center(c))p⌝;⌜app((f)p; q)⌝;
   ⌜contr-path((c)p;app((f)p; q))⌝]⋅
   THENA Auto
   ) }

1
.....wf..... 
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. B : {X ⊢ _}
4. f : {X ⊢ _:(A ⟶ B)}
5. g : {X ⊢ _:(B ⟶ A)}
6. cA : X +⊢ Compositon(A)
7. b : {X.A ⊢ _:(Path_(A)p app((g)p; app((f)p; q)) q)}
8. c : {X ⊢ _:Contractible(B)}
9. {X.A ⊢ _:((A ⟶ B))p} = {X.A ⊢ _:((A)p ⟶ (B)p)} ∈ 𝕌{[i' | j']}
10. {X.A ⊢ _:((B ⟶ A))p} = {X.A ⊢ _:((B)p ⟶ (A)p)} ∈ 𝕌{[i' | j']}
11. (f)p ∈ {X.A ⊢ _:((A)p ⟶ (B)p)}
12. (g)p ∈ {X.A ⊢ _:((B)p ⟶ (A)p)}
13. app(g; contr-center(c)) ∈ {X ⊢ _:A}
⊢ contr-path((c)p;app((f)p; q)) ∈ {X.A ⊢ _:(Path_(B)p (contr-center(c))p app((f)p; q))}

2
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. B : {X ⊢ _}
4. f : {X ⊢ _:(A ⟶ B)}
5. g : {X ⊢ _:(B ⟶ A)}
6. cA : X +⊢ Compositon(A)
7. b : {X.A ⊢ _:(Path_(A)p app((g)p; app((f)p; q)) q)}
8. c : {X ⊢ _:Contractible(B)}
9. {X.A ⊢ _:((A ⟶ B))p} = {X.A ⊢ _:((A)p ⟶ (B)p)} ∈ 𝕌{[i' | j']}
10. {X.A ⊢ _:((B ⟶ A))p} = {X.A ⊢ _:((B)p ⟶ (A)p)} ∈ 𝕌{[i' | j']}
11. (f)p ∈ {X.A ⊢ _:((A)p ⟶ (B)p)}
12. (g)p ∈ {X.A ⊢ _:((B)p ⟶ (A)p)}
13. app(g; contr-center(c)) ∈ {X ⊢ _:A}
14. map-path(X.A;(g)p;contr-path((c)p;app((f)p; q)))
    ∈ {X.A ⊢ _:(Path_(A)p app((g)p; (contr-center(c))p) app((g)p; app((f)p; q)))}
⊢ map-path(X.A;(g)p;contr-path((c)p;app((f)p; q)))
  ∈ {X.A ⊢ _:(Path_(A)p (app(g; contr-center(c)))p app((g)p; app((f)p; q)))}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X  \mvdash{}  \_\}
4.  f  :  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}
5.  g  :  \{X  \mvdash{}  \_:(B  {}\mrightarrow{}  A)\}
6.  cA  :  X  +\mvdash{}  Compositon(A)
7.  b  :  \{X.A  \mvdash{}  \_:(Path\_(A)p  app((g)p;  app((f)p;  q))  q)\}
8.  c  :  \{X  \mvdash{}  \_:Contractible(B)\}
9.  \{X.A  \mvdash{}  \_:((A  {}\mrightarrow{}  B))p\}  =  \{X.A  \mvdash{}  \_:((A)p  {}\mrightarrow{}  (B)p)\}
10.  \{X.A  \mvdash{}  \_:((B  {}\mrightarrow{}  A))p\}  =  \{X.A  \mvdash{}  \_:((B)p  {}\mrightarrow{}  (A)p)\}
11.  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:((A)p  {}\mrightarrow{}  (B)p)\}
12.  (g)p  \mmember{}  \{X.A  \mvdash{}  \_:((B)p  {}\mrightarrow{}  (A)p)\}
13.  app(g;  contr-center(c))  \mmember{}  \{X  \mvdash{}  \_:A\}
\mvdash{}  map-path(X.A;(g)p;contr-path((c)p;app((f)p;  q)))
    \mmember{}  \{X.A  \mvdash{}  \_:(Path\_(A)p  (app(g;  contr-center(c)))p  app((g)p;  app((f)p;  q)))\}


By

---

Latex:
(InstLemmaIJ  `map-path\_wf`  [\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(g)p\mkleeneclose{};\mkleeneopen{}(contr-center(c))p\mkleeneclose{};\mkleeneopen{}app((f)p;  q)\mkleeneclose{};
  \mkleeneopen{}contr-path((c)p;app((f)p;  q))\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index