---

Step * of Lemma cubical-type-restriction-eq

No Annotations
∀[X:j⊢]. ∀[T,A:{X ⊢ _}]. ∀[a:{X ⊢ _:A}]. ∀[g:I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ A(alpha)].
  cubical-type-restriction(X;T;I,alpha,t.(g I alpha t) = a(alpha) ∈ A(alpha)) 
  supposing ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀alpha:X(I). ∀t:T(alpha).
              ((g J f(alpha) (t alpha f)) = (g I alpha t alpha f) ∈ A(f(alpha)))
BY
{ (Unfold `cubical-type-restriction` 0
   THEN Intros
   THEN (RWO "cubical-term-at-morph<" 0 THENA Auto)
   THEN RWO  "-1<" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T,A:\{X  \mvdash{}  \_\}].  \mforall{}[a:\{X  \mvdash{}  \_:A\}].  \mforall{}[g:I:fset(\mBbbN{})  {}\mrightarrow{}  alpha:X(I)  {}\mrightarrow{}  T(alpha)  {}\mrightarrow{}  A(alpha)].
    cubical-type-restriction(X;T;I,alpha,t.(g  I  alpha  t)  =  a(alpha)) 
    supposing  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}alpha:X(I).  \mforall{}t:T(alpha).
                            ((g  J  f(alpha)  (t  alpha  f))  =  (g  I  alpha  t  alpha  f))


By

---

Latex:
(Unfold  `cubical-type-restriction`  0
  THEN  Intros
  THEN  (RWO  "cubical-term-at-morph<"  0  THENA  Auto)
  THEN  RWO    "-1<"  0
  THEN  Auto)

---

Home Index