---

Step * 2 of Lemma ctt-op-meaning_wf


1. X : ?CubicalContext
2. vs : varname() List
3. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
4. f1 : Type
5. L : CttMeaningTriple List
6. vdf-eq(?CubicalContext;ctt-binder-context X vs <k, f1>;L)
7. ||L|| = ||ctt-arity(<k, f1>)|| ∈ ℤ
8. ∀i:ℕ||L||
     ((||fst(map(λx.(fst(snd(x)));L)[i])|| = (fst(ctt-arity(<k, f1>)[i])) ∈ ℤ)
     ∧ (ctt-kind(snd(map(λx.(fst(snd(x)));L)[i])) = (snd(ctt-arity(<k, f1>)[i])) ∈ ℤ)
     ∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);snd(map(λx.(fst(snd(x)));L)[i]))))
9. ∀[i:ℕ||L||]. ((fst(L[i])) = (ctt-binder-context X vs <k, f1> firstn(i;L) (fst(snd(L[i])))) ∈ ?CubicalContext)
10. ¬(k = "opid" ∈ Atom)
11. k = "nType" ∈ Atom
⊢ ctt-op-meaning{i:l}(X; vs; <"nType", f1>; L) ∈ [[X;mkterm(<"nType", f1>;map(λx.(fst(snd(x)));L))]]
BY
{ (RepUR ``ctt_meaning ctt-meaning-type mkwfterm isvarterm mkterm term-opr`` 0
   THEN RepUR ``ctt-op-sort ctt-op-meaning`` 0
   THEN Unfold `uimplies` 0
   THEN (MemTypeCD THENW Auto)
   THEN MemCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  ?CubicalContext
2.  vs  :  varname()  List
3.  k  :  \{k:Atom|  (k  \mmember{}  ``opid  nType  nterm  univ``)\} 
4.  f1  :  Type
5.  L  :  CttMeaningTriple  List
6.  vdf-eq(?CubicalContext;ctt-binder-context  X  vs  <k,  f1>L)
7.  ||L||  =  ||ctt-arity(<k,  f1>)||
8.  \mforall{}i:\mBbbN{}||L||
          ((||fst(map(\mlambda{}x.(fst(snd(x)));L)[i])||  =  (fst(ctt-arity(<k,  f1>)[i])))
          \mwedge{}  (ctt-kind(snd(map(\mlambda{}x.(fst(snd(x)));L)[i]))  =  (snd(ctt-arity(<k,  f1>)[i])))
          \mwedge{}  (\muparrow{}wf-term(\mlambda{}f.ctt-arity(f);\mlambda{}t.ctt-kind(t);snd(map(\mlambda{}x.(fst(snd(x)));L)[i]))))
9.  \mforall{}[i:\mBbbN{}||L||].  ((fst(L[i]))  =  (ctt-binder-context  X  vs  <k,  f1>  firstn(i;L)  (fst(snd(L[i])))))
10.  \mneg{}(k  =  "opid")
11.  k  =  "nType"
\mvdash{}  ctt-op-meaning\{i:l\}(X;  vs;  <"nType",  f1>  L)  \mmember{}  [[X;mkterm(<"nType",  f1>map(\mlambda{}x.(fst(snd(x)));L))]]


By

---

Latex:
(RepUR  ``ctt\_meaning  ctt-meaning-type  mkwfterm  isvarterm  mkterm  term-opr``  0
  THEN  RepUR  ``ctt-op-sort  ctt-op-meaning``  0
  THEN  Unfold  `uimplies`  0
  THEN  (MemTypeCD  THENW  Auto)
  THEN  MemCD
  THEN  Auto)

---

Home Index