Step
*
1
1
1
1
1
1
2
1
1
2
1
5
1
1
1
2
1
1
1
4
1
2
2
1
1
1
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}
12. 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 q q)}
13. q ∈ {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:(Fiber((cubical-lam(X;λI,alpha. (f (snd(al\000Cpha)))))p;q))p}
14. (fiber-point(λI,alpha. (g (snd(alpha)));refl(q)))p ∈ {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;\000Cq) ⊢ _
:(Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q))p}
15. (Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q))p
= X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p\000C)p;(q)p)
∈ {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _}
16. {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:(Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)\000C))))p;q))p}
= {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))\000C))p)p;(q)p)}
∈ 𝕌{[i' | j']}
17. {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)\000C))))p)p;(q)p)}
= {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))\000C))p)p;(q)p)}
∈ 𝕌{[i' | j']}
18. F : {X.discr(B) ⊢ _}
19. ((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p ∈ {X.discr(B).F ⊢ _:(((discr(A))p)p ⟶ ((discr(B))p)p)}
20. fbr : {X.discr(B).F ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p;(q)p)}
21. fiber-path(fbr) ∈ {X.discr(B).F ⊢ _:(Path_((discr(B))p)p (q)p app(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p;
fiber-member(fbr)))}
22. ∀a:{X.discr(B).F ⊢ _:discr(B)}
∀[b:{X.discr(B).F ⊢ _:discr(B)}]. ∀[p:{X.discr(B).F ⊢ _:(Path_discr(B) a b)}].
(a = b ∈ {X.discr(B).F ⊢ _:discr(B)})
23. (q)p = app(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p; fiber-member(fbr)) ∈ {X.discr(B).F ⊢ _:discr(B)}
24. ((cubical-lam(X;λI,alpha. (g (snd(alpha)))))p)p ∈ {X.discr(B).F ⊢ _:(((discr(B))p)p ⟶ ((discr(A))p)p)}
25. app(((cubical-lam(X;λI,alpha. (g (snd(alpha)))))p)p; (q)p)
= app(((cubical-lam(X;λI,alpha. (g (snd(alpha)))))p)p; app(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p; fiber-member\000C(fbr)))
∈ {X.discr(B).F ⊢ _:discr(A)}
26. I : fset(ℕ)
27. a : X.discr(B).F(I)
⊢ (g (snd(fst(a)))) = (g (snd(fst(a)))) ∈ discr(A)(a)
BY
{ (RepUR ``discrete-cubical-type`` 0 THEN RepUR ``cube-context-adjoin discrete-cubical-type`` -1) }
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}
12. 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 q q)}
13. q ∈ {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:(Fiber((cubical-lam(X;λI,alpha. (f (snd(al\000Cpha)))))p;q))p}
14. (fiber-point(λI,alpha. (g (snd(alpha)));refl(q)))p ∈ {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;\000Cq) ⊢ _
:(Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q))p}
15. (Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q))p
= X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p\000C)p;(q)p)
∈ {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _}
16. {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:(Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)\000C))))p;q))p}
= {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))\000C))p)p;(q)p)}
∈ 𝕌{[i' | j']}
17. {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)\000C))))p)p;(q)p)}
= {X.discr(B).Fiber((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p;q) ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))\000C))p)p;(q)p)}
∈ 𝕌{[i' | j']}
18. F : {X.discr(B) ⊢ _}
19. ((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p ∈ {X.discr(B).F ⊢ _:(((discr(A))p)p ⟶ ((discr(B))p)p)}
20. fbr : {X.discr(B).F ⊢ _:Fiber(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p;(q)p)}
21. fiber-path(fbr) ∈ {X.discr(B).F ⊢ _:(Path_((discr(B))p)p (q)p app(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p;
fiber-member(fbr)))}
22. ∀a:{X.discr(B).F ⊢ _:discr(B)}
∀[b:{X.discr(B).F ⊢ _:discr(B)}]. ∀[p:{X.discr(B).F ⊢ _:(Path_discr(B) a b)}].
(a = b ∈ {X.discr(B).F ⊢ _:discr(B)})
23. (q)p = app(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p; fiber-member(fbr)) ∈ {X.discr(B).F ⊢ _:discr(B)}
24. ((cubical-lam(X;λI,alpha. (g (snd(alpha)))))p)p ∈ {X.discr(B).F ⊢ _:(((discr(B))p)p ⟶ ((discr(A))p)p)}
25. app(((cubical-lam(X;λI,alpha. (g (snd(alpha)))))p)p; (q)p)
= app(((cubical-lam(X;λI,alpha. (g (snd(alpha)))))p)p; app(((cubical-lam(X;λI,alpha. (f (snd(alpha)))))p)p; fiber-member\000C(fbr)))
∈ {X.discr(B).F ⊢ _:discr(A)}
26. I : fset(ℕ)
27. a : alpha:alpha:X(I) × B × F(alpha)
⊢ (g (snd(fst(a)))) = (g (snd(fst(a)))) ∈ A
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))))
12. refl(q) \mmember{} \{X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q) \mvdash{} \_
:(Path\_(Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q))p q q)\}
13. q \mmember{} \{X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q) \mvdash{} \_
:(Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q))p\}
14. (fiber-point(\mlambda{}I,alpha. (g (snd(alpha)));refl(q)))p
\mmember{} \{X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q) \mvdash{} \_
:(Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q))p\}
15. (Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q))p
= X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;
q) \mvdash{} Fiber(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p;(q)p)
16. \{X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q) \mvdash{} \_
:(Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q))p\}
= \{X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q) \mvdash{} \_
:Fiber(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p;(q)p)\}
17. \{X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q) \mvdash{} \_
:Fiber(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p;(q)p)\}
= \{X.discr(B).Fiber((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p;q) \mvdash{} \_
:Fiber(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p;(q)p)\}
18. F : \{X.discr(B) \mvdash{} \_\}
19. ((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p \mmember{} \{X.discr(B).F \mvdash{} \_:(((discr(A))p)p {}\mrightarrow{} ((discr(B\000C))p)p)\}
20. fbr : \{X.discr(B).F \mvdash{} \_:Fiber(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p;(q)p)\}
21. fiber-path(fbr) \mmember{} \{X.discr(B).F \mvdash{} \_:(Path\_((discr(B))p)p (q)p
app(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p;
fiber-member(fbr)))\}
22. \mforall{}a:\{X.discr(B).F \mvdash{} \_:discr(B)\}
\mforall{}[b:\{X.discr(B).F \mvdash{} \_:discr(B)\}]. \mforall{}[p:\{X.discr(B).F \mvdash{} \_:(Path\_discr(B) a b)\}]. (a = b)
23. (q)p = app(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha)))))p)p; fiber-member(fbr))
24. ((cubical-lam(X;\mlambda{}I,alpha. (g (snd(alpha)))))p)p \mmember{} \{X.discr(B).F \mvdash{} \_:(((discr(B))p)p {}\mrightarrow{} ((discr(A\000C))p)p)\}
25. app(((cubical-lam(X;\mlambda{}I,alpha. (g (snd(alpha)))))p)p; (q)p)
= app(((cubical-lam(X;\mlambda{}I,alpha. (g (snd(alpha)))))p)p; app(((cubical-lam(X;\mlambda{}I,alpha. (f (snd(alpha))\000C)))p)p;
fiber-member(fbr)))
26. I : fset(\mBbbN{})
27. a : X.discr(B).F(I)
\mvdash{} (g (snd(fst(a)))) = (g (snd(fst(a))))
By
Latex:
(RepUR ``discrete-cubical-type`` 0 THEN RepUR ``cube-context-adjoin discrete-cubical-type`` -1)
Home
Index