Step
*
1
of Lemma
comp-path_wf
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G ⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. b : {G ⊢ _:A}
6. c : {G ⊢ _:A}
7. pth_a_b : {G ⊢ _:(Path_A a b)}
8. pth_b_c : {G ⊢ _:(Path_A b c)}
9. path-eta(pth_a_b) ∈ {G.𝕀 ⊢ _:(A)p}
10. path-eta(pth_b_c) ∈ {G.𝕀 ⊢ _:(A)p}
11. path-eta(refl(a)) ∈ {G.𝕀 ⊢ _:(A)p}
12. ∀[u:{G.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:((A)p)p}]. ∀[a0:{G.𝕀 ⊢ _:(((A)p)p)[0(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)p)p [((q=0) ∨ (q=1)) ⊢→ u] a0 ∈ {G.𝕀 ⊢ _:(((A)p)p)[1(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[1(𝕀)]]})
⊢ <>(comp ((cA)p)p [((q=0) ∨ (q=1)) ⊢→ ((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+)] path-eta(pth_a_b))
∈ {G ⊢ _:(Path_A a c)}
BY
{ InstHyp [⌜((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+)⌝;⌜path-eta(pth_a_b)⌝] (-1)⋅ }
1
.....wf.....
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G ⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. b : {G ⊢ _:A}
6. c : {G ⊢ _:A}
7. pth_a_b : {G ⊢ _:(Path_A a b)}
8. pth_b_c : {G ⊢ _:(Path_A b c)}
9. path-eta(pth_a_b) ∈ {G.𝕀 ⊢ _:(A)p}
10. path-eta(pth_b_c) ∈ {G.𝕀 ⊢ _:(A)p}
11. path-eta(refl(a)) ∈ {G.𝕀 ⊢ _:(A)p}
12. ∀[u:{G.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:((A)p)p}]. ∀[a0:{G.𝕀 ⊢ _:(((A)p)p)[0(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)p)p [((q=0) ∨ (q=1)) ⊢→ u] a0 ∈ {G.𝕀 ⊢ _:(((A)p)p)[1(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[1(𝕀)]]})
⊢ ((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+) ∈ {G.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:((A)p)p}
2
.....wf.....
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G ⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. b : {G ⊢ _:A}
6. c : {G ⊢ _:A}
7. pth_a_b : {G ⊢ _:(Path_A a b)}
8. pth_b_c : {G ⊢ _:(Path_A b c)}
9. path-eta(pth_a_b) ∈ {G.𝕀 ⊢ _:(A)p}
10. path-eta(pth_b_c) ∈ {G.𝕀 ⊢ _:(A)p}
11. path-eta(refl(a)) ∈ {G.𝕀 ⊢ _:(A)p}
12. ∀[u:{G.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:((A)p)p}]. ∀[a0:{G.𝕀 ⊢ _:(((A)p)p)[0(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)p)p [((q=0) ∨ (q=1)) ⊢→ u] a0 ∈ {G.𝕀 ⊢ _:(((A)p)p)[1(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[1(𝕀)]]})
⊢ path-eta(pth_a_b) ∈ {G.𝕀 ⊢ _:(((A)p)p)[0(𝕀)][((q=0) ∨ (q=1))
|⟶ (((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+))[0(𝕀)]]}
3
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G ⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. b : {G ⊢ _:A}
6. c : {G ⊢ _:A}
7. pth_a_b : {G ⊢ _:(Path_A a b)}
8. pth_b_c : {G ⊢ _:(Path_A b c)}
9. path-eta(pth_a_b) ∈ {G.𝕀 ⊢ _:(A)p}
10. path-eta(pth_b_c) ∈ {G.𝕀 ⊢ _:(A)p}
11. path-eta(refl(a)) ∈ {G.𝕀 ⊢ _:(A)p}
12. ∀[u:{G.𝕀, ((q=0) ∨ (q=1)).𝕀 ⊢ _:((A)p)p}]. ∀[a0:{G.𝕀 ⊢ _:(((A)p)p)[0(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[0(𝕀)]]}].
(comp ((cA)p)p [((q=0) ∨ (q=1)) ⊢→ u] a0 ∈ {G.𝕀 ⊢ _:(((A)p)p)[1(𝕀)][((q=0) ∨ (q=1)) |⟶ (u)[1(𝕀)]]})
13. comp ((cA)p)p [((q=0) ∨ (q=1)) ⊢→ ((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+)] path-eta(pth_a_b)
∈ {G.𝕀 ⊢ _:(((A)p)p)[1(𝕀)][((q=0) ∨ (q=1)) |⟶ (((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+))[1(𝕀)]]}
⊢ <>(comp ((cA)p)p [((q=0) ∨ (q=1)) ⊢→ ((path-eta(refl(a)))p+ ∨ (path-eta(pth_b_c))p+)] path-eta(pth_a_b))
∈ {G ⊢ _:(Path_A a c)}
Latex:
Latex:
1. G : CubicalSet\{j\}
2. A : \{G \mvdash{} \_\}
3. cA : G \mvdash{} Compositon(A)
4. a : \{G \mvdash{} \_:A\}
5. b : \{G \mvdash{} \_:A\}
6. c : \{G \mvdash{} \_:A\}
7. pth\_a$_{b}$ : \{G \mvdash{} \_:(Path\_A a b)\}
8. pth\_b$_{c}$ : \{G \mvdash{} \_:(Path\_A b c)\}
9. path-eta(pth\_a$_{b}$) \mmember{} \{G.\mBbbI{} \mvdash{} \_:(A)p\}
10. path-eta(pth\_b$_{c}$) \mmember{} \{G.\mBbbI{} \mvdash{} \_:(A)p\}
11. path-eta(refl(a)) \mmember{} \{G.\mBbbI{} \mvdash{} \_:(A)p\}
12. \mforall{}[u:\{G.\mBbbI{}, ((q=0) \mvee{} (q=1)).\mBbbI{} \mvdash{} \_:((A)p)p\}].
\mforall{}[a0:\{G.\mBbbI{} \mvdash{} \_:(((A)p)p)[0(\mBbbI{})][((q=0) \mvee{} (q=1)) |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}].
(comp ((cA)p)p [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} u] a0
\mmember{} \{G.\mBbbI{} \mvdash{} \_:(((A)p)p)[1(\mBbbI{})][((q=0) \mvee{} (q=1)) |{}\mrightarrow{} (u)[1(\mBbbI{})]]\})
\mvdash{} <>(comp ((cA)p)p [((q=0) \mvee{} (q=1)) \mvdash{}\mrightarrow{} ((path-eta(refl(a)))p+ \mvee{} (path-eta(pth\_b$_{c}\000C$))p+)]
path-eta(pth\_a$_{b}$)) \mmember{} \{G \mvdash{} \_:(Path\_A a c)\}
By
Latex:
InstHyp [\mkleeneopen{}((path-eta(refl(a)))p+ \mvee{} (path-eta(pth\_b$_{c}$))p+)\mkleeneclose{};\mkleeneopen{}path-eta(pth\_a\mbackslash{}f\000Cf24_{b}$)\mkleeneclose{}] (-1)\mcdot{}
Home
Index