---

Step * of Lemma Kan-cubical-type-equal

∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[B:A:{X ⊢ _} × (I:(Cname List)
                                                    ⟶ alpha:X(I)
                                                    ⟶ J:(nameset(I) List)
                                                    ⟶ x:nameset(I)
                                                    ⟶ i:ℕ2
                                                    ⟶ A-open-box(X;A;I;alpha;J;x;i)
                                                    ⟶ A(alpha))].
  A = B ∈ {X ⊢ _(Kan)} 
  supposing A
  = B
  ∈ (A:{X ⊢ _} × (I:(Cname List)
                 ⟶ alpha:X(I)
                 ⟶ J:(nameset(I) List)
                 ⟶ x:nameset(I)
                 ⟶ i:ℕ2
                 ⟶ A-open-box(X;A;I;alpha;J;x;i)
                 ⟶ A(alpha)))
BY
{ (Auto THEN DVar `A'⋅ THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_(Kan)\}].  \mforall{}[B:A:\{X  \mvdash{}  \_\}  \mtimes{}  (I:(Cname  List)
                                                                                                        {}\mrightarrow{}  alpha:X(I)
                                                                                                        {}\mrightarrow{}  J:(nameset(I)  List)
                                                                                                        {}\mrightarrow{}  x:nameset(I)
                                                                                                        {}\mrightarrow{}  i:\mBbbN{}2
                                                                                                        {}\mrightarrow{}  A-open-box(X;A;I;alpha;J;x;i)
                                                                                                        {}\mrightarrow{}  A(alpha))].
    A  =  B  supposing  A  =  B


By

---

Latex:
(Auto  THEN  DVar  `A'\mcdot{}  THEN  EqTypeCD  THEN  Auto)

---

Home Index