---

Step * of Lemma bij-contr_wf

No Annotations
∀X:j⊢. ∀A,B:{X ⊢ _}. ∀f:{X ⊢ _:(A ⟶ B)}. ∀g:{X ⊢ _:(B ⟶ A)}. ∀cA:X +⊢ Compositon(A).
∀b:{X.A ⊢ _:(Path_(A)p app((g)p; app((f)p; q)) q)}. ∀c:{X ⊢ _:Contractible(B)}.
  (bij-contr(X; A; f; g; cA; b; c) ∈ {X ⊢ _:Contractible(A)})
BY
{ (Intros
   THEN ((Assert {X.A ⊢ _:((A ⟶ B))p} = {X.A ⊢ _:((A)p ⟶ (B)p)} ∈ 𝕌{[i' | j']} BY
                (EqCDA THEN Auto))
         THEN (Assert {X.A ⊢ _:((B ⟶ A))p} = {X.A ⊢ _:((B)p ⟶ (A)p)} ∈ 𝕌{[i' | j']} BY
                     (EqCDA THEN Auto))
         )
   THEN (Assert (f)p ∈ {X.A ⊢ _:((A)p ⟶ (B)p)} BY
               ((Assert (f)p ∈ {X.A ⊢ _:((A ⟶ B))p} BY Auto) THEN InferEqualType THEN Eq))
   THEN (Assert (g)p ∈ {X.A ⊢ _:((B)p ⟶ (A)p)} BY
               ((Assert (g)p ∈ {X.A ⊢ _:((B ⟶ A))p} BY Auto) THEN InferEqualType THEN Eq))
   THEN ((Assert app(g; contr-center(c)) ∈ {X ⊢ _:A} BY Auto) ORELSE Auto)
   THEN ProveWfLemma) }

1
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)))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}A,B:\{X  \mvdash{}  \_\}.  \mforall{}f:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}.  \mforall{}g:\{X  \mvdash{}  \_:(B  {}\mrightarrow{}  A)\}.  \mforall{}cA:X  +\mvdash{}  Compositon(A).
\mforall{}b:\{X.A  \mvdash{}  \_:(Path\_(A)p  app((g)p;  app((f)p;  q))  q)\}.  \mforall{}c:\{X  \mvdash{}  \_:Contractible(B)\}.
    (bij-contr(X;  A;  f;  g;  cA;  b;  c)  \mmember{}  \{X  \mvdash{}  \_:Contractible(A)\})


By

---

Latex:
(Intros
  THEN  ((Assert  \{X.A  \mvdash{}  \_:((A  {}\mrightarrow{}  B))p\}  =  \{X.A  \mvdash{}  \_:((A)p  {}\mrightarrow{}  (B)p)\}  BY
                            (EqCDA  THEN  Auto))
              THEN  (Assert  \{X.A  \mvdash{}  \_:((B  {}\mrightarrow{}  A))p\}  =  \{X.A  \mvdash{}  \_:((B)p  {}\mrightarrow{}  (A)p)\}  BY
                                      (EqCDA  THEN  Auto))
              )
  THEN  (Assert  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:((A)p  {}\mrightarrow{}  (B)p)\}  BY
                          ((Assert  (f)p  \mmember{}  \{X.A  \mvdash{}  \_:((A  {}\mrightarrow{}  B))p\}  BY  Auto)  THEN  InferEqualType  THEN  Eq))
  THEN  (Assert  (g)p  \mmember{}  \{X.A  \mvdash{}  \_:((B)p  {}\mrightarrow{}  (A)p)\}  BY
                          ((Assert  (g)p  \mmember{}  \{X.A  \mvdash{}  \_:((B  {}\mrightarrow{}  A))p\}  BY  Auto)  THEN  InferEqualType  THEN  Eq))
  THEN  ((Assert  app(g;  contr-center(c))  \mmember{}  \{X  \mvdash{}  \_:A\}  BY  Auto)  ORELSE  Auto)
  THEN  ProveWfLemma)

---

Home Index