---

Step * of Lemma comp-op-to-comp-fun_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)].  (cop-to-cfun(cA) ∈ composition-function{j:l,i:l}(Gamma;A))
BY
{ (Intros THEN Unhide THEN RepUR ``composition-function comp-op-to-comp-fun`` 0 THEN RepeatFor 5 ((MemCD THENA Auto))) }

1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. H : CubicalSet{j}
5. sigma : H.𝕀 j⟶ Gamma
6. phi : {H ⊢ _:𝔽}
7. u : {H, phi.𝕀 ⊢ _:(A)sigma}
8. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⊢ comp (cA)sigma [phi ⊢→ u] a0 ∈ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].
    (cop-to-cfun(cA)  \mmember{}  composition-function\{j:l,i:l\}(Gamma;A))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepUR  ``composition-function  comp-op-to-comp-fun``  0
  THEN  RepeatFor  5  ((MemCD  THENA  Auto)))

---

Home Index