---

Step * 1 of Lemma csm-transport

.....subterm..... T:t
3:n
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. a : {Gamma ⊢ _:(A)[0(𝕀)]}
5. H : CubicalSet{j}
6. s : H j⟶ Gamma
7. (comp cA [0(𝔽) ⊢→ discr(⋅)] a)s = comp (cA)s+ [(0(𝔽))s ⊢→ (discr(⋅))s+] (a)s ∈ {H ⊢ _:((A)[1(𝕀)])s}
⊢ comp (cA)s+ [0(𝔽) ⊢→ discr(⋅)] (a)s = comp (cA)s+ [(0(𝔽))s ⊢→ (discr(⋅))s+] (a)s ∈ {H ⊢ _:((A)[1(𝕀)])s}
BY
{ (Symmetry
   THEN (Assert ⌜(discr(⋅))s+ ∈ {H, (0(𝔽))s.𝕀 ⊢ _:(A)s+}⌝⋅ THENA (RWO  "csm-face-0" 0 THEN Auto))
   THEN (Assert (a)s ∈ {H ⊢ _:((A)s+)[0(𝕀)][(0(𝔽))s |⟶ ((discr(⋅))s+)[0(𝕀)]]} BY
               ((RWO  "csm-face-0" 0 THENA Auto)
                THEN MemTypeCD
                THEN (Subst' ((A)s+)[0(𝕀)] ~ ((A)[0(𝕀)])s 0 THENA CsmUnfolding)
                THEN Try (Complete (Auto))))) }

1
.....aux..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. a : {Gamma ⊢ _:(A)[0(𝕀)]}
5. H : CubicalSet{j}
6. s : H j⟶ Gamma
7. (comp cA [0(𝔽) ⊢→ discr(⋅)] a)s = comp (cA)s+ [(0(𝔽))s ⊢→ (discr(⋅))s+] (a)s ∈ {H ⊢ _:((A)[1(𝕀)])s}
8. (discr(⋅))s+ ∈ {H, (0(𝔽))s.𝕀 ⊢ _:(A)s+}
9. a1 : {H ⊢ _:((A)s+)[0(𝕀)]}
⊢ istype(((discr(⋅))s+)[0(𝕀)] = a1 ∈ {H, 0(𝔽) ⊢ _:((A)[0(𝕀)])s})

2
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. a : {Gamma ⊢ _:(A)[0(𝕀)]}
5. H : CubicalSet{j}
6. s : H j⟶ Gamma
7. (comp cA [0(𝔽) ⊢→ discr(⋅)] a)s = comp (cA)s+ [(0(𝔽))s ⊢→ (discr(⋅))s+] (a)s ∈ {H ⊢ _:((A)[1(𝕀)])s}
8. (discr(⋅))s+ ∈ {H, (0(𝔽))s.𝕀 ⊢ _:(A)s+}
9. (a)s ∈ {H ⊢ _:((A)s+)[0(𝕀)][(0(𝔽))s |⟶ ((discr(⋅))s+)[0(𝕀)]]}
⊢ comp (cA)s+ [(0(𝔽))s ⊢→ (discr(⋅))s+] (a)s = comp (cA)s+ [0(𝔽) ⊢→ discr(⋅)] (a)s ∈ {H ⊢ _:((A)[1(𝕀)])s}

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  cA  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
4.  a  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}
5.  H  :  CubicalSet\{j\}
6.  s  :  H  j{}\mrightarrow{}  Gamma
7.  (comp  cA  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{})]  a)s  =  comp  (cA)s+  [(0(\mBbbF{}))s  \mvdash{}\mrightarrow{}  (discr(\mcdot{}))s+]  (a)s
\mvdash{}  comp  (cA)s+  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{})]  (a)s  =  comp  (cA)s+  [(0(\mBbbF{}))s  \mvdash{}\mrightarrow{}  (discr(\mcdot{}))s+]  (a)s


By

---

Latex:
(Symmetry
  THEN  (Assert  \mkleeneopen{}(discr(\mcdot{}))s+  \mmember{}  \{H,  (0(\mBbbF{}))s.\mBbbI{}  \mvdash{}  \_:(A)s+\}\mkleeneclose{}\mcdot{}  THENA  (RWO    "csm-face-0"  0  THEN  Auto))
  THEN  (Assert  (a)s  \mmember{}  \{H  \mvdash{}  \_:((A)s+)[0(\mBbbI{})][(0(\mBbbF{}))s  |{}\mrightarrow{}  ((discr(\mcdot{}))s+)[0(\mBbbI{})]]\}  BY
                          ((RWO    "csm-face-0"  0  THENA  Auto)
                            THEN  MemTypeCD
                            THEN  (Subst'  ((A)s+)[0(\mBbbI{})]  \msim{}  ((A)[0(\mBbbI{})])s  0  THENA  CsmUnfolding)
                            THEN  Try  (Complete  (Auto)))))

---

Home Index