---

Step * of Lemma update-context-lvl_wf

No Annotations
∀[ctxt:CubicalContext]. ∀[lvl:ℕ4]. ∀[T:{fst(ctxt) ⊢lvl _}]. ∀[v:varname()].
  (update-context-lvl(ctxt;lvl;T;v) ∈ CubicalContext)
BY
{ (Intros
   THEN Unhide
   THEN D 1
   THEN D 2
   THEN Unfolds ``cubical_context update-context-lvl`` 0
   THEN All Reduce
   THEN MemCD) }

1
.....subterm..... T:t
1:n
1. X : CubicalSet'''
2. vs : varname() List
3. c2 : {v:varname()| (v ∈ vs)}  ⟶ cttTerm(X)
4. lvl : ℕ4
5. T : {X ⊢lvl _}
6. v : varname()
⊢ X.T ⊢'''

2
.....subterm..... T:t
2:n
1. X : CubicalSet'''
2. vs : varname() List
3. c2 : {v:varname()| (v ∈ vs)}  ⟶ cttTerm(X)
4. lvl : ℕ4
5. T : {X ⊢lvl _}
6. v : varname()
⊢ <[v / vs], λx.if eq_var(x;v) then var-term-meaning(lvl;T) else (c2 x)p fi > ∈ vs:varname() List × ({v:varname()| 
                                                                                                      (v ∈ vs)} 
                                                                                                    ⟶ cttTerm(X.T))

3
.....eq aux..... 
1. X : CubicalSet'''
2. vs : varname() List
3. c2 : {v:varname()| (v ∈ vs)}  ⟶ cttTerm(X)
4. lvl : ℕ4
5. T : {X ⊢lvl _}
6. v : varname()
7. X1 : CubicalSet'''
⊢ istype(vs:varname() List × ({v:varname()| (v ∈ vs)}  ⟶ cttTerm(X1)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[ctxt:CubicalContext].  \mforall{}[lvl:\mBbbN{}4].  \mforall{}[T:\{fst(ctxt)  \mvdash{}lvl  \_\}].  \mforall{}[v:varname()].
    (update-context-lvl(ctxt;lvl;T;v)  \mmember{}  CubicalContext)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  D  1
  THEN  D  2
  THEN  Unfolds  ``cubical\_context  update-context-lvl``  0
  THEN  All  Reduce
  THEN  MemCD)

---

Home Index