Proof of Nuprl Lemma : discrete-pi-equiv

Step * 2 3 1 1 1 1 1 1 1 2 3 1 1 1 1 1 1 1 1 1 1 1 1 1 1 of Lemma discrete-pi-equiv

1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. discrete-function(q) ∈ {X.Πdiscr(A) discrete-family(A;a.B[a]) ⊢ _:(discr(a:A ⟶ B[a]))p}
5. (Fiber((cubical-lam(X;discrete-function(q)))p;q))p
= X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;
q) ⊢ Fiber(((cubical-lam(X;discrete-function(q)))p)p;(q)p)
∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _}
6. q ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _
:(Fiber((cubical-lam(X;discrete-function(q)))p;q))p}
7. (q)p ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _:discr(a:A ⟶ B[a])}

8. ((cubical-lam(X;discrete-function(q)))p)p ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _

                                                :(((Πdiscr(A) discrete-family(A;a.B[a]))p)p ⟶ discr(a:A ⟶ B[a]))}

9. (Fiber((cubical-lam(X;discrete-function(q)))p;q))p
= X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;
                             q) ⊢ Fiber(((cubical-lam(X;discrete-function(q)))p)p;(q)p)
∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _}
10. q ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _
         :Fiber(((cubical-lam(X;discrete-function(q)))p)p;(q)p)}
11. app(((cubical-lam(X;discrete-function(q)))p)p; fiber-member(q))
= (q)p
∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _:discr(a:A ⟶ B[a])}
12. fiber-member(q) ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _
                       :((Πdiscr(A) discrete-family(A;a.B[a]))p)p}
13. v : {X.discr(a:A ⟶ B[a]) ⊢ _}

14. X.discr(a:A ⟶ B[a]) ⊢ Fiber((cubical-lam(X;discrete-function(q)))p;q) = v ∈ {X.discr(a:A ⟶ B[a]) ⊢ _}

15. (Πdiscr(A) discrete-family(A;a.B[a]))p
= X.discr(a:A ⟶ B[a]) ⊢ Πdiscr(A) discrete-family(A;a.B[a])
∈ {X.discr(a:A ⟶ B[a]) ⊢ _}
16. (Πdiscr(A) discrete-family(A;a.B[a]))p
= X.discr(a:A ⟶ B[a]).v ⊢ Π(discr(A))p (discrete-family(A;a.B[a]))(p o p;q)
∈ {X.discr(a:A ⟶ B[a]).v ⊢ _}
⊢ X.discr(a:A ⟶ B[a]).v ⊢ Πdiscr(A) discrete-family(A;a.B[a])
= ((Πdiscr(A) discrete-family(A;a.B[a]))p)p
∈ {X.discr(a:A ⟶ B[a]).v ⊢ _}
BY

{ ((RWO  "csm-discrete-cubical-type csm-discrete-family" (-1)) 
 CollapseTHENA (Auto⋅))⋅ }

1
1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. discrete-function(q) ∈ {X.Πdiscr(A) discrete-family(A;a.B[a]) ⊢ _:(discr(a:A ⟶ B[a]))p}
5. (Fiber((cubical-lam(X;discrete-function(q)))p;q))p
= X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;
q) ⊢ Fiber(((cubical-lam(X;discrete-function(q)))p)p;(q)p)
∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _}
6. q ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _
:(Fiber((cubical-lam(X;discrete-function(q)))p;q))p}
7. (q)p ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _:discr(a:A ⟶ B[a])}

8. ((cubical-lam(X;discrete-function(q)))p)p ∈ {X.discr(a:A ⟶ B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) ⊢ _

                                                :(((Πdiscr(A) discrete-family(A;a.B[a]))p)p ⟶ discr(a:A ⟶ B[a]))}

14. X.discr(a:A ⟶ B[a]) ⊢ Fiber((cubical-lam(X;discrete-function(q)))p;q) = v ∈ {X.discr(a:A ⟶ B[a]) ⊢ _}

