Step
*
1
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)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(𝕀)]})}
BY
{ ((RWO "csm-case-endpoints" (-1) THENA Auto)
THEN Reduce -1
THEN (RWW "term-p+0 term-p+1" (-1) THENA Auto)
THEN (Subst' (q)1(Gamma.𝕀) ~ q -1 THENA (CsmUnfolding 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=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]]})
⊢ 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)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+])[0(\mBbbI{})]]\}]
(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)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+])[1(\mBbbI{})]]\})
\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:
((RWO "csm-case-endpoints" (-1) THENA Auto)
THEN Reduce -1
THEN (RWW "term-p+0 term-p+1" (-1) THENA Auto)
THEN (Subst' (q)1(Gamma.\mBbbI{}) \msim{} q -1 THENA (CsmUnfolding THEN Auto)))
Home
Index