---

Step * of Lemma composition-term-uniformity

No Annotations
∀[H,K:j⊢]. ∀[tau:K j⟶ H]. ∀[phi:{H ⊢ _:𝔽}]. ∀[A:{H.𝕀 ⊢ _}]. ∀[u:{H, phi.𝕀 ⊢ _:A}].
∀[a0:{H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}]. ∀[cA:H.𝕀 ⊢ CompOp(A)].
  ((comp cA [phi ⊢→ u] a0)tau = comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau ∈ {K ⊢ _:((A)[1(𝕀)])tau})
BY
{ (Intros THEN (Assert ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽} BY (GenConcl ⌜(phi)p = xx ∈ {H.𝕀 ⊢ _:𝔽}⌝⋅ THEN Auto))) }

1
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : H.𝕀 ⊢ CompOp(A)
9. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
⊢ (comp cA [phi ⊢→ u] a0)tau = comp (cA)tau+ [(phi)tau ⊢→ (u)tau+] (a0)tau ∈ {K ⊢ _:((A)[1(𝕀)])tau}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{H.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[u:\{H,  phi.\mBbbI{}  \mvdash{}  \_:A\}].
\mforall{}[a0:\{H  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}].  \mforall{}[cA:H.\mBbbI{}  \mvdash{}  CompOp(A)].
    ((comp  cA  [phi  \mvdash{}\mrightarrow{}  u]  a0)tau  =  comp  (cA)tau+  [(phi)tau  \mvdash{}\mrightarrow{}  (u)tau+]  (a0)tau)


By

---

Latex:
(Intros  THEN  (Assert  ((phi)p)tau+  \mmember{}  \{K.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}  BY  (GenConcl  \mkleeneopen{}(phi)p  =  xx\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index