---

Step * of Lemma equiv-bijection-equiv

∀[A,B:Type]. ∀[e:A ~ B].
  ((((λe.<equiv-bijection(e), equiv-bijection-is(e)>) o (λe.bijection-equiv(();A;B;fst(e);bij_inv(snd(e))))) e)
  = e
  ∈ A ~ B)
BY
{ (RepUR ``compose equiv-bijection bijection-equiv equiv-witness equiv-fun discrete-fun`` 0
   THEN RepUR ``cubical-pair cubical-lam cubical-lambda cubical-term-at cubical-fst`` 0
   THEN RepUR ``trivial-cube-set cc-adjoin-cube equiv-bijection-is equiv-contr`` 0
   THEN RepUR ``cubical-app cubical-snd fiber-point cubical-fst cubical-pair contr-witness`` 0
   THEN RepUR ``discrete-cubical-term cubical-term-at`` 0
   THEN Auto) }

1
1. A : Type
2. B : Type
3. e : A ~ B
⊢ <λu.((fst(e)) u), λa1,a2,eq. Ax, λb.<bij_inv(snd(e)) b, Ax>> = e ∈ A ~ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[e:A  \msim{}  B].
    ((((\mlambda{}e.<equiv-bijection(e),  equiv-bijection-is(e)>)
          o  (\mlambda{}e.bijection-equiv(();A;B;fst(e);bij\_inv(snd(e))))) 
        e)
    =  e)


By

---

Latex:
(RepUR  ``compose  equiv-bijection  bijection-equiv  equiv-witness  equiv-fun  discrete-fun``  0
  THEN  RepUR  ``cubical-pair  cubical-lam  cubical-lambda  cubical-term-at  cubical-fst``  0
  THEN  RepUR  ``trivial-cube-set  cc-adjoin-cube  equiv-bijection-is  equiv-contr``  0
  THEN  RepUR  ``cubical-app  cubical-snd  fiber-point  cubical-fst  cubical-pair  contr-witness``  0
  THEN  RepUR  ``discrete-cubical-term  cubical-term-at``  0
  THEN  Auto)

---

Home Index