---

Step * 1 1 of Lemma csm-comp-fun-to-comp-op


1. Gamma : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : Gamma ⊢ Compositon(A)
6. cop-to-cfun(cfun-to-cop(Gamma;A;cA)) = cA ∈ Gamma ⊢ Compositon(A)
⊢ (cfun-to-cop(Gamma;A;cop-to-cfun(cfun-to-cop(Gamma;A;cA))))tau
= cfun-to-cop(K;(A)tau;(cop-to-cfun(cfun-to-cop(Gamma;A;cA)))tau)
∈ K ⊢ CompOp((A)tau)
BY
{ (RWO "csm-comp-op-to-comp-fun-sq" 0 THENA Auto) }

1
1. Gamma : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ Gamma
4. A : {Gamma ⊢ _}
5. cA : Gamma ⊢ Compositon(A)
6. cop-to-cfun(cfun-to-cop(Gamma;A;cA)) = cA ∈ Gamma ⊢ Compositon(A)
⊢ (cfun-to-cop(Gamma;A;cop-to-cfun(cfun-to-cop(Gamma;A;cA))))tau
= cfun-to-cop(K;(A)tau;cop-to-cfun((cfun-to-cop(Gamma;A;cA))tau))
∈ K ⊢ CompOp((A)tau)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  cA  :  Gamma  \mvdash{}  Compositon(A)
6.  cop-to-cfun(cfun-to-cop(Gamma;A;cA))  =  cA
\mvdash{}  (cfun-to-cop(Gamma;A;cop-to-cfun(cfun-to-cop(Gamma;A;cA))))tau
=  cfun-to-cop(K;(A)tau;(cop-to-cfun(cfun-to-cop(Gamma;A;cA)))tau)


By

---

Latex:
(RWO  "csm-comp-op-to-comp-fun-sq"  0  THENA  Auto)

---

Home Index