---

Step * 1 of Lemma system-type-properties


1. Gamma : CubicalSet{j}
⊢ compatible-system{i:l}(Gamma;[])
⇒ (Gamma, \/(map(λp.(fst(p));[])) ⊢ system-type([])
   ∧ (∀i:ℕ||[]||. (system-type([]) = (snd([][i])) ∈ {Gamma, fst([][i]) ⊢ _})))
BY
{ ((D 0 THENA Auto) THEN RepUR ``system-type face-or-list`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
\mvdash{}  compatible-system\{i:l\}(Gamma;[])
{}\mRightarrow{}  (Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));[]))  \mvdash{}  system-type([])
      \mwedge{}  (\mforall{}i:\mBbbN{}||[]||.  (system-type([])  =  (snd([][i])))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RepUR  ``system-type  face-or-list``  0  THEN  Auto)

---

Home Index