---

Step * 1 of Lemma csm-filling_term

.....equality..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. cA : Gamma.𝕀 ⊢ CompOp(A)
5. u : {Gamma.𝕀, (phi)p ⊢ _:A}
6. a0 : {Gamma ⊢ _:(A)[0(𝕀)][phi |⟶ u[0]]}
7. Delta : CubicalSet{j}
8. s : Delta j⟶ Gamma
9. (fill cop-to-cfun(cA) [phi ⊢→ u] a0)s+
= fill (cop-to-cfun(cA))s+ [(phi)s ⊢→ (u)s+] (a0)s
∈ {Delta.𝕀 ⊢ _:(A)s+[((phi)s)p |⟶ (u)s+]}
⊢ (cop-to-cfun(cA))s+ ~ cop-to-cfun((cA)s+)
BY
{ (RepUR ``csm-comp-structure comp-op-to-comp-fun csm-composition`` 0 THEN CsmUnfolding THEN EqCD) }

---

Latex:

---

Latex:
.....equality..... 
1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
4.  cA  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
5.  u  :  \{Gamma.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}
6.  a0  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  u[0]]\}
7.  Delta  :  CubicalSet\{j\}
8.  s  :  Delta  j{}\mrightarrow{}  Gamma
9.  (fill  cop-to-cfun(cA)  [phi  \mvdash{}\mrightarrow{}  u]  a0)s+  =  fill  (cop-to-cfun(cA))s+  [(phi)s  \mvdash{}\mrightarrow{}  (u)s+]  (a0)s
\mvdash{}  (cop-to-cfun(cA))s+  \msim{}  cop-to-cfun((cA)s+)


By

---

Latex:
(RepUR  ``csm-comp-structure  comp-op-to-comp-fun  csm-composition``  0  THEN  CsmUnfolding  THEN  EqCD)

---

Home Index