Proof of Nuprl Lemma : fillpath

Step * of Lemma fillpath_wf

No Annotations

∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)]. ∀[x:{Gamma ⊢ _:(A)[1(𝕀)]}]. ∀[y:{Gamma ⊢ _:(A)[0(𝕀)]}].

∀[z:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}].
(fillpath(Gamma;A;cA;x;y;z) ∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}|

                                 ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})

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

     (((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and
     ((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
BY
{ (RepeatFor 3 (Intro)
   THEN (Assert Gamma.𝕀 ⊢ ((A)[0(𝕀)])p BY
               Auto)
   THEN (Assert Gamma.𝕀 ⊢ ((A)[1(𝕀)])p BY
               Auto)
   THEN (RepeatFor 3 (Intro)
         THEN (Assert (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]} BY
                     (InferEqualType THEN Reduce 0 THEN Auto))
         THEN (Assert (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]} BY
                     (InferEqualType THEN Reduce 0 THEN Auto))
         THEN ((D 0 THENW Auto) THEN (D 0 THENW (EqualityIsType1 THEN Auto)))
         THEN (Assert (x)p ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p} BY
                     Auto)
         THEN (Assert (y)p ∈ {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p} BY
                     Auto))
   THEN Unfold `fillpath` 0

   THEN (InstLemmaIJ `composition-term_wf` [⌜Gamma.𝕀⌝;⌜((q=0) ∨ (q=1))⌝;⌜(A)p+⌝;⌜(cA)p+⌝]⋅ THENA Auto)

   THEN ((Subst' ((A)p+)[1(𝕀)] ~ ((A)[1(𝕀)])p -1 THENA (CsmUnfolding THEN Auto))
         THEN (Subst' ((A)p+)[0(𝕀)] ~ ((A)[0(𝕀)])p -1 THENA (CsmUnfolding THEN Auto))
         )
   THEN (InstHyp [⌜[(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+]⌝] (-1)⋅
         THENA (SubsumeC ⌜{Gamma.𝕀.𝕀, (((q)p=0) ∨ ((q)p=1)) ⊢ _:(A)p+}⌝⋅

                THENL [(MemCD THEN Auto); (RWW "csm-face-one< csm-face-zero< csm-face-or<" 0 THEN Auto)]

)
)) }

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)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+])[0(𝕀)]]}]

(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)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+])[1(𝕀)]]})

⊢ 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:
No Annotations \mforall{}[Gamma:j\mvdash{}]. \mforall{}[A:\{Gamma.\mBbbI{} \mvdash{} \_\}]. \mforall{}[cA:Gamma.\mBbbI{} \mvdash{} CompOp(A)]. \mforall{}[x:\{Gamma \mvdash{} \_:(A)[1(\mBbbI{})]\}]. \mforall{}[y:\{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\}]. \mforall{}[z:\{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p\}]. (fillpath(Gamma;A;cA;x;y;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))\} \000C) supposing (((z)[0(\mBbbI{})] = app(rev-transport-fun(Gamma;A;cA); x)) and ((z)[1(\mBbbI{})] = y)) By Latex: (RepeatFor 3 (Intro) THEN (Assert Gamma.\mBbbI{} \mvdash{} ((A)[0(\mBbbI{})])p BY Auto) THEN (Assert Gamma.\mBbbI{} \mvdash{} ((A)[1(\mBbbI{})])p BY Auto) THEN (RepeatFor 3 (Intro) THEN (Assert (z)[1(\mBbbI{})] \mmember{} \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\} BY (InferEqualType THEN Reduce 0 THEN Auto)) THEN (Assert (z)[0(\mBbbI{})] \mmember{} \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\} BY (InferEqualType THEN Reduce 0 THEN Auto)) THEN ((D 0 THENW Auto) THEN (D 0 THENW (EqualityIsType1 THEN Auto))) THEN (Assert (x)p \mmember{} \{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p\} BY Auto) THEN (Assert (y)p \mmember{} \{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p\} BY Auto)) THEN Unfold `fillpath` 0 THEN (InstLemmaIJ `composition-term\_wf` [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}((q=0) \mvee{} (q=1))\mkleeneclose{};\mkleeneopen{}(A)p+\mkleeneclose{};\mkleeneopen{}(cA)p+\mkleeneclose{}]\mcdot{} THENA Auto) THEN ((Subst' ((A)p+)[1(\mBbbI{})] \msim{} ((A)[1(\mBbbI{})])p -1 THENA (CsmUnfolding THEN Auto)) THEN (Subst' ((A)p+)[0(\mBbbI{})] \msim{} ((A)[0(\mBbbI{})])p -1 THENA (CsmUnfolding THEN Auto)) ) THEN (InstHyp [\mkleeneopen{}[(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+]\mkleeneclose{}] (-1)\mcdot{} THENA (SubsumeC \mkleeneopen{}\{Gamma.\mBbbI{}.\mBbbI{}, (((q)p=0) \mvee{} ((q)p=1)) \mvdash{} \_:(A)p+\}\mkleeneclose{}\mcdot{} THENL [(MemCD THEN Auto) ; (RWW "csm-face-one< csm-face-zero< csm-face-or<" 0 THEN Auto)] ) )) Home Index