Step
*
2
of Lemma
fill-path_wf
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. x : {Gamma ⊢ _:(A)[1(𝕀)]}
5. y : {Gamma ⊢ _:(A)[0(𝕀)]}
6. ∀[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(𝕀)]})} ) supposi\000Cng
(((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and
((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
7. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
8. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
9. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
10. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
14. 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(𝕀)]})}
15. {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}|
((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]}) ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})}
∈ 𝕌{[i | j']}
⊢ <>(fillpath(Gamma;A;cA;x;y;z)) ∈ {Gamma ⊢ _:(Path_(A)[1(𝕀)] x app(transport-fun(Gamma;A;cA); y))}
BY
{ ((MemTypeHD (-2) THENA Auto) THEN All (Fold `member`) THEN InferEqualType) }
1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. x : {Gamma ⊢ _:(A)[1(𝕀)]}
5. y : {Gamma ⊢ _:(A)[0(𝕀)]}
6. ∀[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(𝕀)]})} ) supposi\000Cng
(((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and
((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
7. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
8. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
9. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
10. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
14. fillpath(Gamma;A;cA;x;y;z) ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}
15. ((fillpath(Gamma;A;cA;x;y;z))[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
∧ ((fillpath(Gamma;A;cA;x;y;z))[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
16. {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}|
((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]}) ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})}
∈ 𝕌{[i | j']}
⊢ {Gamma ⊢ _:(Path_(A)[1(𝕀)] (fillpath(Gamma;A;cA;x;y;z))[0(𝕀)] (fillpath(Gamma;A;cA;x;y;z))[1(𝕀)])}
= {Gamma ⊢ _:(Path_(A)[1(𝕀)] x app(transport-fun(Gamma;A;cA); y))}
∈ 𝕌{[i' | j']}
2
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. x : {Gamma ⊢ _:(A)[1(𝕀)]}
5. y : {Gamma ⊢ _:(A)[0(𝕀)]}
6. ∀[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(𝕀)]})} ) supposi\000Cng
(((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and
((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
7. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
8. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
9. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
10. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
14. fillpath(Gamma;A;cA;x;y;z) ∈ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}
15. ((fillpath(Gamma;A;cA;x;y;z))[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
∧ ((fillpath(Gamma;A;cA;x;y;z))[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
16. {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}|
((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]}) ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})}
∈ 𝕌{[i | j']}
17. {Gamma ⊢ _:(Path_(A)[1(𝕀)] (fillpath(Gamma;A;cA;x;y;z))[0(𝕀)] (fillpath(Gamma;A;cA;x;y;z))[1(𝕀)])}
= {Gamma ⊢ _:(Path_(A)[1(𝕀)] x app(transport-fun(Gamma;A;cA); y))}
∈ 𝕌{[i' | j']}
⊢ <>(fillpath(Gamma;A;cA;x;y;z)) ∈ {Gamma ⊢ _:(Path_(A)[1(𝕀)] (fillpath(Gamma;A;cA;x;y;z))[0(𝕀)]
(fillpath(Gamma;A;cA;x;y;z))[1(𝕀)])}
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma.\mBbbI{} \mvdash{} \_\}
3. cA : Gamma.\mBbbI{} \mvdash{} CompOp(A)
4. x : \{Gamma \mvdash{} \_:(A)[1(\mBbbI{})]\}
5. y : \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\}
6. \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))\} ) supposing
(((z)[0(\mBbbI{})] = app(rev-transport-fun(Gamma;A;cA); x)) and
((z)[1(\mBbbI{})] = y))
7. Gamma.\mBbbI{} \mvdash{} ((A)[0(\mBbbI{})])p
8. Gamma.\mBbbI{} \mvdash{} ((A)[1(\mBbbI{})])p
9. z : \{Gamma.\mBbbI{} \mvdash{} \_:((A)[0(\mBbbI{})])p\}
10. (z)[1(\mBbbI{})] \mmember{} \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\}
11. (z)[0(\mBbbI{})] \mmember{} \{Gamma \mvdash{} \_:(A)[0(\mBbbI{})]\}
12. (z)[1(\mBbbI{})] = y
13. (z)[0(\mBbbI{})] = app(rev-transport-fun(Gamma;A;cA); x)
14. 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))\}
15. \{t:\{Gamma.\mBbbI{} \mvdash{} \_:((A)[1(\mBbbI{})])p\}|
((t)[0(\mBbbI{})] = x) \mwedge{} ((t)[1(\mBbbI{})] = app(transport-fun(Gamma;A;cA); y))\} \mmember{} \mBbbU{}\{[i | j']\}
\mvdash{} <>(fillpath(Gamma;A;cA;x;y;z)) \mmember{} \{Gamma \mvdash{} \_:(Path\_(A)[1(\mBbbI{})] x app(transport-fun(Gamma;A;cA); y))\}
By
Latex:
((MemTypeHD (-2) THENA Auto) THEN All (Fold `member`) THEN InferEqualType)
Home
Index