---

Step * 2 1 1 1 1 1 1 2 of Lemma system-type-properties


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. u1 : {Gamma, phi ⊢ _}
4. v : (phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List
5. compatible-system{i:l}(Gamma;v)
6. Gamma, \/(map(λp.(fst(p));v)) ⊢ system-type(v)
7. ∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _})
8. i : ℕ||v||
9. system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _}
10. let phi2,A2 = v[i] 
    in u1 = A2 ∈ {Gamma, (phi ∧ phi2) ⊢ _}
11. v[i] = v[i] ∈ (phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _})
⊢ (phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) ⊆r (Top × Top)
BY
{ (At ⌜𝕌'⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  u1  :  \{Gamma,  phi  \mvdash{}  \_\}
4.  v  :  (phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\})  List
5.  compatible-system\{i:l\}(Gamma;v)
6.  Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));v))  \mvdash{}  system-type(v)
7.  \mforall{}i:\mBbbN{}||v||.  (system-type(v)  =  (snd(v[i])))
8.  i  :  \mBbbN{}||v||
9.  system-type(v)  =  (snd(v[i]))
10.  let  phi2,A2  =  v[i] 
        in  u1  =  A2
11.  v[i]  =  v[i]
\mvdash{}  (phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\})  \msubseteq{}r  (Top  \mtimes{}  Top)


By

---

Latex:
(At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index