Proof of Nuprl Lemma : fillpath

Step * 1 1 1 1 2 of Lemma fillpath_wf

1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
6. x : {Gamma ⊢ _:(A)[1(𝕀)]}
7. y : {Gamma ⊢ _:(A)[0(𝕀)]}
8. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
9. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
10. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (x)p ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}
14. (y)p ∈ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}

15. ∀[u:{Gamma.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:(A)p+}]. ∀[a0:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ (u)[0(𝕀)]]}].

      (comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ u] a0 ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ (u)[1(𝕀)]]})

16. ∀[a0:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[0(𝕀)])p;

                                                        q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[0(𝕀)])p]]}]

(comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ [(q)p=0 ⊢→ (app(fill-type-down(Gamma;A;cA); (x)p))p+;

                                        (q)p=1 ⊢→ (app(fill-type-up(Gamma;A;cA); (y)p))p+]] a0

       ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[1(𝕀)])p;

                                                        q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[1(𝕀)])p]]})

17. {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[0(𝕀)])p;

                                                   q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[0(𝕀)])p]]}

= {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 ⊢→ (y)p]]}

∈ 𝕌{[i | j']}

18. {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[1(𝕀)])p;

                                                   q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[1(𝕀)])p]]}

= {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (x)p; q=1 ⊢→ (app(transport-fun(Gamma;A;cA); y))p]]}

∈ 𝕌{[i | j']}

19. z ∈ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 ⊢→ (y)p]]}

⊢ comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ [(q)p=0 ⊢→ (app(fill-type-down(Gamma;A;cA); (x)p))p+;

                                   (q)p=1 ⊢→ (app(fill-type-up(Gamma;A;cA); (y)p))p+]] z

∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}|

     ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]}) ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})}

BY
{ (InstHyp [⌜z⌝] (-4)⋅ THENA InferEqualTypeGen) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
6. x : {Gamma ⊢ _:(A)[1(𝕀)]}
7. y : {Gamma ⊢ _:(A)[0(𝕀)]}
8. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
9. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
10. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (x)p ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}
14. (y)p ∈ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}

15. ∀[u:{Gamma.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:(A)p+}]. ∀[a0:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ (u)[0(𝕀)]]}].

      (comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ u] a0 ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ (u)[1(𝕀)]]})

16. ∀[a0:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[0(𝕀)])p;

                                                        q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[0(𝕀)])p]]}]

(comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ [(q)p=0 ⊢→ (app(fill-type-down(Gamma;A;cA); (x)p))p+;

                                        (q)p=1 ⊢→ (app(fill-type-up(Gamma;A;cA); (y)p))p+]] a0

       ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[1(𝕀)])p;

                                                        q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[1(𝕀)])p]]})

17. {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[0(𝕀)])p;

                                                   q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[0(𝕀)])p]]}

= {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 ⊢→ (y)p]]}

∈ 𝕌{[i | j']}

18. {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[1(𝕀)])p;

                                                   q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[1(𝕀)])p]]}

= {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (x)p; q=1 ⊢→ (app(transport-fun(Gamma;A;cA); y))p]]}

∈ 𝕌{[i | j']}

19. z ∈ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 ⊢→ (y)p]]}

⊢ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 ⊢→ (y)p]]}

= {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[0(𝕀)])p;

                                                 q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[0(𝕀)])p]]}

∈ 𝕌{[i | j']}

2
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
6. x : {Gamma ⊢ _:(A)[1(𝕀)]}
7. y : {Gamma ⊢ _:(A)[0(𝕀)]}
8. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
9. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
10. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (x)p ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}
14. (y)p ∈ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}

15. ∀[u:{Gamma.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:(A)p+}]. ∀[a0:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ (u)[0(𝕀)]]}].

      (comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ u] a0 ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ (u)[1(𝕀)]]})

16. ∀[a0:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[0(𝕀)])p;

                                                        q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[0(𝕀)])p]]}]

(comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ [(q)p=0 ⊢→ (app(fill-type-down(Gamma;A;cA); (x)p))p+;

                                        (q)p=1 ⊢→ (app(fill-type-up(Gamma;A;cA); (y)p))p+]] a0

       ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[1(𝕀)])p;

                                                        q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[1(𝕀)])p]]})

17. {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[0(𝕀)])p;

                                                   q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[0(𝕀)])p]]}

= {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 ⊢→ (y)p]]}

∈ 𝕌{[i | j']}

18. {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[1(𝕀)])p;

                                                   q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[1(𝕀)])p]]}

= {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (x)p; q=1 ⊢→ (app(transport-fun(Gamma;A;cA); y))p]]}

∈ 𝕌{[i | j']}

19. z ∈ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 ⊢→ (y)p]]}

20. comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ [(q)p=0 ⊢→ (app(fill-type-down(Gamma;A;cA); (x)p))p+;

                                     (q)p=1 ⊢→ (app(fill-type-up(Gamma;A;cA); (y)p))p+]] z

    ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p[((q=0) ∨ (q=1)) |⟶ [q=0 ⊢→ ((app(fill-type-down(Gamma;A;cA); (x)p))[1(𝕀)])p;

                                                     q=1 ⊢→ ((app(fill-type-up(Gamma;A;cA); (y)p))[1(𝕀)])p]]}

⊢ comp (cA)p+ [((q=0) ∨ (q=1)) ⊢→ [(q)p=0 ⊢→ (app(fill-type-down(Gamma;A;cA); (x)p))p+;

                                   (q)p=1 ⊢→ (app(fill-type-up(Gamma;A;cA); (y)p))p+]] z

∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}|

     ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]}) ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})}

Latex:

Latex:
1. Gamma : CubicalSet\{j\} 2. A : \{Gamma.\mBbbI{} \mvdash{} \_\} 3. cA : Gamma.\mBbbI{} \mvdash{} CompOp(A) 4. Gamma.\mBbbI{} \mvdash{} ((A)[0(\mBbbI{})])p 5. Gamma.\mBbbI{} \mvdash{} ((A)[1(\mBbbI{})])p 6. x : \{Gamma \mvdash{} \_:(A)[1(\mBbbI{})]\} 7. y : \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\} 8. z : \{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p\} 9. (z)[1(\mBbbI{})] \mmember{} \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\} 10. (z)[0(\mBbbI{})] \mmember{} \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\} 11. (z)[1(\mBbbI{})] = y 12. (z)[0(\mBbbI{})] = app(rev-transport-fun(Gamma;A;cA); x) 13. (x)p \mmember{} \{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p\} 14. (y)p \mmember{} \{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p\} 15. \mforall{}[u:\{Gamma.\mBbbI{}, ((q=0) \mvee{} (q=1)).\mBbbI{} \mvdash{} \_:(A)p+\}]. \mforall{}[a0:\{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}]. (comp (cA)p+ [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} u] a0 \mmember{} \{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} (u)[1(\mBbbI{})]]\}) 16. \mforall{}[a0:\{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} [q=0 \mvdash{}\mrightarrow{} ((app(fill-type-down(Gamma;A;cA); (x)p))[0(\mBbbI{})])p; q=1 \mvdash{}\mrightarrow{} ((app(fill-type-up(Gamma;A;cA); (y)p))[0(\mBbbI{})])p]]\}] (comp (cA)p+ [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} [(q)p=0 \mvdash{}\mrightarrow{} (app(fill-type-down(Gamma;A;cA); (x)p))p+; (q)p=1 \mvdash{}\mrightarrow{} (app(fill-type-up(Gamma;A;cA); (y)p))p+]] a0 \mmember{} \{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} [q=0 \mvdash{}\mrightarrow{} ((app(fill-type-down(Gamma;A;cA); (x)p))[1(\mBbbI{})])p; q=1 \mvdash{}\mrightarrow{} ((app(fill-type-up(Gamma;A;cA); (y)p))[1(\mBbbI{})])p]]\}) 17. \{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} [q=0 \mvdash{}\mrightarrow{} ((app(fill-type-down(Gamma;A;cA); (x)p))[0(\mBbbI{})])p; q=1 \mvdash{}\mrightarrow{} ((app(fill-type-up(Gamma;A;cA); (y)p))[0(\mBbbI{})])p]]\} = \{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} [q=0 \mvdash{}\mrightarrow{} (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 \mvdash{}\mrightarrow{} (y)p]]\} 18. \{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} [q=0 \mvdash{}\mrightarrow{} ((app(fill-type-down(Gamma;A;cA); (x)p))[1(\mBbbI{})])p; q=1 \mvdash{}\mrightarrow{} ((app(fill-type-up(Gamma;A;cA); (y)p))[1(\mBbbI{})])p]]\} = \{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} [q=0 \mvdash{}\mrightarrow{} (x)p; q=1 \mvdash{}\mrightarrow{} (app(transport-fun(Gamma;A;cA); y))p]]\} 19. z \mmember{} \{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p[((q=0) \mvee{} (q=1)) |{}\mrightarrow{} [q=0 \mvdash{}\mrightarrow{} (app(rev-transport-fun(Gamma;A;cA); x))p; q=1 \mvdash{}\mrightarrow{} (y)p]]\} \mvdash{} comp (cA)p+ [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} [(q)p=0 \mvdash{}\mrightarrow{} (app(fill-type-down(Gamma;A;cA); (x)p))p+; (q)p=1 \mvdash{}\mrightarrow{} (app(fill-type-up(Gamma;A;cA); (y)p))p+]] z \mmember{} \{t:\{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p\}| ((t)[0(\mBbbI{})] = x) \mwedge{} ((t)[1(\mBbbI{})] = app(transport-fun(Gamma;A;cA); y))\} By Latex: (InstHyp [\mkleeneopen{}z\mkleeneclose{}] (-4)\mcdot{} THENA InferEqualTypeGen) Home Index