---

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

No Annotations
∀[Gamma,K:j⊢]. ∀[tau:K j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ Compositon(A)].
  ((cfun-to-cop(Gamma;A;cA))tau = cfun-to-cop(K;(A)tau;(cA)tau) ∈ K ⊢ CompOp((A)tau))
BY
{ (Intros THEN (InstLemma `comp-fun-to-comp-op-inverse` [⌜Gamma⌝;⌜A⌝;⌜cA⌝]⋅ 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;cA))tau = cfun-to-cop(K;(A)tau;(cA)tau) ∈ K ⊢ CompOp((A)tau)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  Gamma].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  Compositon(A)].
    ((cfun-to-cop(Gamma;A;cA))tau  =  cfun-to-cop(K;(A)tau;(cA)tau))


By

---

Latex:
(Intros  THEN  (InstLemma  `comp-fun-to-comp-op-inverse`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}cA\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index