---

Step * of Lemma equal-composition-op

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[c1:Gamma ⊢ CompOp(A)]. ∀[c2:I:fset(ℕ)
                                                             ⟶ i:{i:ℕ| ¬i ∈ I} 
                                                             ⟶ rho:Gamma(I+i)
                                                             ⟶ phi:𝔽(I)
                                                             ⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
                                                             ⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
                                                             ⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u)].
  c1 = c2 ∈ Gamma ⊢ CompOp(A) 
  supposing c1
  = c2
  ∈ (I:fset(ℕ)
    ⟶ i:{i:ℕ| ¬i ∈ I} 
    ⟶ rho:Gamma(I+i)
    ⟶ phi:𝔽(I)
    ⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
    ⟶ cubical-path-0(Gamma;A;I;i;rho;phi;u)
    ⟶ cubical-path-1(Gamma;A;I;i;rho;phi;u))
BY
{ (Auto THEN D 3 THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[c1:Gamma  \mvdash{}  CompOp(A)].
\mforall{}[c2:I:fset(\mBbbN{})
          {}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
          {}\mrightarrow{}  rho:Gamma(I+i)
          {}\mrightarrow{}  phi:\mBbbF{}(I)
          {}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
          {}\mrightarrow{}  cubical-path-0(Gamma;A;I;i;rho;phi;u)
          {}\mrightarrow{}  cubical-path-1(Gamma;A;I;i;rho;phi;u)].
    c1  =  c2  supposing  c1  =  c2


By

---

Latex:
(Auto  THEN  D  3  THEN  EqTypeCD  THEN  Auto)

---

Home Index