---

Step * 1 of Lemma pathtype-comp_wf

.....assertion..... 
1. [G] : CubicalSet{j}
2. [A] : {G ⊢ _}
3. [cA] : G ⊢ Compositon(A)
⊢ pathtype-comp(G;A;cA) ∈ composition-function{j:l,i:l}(G;Path(A))
BY
{ (Unfolds ``pathtype-comp composition-function`` 0
   THEN RepeatFor 5 ((FunExt THENA Auto))
   THEN Reduce 0
   THEN (Assert ⌜{H, phi.𝕀 ⊢ _:(Path(A))sigma} = {H, phi.𝕀 ⊢ _:Path((A)sigma)} ∈ 𝕌{[i' | j']}⌝⋅ THENA (EqCDA THEN Auto))
   THEN (Assert ⌜a0 ∈ {H ⊢ _:Path(((A)sigma)[0(𝕀)])}⌝⋅
         THENA (DVar `a0' THEN (InferEqualType THEN Try (Trivial)) THEN EqCDA THEN RWO "csm-pathtype" 0 THEN Auto)
         )
   THEN (InstLemma `cubicalpath-app_wf` [⌜H⌝;⌜((A)sigma)[0(𝕀)]⌝;⌜a0⌝;⌜0(𝕀)⌝]⋅ THENA Auto)
   THEN ((InstLemma `csm+_wf` [⌜H⌝;⌜H.𝕀⌝;⌜𝕀⌝;⌜p⌝]⋅ THENA Auto) THEN (RWO  "csm-interval-type" (-1) THENA Auto))
   THEN (InstLemma `comp_term_wf`  [⌜H.𝕀⌝;⌜(phi)p⌝;⌜((A)sigma)p+⌝;⌜((cA)sigma)p+⌝]⋅ THENA Auto)
   THEN (Subst' (((A)sigma)p+)[1(𝕀)] ~ (((A)sigma)[1(𝕀)])p -1 THENA (CsmUnfolding THEN Auto))) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G ⊢ Compositon(A)
4. H : CubicalSet{j}
5. sigma : H.𝕀 j⟶ G
6. phi : {H ⊢ _:𝔽}
7. u : {H, phi.𝕀 ⊢ _:(Path(A))sigma}
8. a0 : {H ⊢ _:((Path(A))sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
9. {H, phi.𝕀 ⊢ _:(Path(A))sigma} = {H, phi.𝕀 ⊢ _:Path((A)sigma)} ∈ 𝕌{[i' | j']}
10. a0 ∈ {H ⊢ _:Path(((A)sigma)[0(𝕀)])}
11. a0 @ 0(𝕀) ∈ {H ⊢ _:((A)sigma)[0(𝕀)]}
12. p+ ∈ H.𝕀.𝕀 ij⟶ H.𝕀
13. ∀[u:{H.𝕀, (phi)p.𝕀 ⊢ _:((A)sigma)p+}]. ∀[a0:{H.𝕀 ⊢ _:(((A)sigma)p+)[0(𝕀)][(phi)p |⟶ (u)[0(𝕀)]]}].
      (comp ((cA)sigma)p+ [(phi)p ⊢→ u] a0 ∈ {H.𝕀 ⊢ _:(((A)sigma)[1(𝕀)])p[(phi)p |⟶ (u)[1(𝕀)]]})
⊢ <>comp ((cA)sigma)p+ [(phi)p ⊢→ (u)p+ @ (q)p] (a0)p @ q ∈ {H ⊢ _:((Path(A))sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}

---

Latex:

---

Latex:
.....assertion..... 
1.  [G]  :  CubicalSet\{j\}
2.  [A]  :  \{G  \mvdash{}  \_\}
3.  [cA]  :  G  \mvdash{}  Compositon(A)
\mvdash{}  pathtype-comp(G;A;cA)  \mmember{}  composition-function\{j:l,i:l\}(G;Path(A))


By

---

Latex:
(Unfolds  ``pathtype-comp  composition-function``  0
  THEN  RepeatFor  5  ((FunExt  THENA  Auto))
  THEN  Reduce  0
  THEN  (Assert  \mkleeneopen{}\{H,  phi.\mBbbI{}  \mvdash{}  \_:(Path(A))sigma\}  =  \{H,  phi.\mBbbI{}  \mvdash{}  \_:Path((A)sigma)\}\mkleeneclose{}\mcdot{}
              THENA  (EqCDA  THEN  Auto)
              )
  THEN  (Assert  \mkleeneopen{}a0  \mmember{}  \{H  \mvdash{}  \_:Path(((A)sigma)[0(\mBbbI{})])\}\mkleeneclose{}\mcdot{}
              THENA  (DVar  `a0'
                            THEN  (InferEqualType  THEN  Try  (Trivial))
                            THEN  EqCDA
                            THEN  RWO  "csm-pathtype"  0
                            THEN  Auto)
              )
  THEN  (InstLemma  `cubicalpath-app\_wf`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}((A)sigma)[0(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}a0\mkleeneclose{};\mkleeneopen{}0(\mBbbI{})\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `csm+\_wf`  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RWO    "csm-interval-type"  (-1)  THENA  Auto)
              )
  THEN  (InstLemma  `comp\_term\_wf`    [\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(phi)p\mkleeneclose{};\mkleeneopen{}((A)sigma)p+\mkleeneclose{};\mkleeneopen{}((cA)sigma)p+\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  (((A)sigma)p+)[1(\mBbbI{})]  \msim{}  (((A)sigma)[1(\mBbbI{})])p  -1  THENA  (CsmUnfolding  THEN  Auto)))

---

Home Index