---

Step * of Lemma bijection-preserves-contractible

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)}.
  {X ⊢ _:Contractible(A)}
BY
{ (Intros THEN Try ((UseWitness ⌜bij-contr(X; A; f; g; cA; b; c)⌝⋅ THEN Auto))) }

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


By

---

Latex:
(Intros  THEN  Try  ((UseWitness  \mkleeneopen{}bij-contr(X;  A;  f;  g;  cA;  b;  c)\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index