---

Step * 1 of Lemma bijection-preserves-contractible


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)
⊢ istype({X.A ⊢ _:(Path_(A)p app((g)p; app((f)p; q)) q)})
BY
{ (((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 Auto) }

---

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)
\mvdash{}  istype(\{X.A  \mvdash{}  \_:(Path\_(A)p  app((g)p;  app((f)p;  q))  q)\})


By

---

Latex:
(((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  Auto)

---

Home Index