---

Step * of Lemma system-type-properties

No Annotations
∀Gamma:j⊢. ∀sys:(phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List.
  (compatible-system{i:l}(Gamma;sys)
  ⇒ (Gamma, \/(map(λp.(fst(p));sys)) ⊢ system-type(sys)
     ∧ (∀i:ℕ||sys||. (system-type(sys) = (snd(sys[i])) ∈ {Gamma, fst(sys[i]) ⊢ _}))))
BY
{ InductionOnList }

1
1. Gamma : CubicalSet{j}
⊢ compatible-system{i:l}(Gamma;[])
⇒ (Gamma, \/(map(λp.(fst(p));[])) ⊢ system-type([])
   ∧ (∀i:ℕ||[]||. (system-type([]) = (snd([][i])) ∈ {Gamma, fst([][i]) ⊢ _})))

2
1. Gamma : CubicalSet{j}
2. u : phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}
3. v : (phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List
4. compatible-system{i:l}(Gamma;v)
⇒ (Gamma, \/(map(λp.(fst(p));v)) ⊢ system-type(v)
   ∧ (∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _})))
⊢ compatible-system{i:l}(Gamma;[u / v])
⇒ (Gamma, \/(map(λp.(fst(p));[u / v])) ⊢ system-type([u / v])
   ∧ (∀i:ℕ||[u / v]||. (system-type([u / v]) = (snd([u / v][i])) ∈ {Gamma, fst([u / v][i]) ⊢ _})))

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}sys:(phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\})  List.
    (compatible-system\{i:l\}(Gamma;sys)
    {}\mRightarrow{}  (Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));sys))  \mvdash{}  system-type(sys)
          \mwedge{}  (\mforall{}i:\mBbbN{}||sys||.  (system-type(sys)  =  (snd(sys[i]))))))


By

---

Latex:
InductionOnList

---

Home Index