---

Step * of Lemma csm-rev-type-line-comp

No Annotations
∀[G,K:j⊢]. ∀[tau:K j⟶ G]. ∀[A:{G.𝕀 ⊢ _}]. ∀[cA:G.𝕀 ⊢ CompOp(A)].
  (((cA)-)tau+ = ((cA)tau+)- ∈ K.𝕀 ⊢ CompOp(((A)-)tau+))
BY
{ (Auto THEN Unfolds ``rev-type-line rev-type-line-comp`` 0) }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G.𝕀 ⊢ _}
5. cA : G.𝕀 ⊢ CompOp(A)
⊢ ((cA)(p;1-(q)))tau+ = ((cA)tau+)(p;1-(q)) ∈ K.𝕀 ⊢ CompOp(((A)(p;1-(q)))tau+)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  G].  \mforall{}[A:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:G.\mBbbI{}  \mvdash{}  CompOp(A)].    (((cA)-)tau+  =  ((cA)tau+)-)


By

---

Latex:
(Auto  THEN  Unfolds  ``rev-type-line  rev-type-line-comp``  0)

---

Home Index