---

Step * of Lemma comp-path_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[cA:G ⊢ Compositon(A)]. ∀[a,b,c:{G ⊢ _:A}]. ∀[pth_a_b:{G ⊢ _:(Path_A a b)}].
∀[pth_b_c:{G ⊢ _:(Path_A b c)}].
  (pth_a_b + pth_b_c ∈ {G ⊢ _:(Path_A a c)})
BY
{ (Intros
   THEN Unfold `comp-path` 0
   THEN (Unhide
         THEN (InstLemma `path-eta_wf` [⌜G⌝;⌜A⌝;⌜pth_a_b⌝]⋅ THENA Auto)
         THEN (InstLemma `path-eta_wf` [⌜G⌝;⌜A⌝;⌜pth_b_c⌝]⋅ THENA Auto)
         THEN (InstLemma `path-eta_wf` [⌜G⌝;⌜A⌝;⌜refl(a)⌝]⋅ THENA Auto)
         THEN (InstLemma `comp_term_wf` [⌜G.𝕀⌝;⌜((q=0) ∨ (q=1))⌝;⌜((A)p)p⌝;⌜((cA)p)p⌝]⋅ THENA Auto))
   THEN skip{(BLemma `term-to-path-wf` THEN Try (Trivial))}) }

1
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)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  \mvdash{}  Compositon(A)].  \mforall{}[a,b,c:\{G  \mvdash{}  \_:A\}].  \mforall{}[pth\_a$_{b}\mbackslash{}ff2\000C4:\{G  \mvdash{}  \_:(Path\_A  a  b)\}].
\mforall{}[pth\_b$_{c}$:\{G  \mvdash{}  \_:(Path\_A  b  c)\}].
    (pth\_a$_{b}$  +  pth\_b$_{c}$  \mmember{}  \{G  \mvdash{}  \_:(Path\_A  a  c)\})


By

---

Latex:
(Intros
  THEN  Unfold  `comp-path`  0
  THEN  (Unhide
              THEN  (InstLemma  `path-eta\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}pth\_a$_{b}$\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `path-eta\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}pth\_b$_{c}$\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `path-eta\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}refl(a)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `comp\_term\_wf`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}((q=0)  \mvee{}  (q=1))\mkleeneclose{};\mkleeneopen{}((A)p)p\mkleeneclose{};\mkleeneopen{}((cA)p)p\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  skip\{(BLemma  `term-to-path-wf`  THEN  Try  (Trivial))\})

---

Home Index