---

Step * 1 1 of Lemma ctt-kind-1


1. t : CttTerm
2. ¬↑isvarterm(t)
3. ∀[opr:𝕌']. ∀[t:term(opr)].  (isvarterm(t) ∈ 𝔹)
4. v : {x:Atom| (x ∈ ``fibrant type term``)} 
5. ctt-op-sort(term-opr(t)) = v ∈ {x:Atom| (x ∈ ``fibrant type term``)} 
⊢ (if v =a "fibrant" then 1 if v =a "type" then 2 else 0 fi  = 1 ∈ ℤ) ⇒ (↑v =a "fibrant")
BY
{ (D -2 THEN (Assert (v ∈ ``fibrant type term``) BY (Unhide THEN Auto))) }

1
1. t : CttTerm
2. ¬↑isvarterm(t)
3. ∀[opr:𝕌']. ∀[t:term(opr)].  (isvarterm(t) ∈ 𝔹)
4. v : Atom
5. [%13] : (v ∈ ``fibrant type term``)
6. ctt-op-sort(term-opr(t)) = v ∈ {x:Atom| (x ∈ ``fibrant type term``)} 
7. (v ∈ ``fibrant type term``)
⊢ (if v =a "fibrant" then 1 if v =a "type" then 2 else 0 fi  = 1 ∈ ℤ) ⇒ (↑v =a "fibrant")

---

Latex:

---

Latex:

1.  t  :  CttTerm
2.  \mneg{}\muparrow{}isvarterm(t)
3.  \mforall{}[opr:\mBbbU{}'].  \mforall{}[t:term(opr)].    (isvarterm(t)  \mmember{}  \mBbbB{})
4.  v  :  \{x:Atom|  (x  \mmember{}  ``fibrant  type  term``)\} 
5.  ctt-op-sort(term-opr(t))  =  v
\mvdash{}  (if  v  =a  "fibrant"  then  1  if  v  =a  "type"  then  2  else  0  fi    =  1)  {}\mRightarrow{}  (\muparrow{}v  =a  "fibrant")


By

---

Latex:
(D  -2  THEN  (Assert  (v  \mmember{}  ``fibrant  type  term``)  BY  (Unhide  THEN  Auto)))

---

Home Index