---

Step * of Lemma bijection-equiv_wf

No Annotations
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[g:B ⟶ A].
  (∀[X:j⊢]. (bijection-equiv(X;A;B;f;g) ∈ {X ⊢ _:Equiv(discr(A);discr(B))})) supposing 
     ((∀a:A. ((g (f a)) = a ∈ A)) and 
     (∀b:B. ((f (g b)) = b ∈ B)))
BY
{ (Auto
   THEN (Assert λI,alpha. (f (snd(alpha))) ∈ {X.discr(A) ⊢ _:discr(B)} BY
               ((MemTypeCD THENW Auto) THEN RepUR ``discrete-cubical-type cube-context-adjoin`` 0 THEN Auto))
   THEN (Assert λI,alpha. (g (snd(alpha))) ∈ {X.discr(B) ⊢ _:discr(A)} BY
               ((MemTypeCD THENW Auto) THEN RepUR ``discrete-cubical-type cube-context-adjoin`` 0 THEN Auto))
   THEN (Assert cubical-lam(X;λI,alpha. (f (snd(alpha)))) ∈ {X ⊢ _:(discr(A) ⟶ discr(B))} BY
               Auto)
   THEN (Assert q = app((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p; λI,alpha. (g (snd(alpha)))) ∈ {X.discr(B) ⊢ _:(dis\000Ccr(B))p} BY
               ((CubicalTermEqual THENA Auto)
                THEN RepUR ``discrete-cubical-type cubical-app cubical-lam cubical-lambda`` 0
                THEN CsmUnfolding
                THEN RepUR ``cube-context-adjoin`` -1
                THEN Symmetry
                THEN BackThruSomeHyp))
   THEN ProveWfLemma) }

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}
⊢ (λ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)))))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[g:B  {}\mrightarrow{}  A].
    (\mforall{}[X:j\mvdash{}].  (bijection-equiv(X;A;B;f;g)  \mmember{}  \{X  \mvdash{}  \_:Equiv(discr(A);discr(B))\}))  supposing 
          ((\mforall{}a:A.  ((g  (f  a))  =  a))  and 
          (\mforall{}b:B.  ((f  (g  b))  =  b)))


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}I,alpha.  (f  (snd(alpha)))  \mmember{}  \{X.discr(A)  \mvdash{}  \_:discr(B)\}  BY
                          ((MemTypeCD  THENW  Auto)
                            THEN  RepUR  ``discrete-cubical-type  cube-context-adjoin``  0
                            THEN  Auto))
  THEN  (Assert  \mlambda{}I,alpha.  (g  (snd(alpha)))  \mmember{}  \{X.discr(B)  \mvdash{}  \_:discr(A)\}  BY
                          ((MemTypeCD  THENW  Auto)
                            THEN  RepUR  ``discrete-cubical-type  cube-context-adjoin``  0
                            THEN  Auto))
  THEN  (Assert  cubical-lam(X;\mlambda{}I,alpha.  (f  (snd(alpha))))  \mmember{}  \{X  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}  BY
                          Auto)
  THEN  (Assert  q  =  app((cubical-lam(X;\mlambda{}I,alpha.  (f  (snd(alpha)))))p;  \mlambda{}I,alpha.  (g  (snd(alpha))))  BY
                          ((CubicalTermEqual  THENA  Auto)
                            THEN  RepUR  ``discrete-cubical-type  cubical-app  cubical-lam  cubical-lambda``  0
                            THEN  CsmUnfolding
                            THEN  RepUR  ``cube-context-adjoin``  -1
                            THEN  Symmetry
                            THEN  BackThruSomeHyp))
  THEN  ProveWfLemma)

---

Home Index