---

Step * of Lemma composition-structure-equal

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[c1,c2:Gamma ⊢ Compositon(A)].
  c1 = c2 ∈ Gamma ⊢ Compositon(A) 
  supposing ∀H:j⊢. ∀sigma:H.𝕀 j⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi.𝕀 ⊢ _:(A)sigma}.
            ∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
              ((c1 H sigma phi u a0) = (c2 H sigma phi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]})
BY
{ Intros }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. c1 : Gamma ⊢ Compositon(A)
4. c2 : Gamma ⊢ Compositon(A)
5. ∀H:j⊢. ∀sigma:H.𝕀 j⟶ Gamma. ∀phi:{H ⊢ _:𝔽}. ∀u:{H, phi.𝕀 ⊢ _:(A)sigma}.
   ∀a0:{H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}.
     ((c1 H sigma phi u a0) = (c2 H sigma phi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]})
⊢ c1 = c2 ∈ Gamma ⊢ Compositon(A)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[c1,c2:Gamma  \mvdash{}  Compositon(A)].
    c1  =  c2 
    supposing  \mforall{}H:j\mvdash{}.  \mforall{}sigma:H.\mBbbI{}  j{}\mrightarrow{}  Gamma.  \mforall{}phi:\{H  \mvdash{}  \_:\mBbbF{}\}.  \mforall{}u:\{H,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}.
                        \mforall{}a0:\{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}.
                            ((c1  H  sigma  phi  u  a0)  =  (c2  H  sigma  phi  u  a0))


By

---

Latex:
Intros

---

Home Index