15. (Πdiscr(A) discrete-family(A;a.B[a]))p
= X.discr(a:A ⟶ B[a]) ⊢ Πdiscr(A) discrete-family(A;a.B[a])
∈ {X.discr(a:A ⟶ B[a]) ⊢ _}
16. (Πdiscr(A) discrete-family(A;a.B[a]))p
= X.discr(a:A ⟶ B[a]).v ⊢ Πdiscr(A) discrete-family(A;a.B[a])
∈ {X.discr(a:A ⟶ B[a]).v ⊢ _}
⊢ X.discr(a:A ⟶ B[a]).v ⊢ Πdiscr(A) discrete-family(A;a.B[a])
= ((Πdiscr(A) discrete-family(A;a.B[a]))p)p
∈ {X.discr(a:A ⟶ B[a]).v ⊢ _}

Latex:

Latex:
1. A : Type 2. B : A {}\mrightarrow{} Type 3. X : CubicalSet\{j\} 4. discrete-function(q) \mmember{} \{X.\mPi{}discr(A) discrete-family(A;a.B[a]) \mvdash{} \_:(discr(a:A {}\mrightarrow{} B[a]))p\} 5. (Fiber((cubical-lam(X;discrete-function(q)))p;q))p = X.discr(a:A {}\mrightarrow{} B[a]).Fiber((cubical-lam(X;discrete-function(q)))p; q) \mvdash{} Fiber(((cubical-lam(X;discrete-function(q)))p)p;(q)p) 6. q \mmember{} \{X.discr(a:A {}\mrightarrow{} B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) \mvdash{} \_ :(Fiber((cubical-lam(X;discrete-function(q)))p;q))p\} 7. (q)p \mmember{} \{X.discr(a:A {}\mrightarrow{} B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) \mvdash{} \_:discr(a:A {}\mrightarrow{} B[a])\} 8. ((cubical-lam(X;discrete-function(q)))p)p \mmember{} \{X.discr(a:A {}\mrightarrow{} B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) \mvdash{} \_ :(((\mPi{}discr(A) discrete-family(A;a.B[a]))p)p {}\mrightarrow{} discr(a:A {}\mrightarrow{} B[a]))\} 9. (Fiber((cubical-lam(X;discrete-function(q)))p;q))p = X.discr(a:A {}\mrightarrow{} B[a]).Fiber((cubical-lam(X;discrete-function(q)))p; q) \mvdash{} Fiber(((cubical-lam(X;discrete-function(q)))p)p;(q)p) 10. q \mmember{} \{X.discr(a:A {}\mrightarrow{} B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) \mvdash{} \_ :Fiber(((cubical-lam(X;discrete-function(q)))p)p;(q)p)\} 11. app(((cubical-lam(X;discrete-function(q)))p)p; fiber-member(q)) = (q)p 12. fiber-member(q) \mmember{} \{X.discr(a:A {}\mrightarrow{} B[a]).Fiber((cubical-lam(X;discrete-function(q)))p;q) \mvdash{} \_ :((\mPi{}discr(A) discrete-family(A;a.B[a]))p)p\} 13. v : \{X.discr(a:A {}\mrightarrow{} B[a]) \mvdash{} \_\} 14. X.discr(a:A {}\mrightarrow{} B[a]) \mvdash{} Fiber((cubical-lam(X;discrete-function(q)))p;q) = v 15. (\mPi{}discr(A) discrete-family(A;a.B[a]))p = X.discr(a:A {}\mrightarrow{} B[a]) \mvdash{} \mPi{}discr(A) discrete-family(A;a.B[a]) 16. (\mPi{}discr(A) discrete-family(A;a.B[a]))p = X.discr(a:A {}\mrightarrow{} B[a]).v \mvdash{} \mPi{}(discr(A))p (discrete-family(A;a.B[a]))(p o p;q) \mvdash{} X.discr(a:A {}\mrightarrow{} B[a]).v \mvdash{} \mPi{}discr(A) discrete-family(A;a.B[a]) = ((\mPi{}discr(A) discrete-family(A;a.B[a]))p)p By Latex: ((RWO "csm-discrete-cubical-type csm-discrete-family" (-1)) CollapseTHENA (Auto\mcdot{}))\mcdot{} Home Index