---

Step * 1 of Lemma bijection-equiv_wf


1. A : Type
2. B : Type
3. f : A ⟶ B
4. g : B ⟶ A
5. ∀b:B. ((f (g b)) = b ∈ B)
6. ∀a:A. ((g (f a)) = a ∈ A)
7. X : CubicalSet{j}
8. λI,alpha. (f (snd(alpha))) ∈ {X.discr(A) ⊢ _:discr(B)}
9. λI,alpha. (g (snd(alpha))) ∈ {X.discr(B) ⊢ _:discr(A)}
10. cubical-lam(X;λI,alpha. (f (snd(alpha)))) ∈ {X ⊢ _:(discr(A) ⟶ discr(B))}
11. q = app((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p; λI,alpha. (g (snd(alpha)))) ∈ {X.discr(B) ⊢ _:(discr(B))p}
⊢ (λcontr-witness(X.discr(B);fiber-point(λI,alpha. (g (snd(alpha)));refl(q));refl(q)))
  ∈ {X ⊢ _:IsEquiv(discr(A);discr(B);cubical-lam(X;λI,alpha. (f (snd(alpha)))))}
BY
{ (Unfold `is-cubical-equiv` 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. g : B ⟶ A
5. ∀b:B. ((f (g b)) = b ∈ B)
6. ∀a:A. ((g (f a)) = a ∈ A)
7. X : CubicalSet{j}
8. λI,alpha. (f (snd(alpha))) ∈ {X.discr(A) ⊢ _:discr(B)}
9. λI,alpha. (g (snd(alpha))) ∈ {X.discr(B) ⊢ _:discr(A)}
10. cubical-lam(X;λI,alpha. (f (snd(alpha)))) ∈ {X ⊢ _:(discr(A) ⟶ discr(B))}
11. q = app((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p; λI,alpha. (g (snd(alpha)))) ∈ {X.discr(B) ⊢ _:(discr(B))p}
⊢ refl(q) ∈ {X.discr(B) ⊢ _:(Path_(discr(B))p q app((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p; λI,alpha. (g (snd(alph\000Ca)))))}

2
1. A : Type
2. B : Type
3. f : A ⟶ B
4. g : B ⟶ A
5. ∀b:B. ((f (g b)) = b ∈ B)
6. ∀a:A. ((g (f a)) = a ∈ A)
7. X : CubicalSet{j}
8. λI,alpha. (f (snd(alpha))) ∈ {X.discr(A) ⊢ _:discr(B)}
9. λI,alpha. (g (snd(alpha))) ∈ {X.discr(B) ⊢ _:discr(A)}
10. cubical-lam(X;λI,alpha. (f (snd(alpha)))) ∈ {X ⊢ _:(discr(A) ⟶ discr(B))}
11. q = app((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p; λI,alpha. (g (snd(alpha)))) ∈ {X.discr(B) ⊢ _:(discr(B))p}
⊢ refl(q) ∈ {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _
             :(Path_(Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q))p (fiber-point(λI,alpha. (g (snd(alpha)));ref\000Cl(q)))p q)}

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  g  :  B  {}\mrightarrow{}  A
5.  \mforall{}b:B.  ((f  (g  b))  =  b)
6.  \mforall{}a:A.  ((g  (f  a))  =  a)
7.  X  :  CubicalSet\{j\}
8.  \mlambda{}I,alpha.  (f  (snd(alpha)))  \mmember{}  \{X.discr(A)  \mvdash{}  \_:discr(B)\}
9.  \mlambda{}I,alpha.  (g  (snd(alpha)))  \mmember{}  \{X.discr(B)  \mvdash{}  \_:discr(A)\}
10.  cubical-lam(X;\mlambda{}I,alpha.  (f  (snd(alpha))))  \mmember{}  \{X  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
11.  q  =  app((cubical-lam(X;\mlambda{}I,alpha.  (f  (snd(alpha)))))p;  \mlambda{}I,alpha.  (g  (snd(alpha))))
\mvdash{}  (\mlambda{}contr-witness(X.discr(B);fiber-point(\mlambda{}I,alpha.  (g  (snd(alpha)));refl(q));refl(q)))
    \mmember{}  \{X  \mvdash{}  \_:IsEquiv(discr(A);discr(B);cubical-lam(X;\mlambda{}I,alpha.  (f  (snd(alpha)))))\}


By

---

Latex:
(Unfold  `is-cubical-equiv`  0  THEN  Auto)

---

Home Index