---

Step * 2 1 1 1 2 2 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. (∀y∈v.let phi1,A1 = <phi, u1> 
         in let phi2,A2 = y 
            in A1 = A2 ∈ {Gamma, (phi1 ∧ phi2) ⊢ _})
7. Gamma, \/(map(λp.(fst(p));v)) ⊢ system-type(v)
8. ∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _})
9. ∀i:ℕ||v||. (u1 = system-type(v) ∈ {Gamma, (phi ∧ fst(v[i])) ⊢ _})
10. Gamma, \/(map(λp.(phi ∧ fst(p));v)) ⊢ u1
11. system-type(v) = system-type(v) ∈ {Gamma, \/(map(λp.(fst(p));v)) ⊢ _}
⊢ {Gamma, \/(map(λp.(fst(p));v)) ⊢ _} ⊆r {Gamma, \/(map(λp.(phi ∧ fst(p));v)) ⊢ _}
BY
{ (BLemma `context-subset-subtype` THEN Auto) }

1
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. (∀y∈v.let phi1,A1 = <phi, u1> 
         in let phi2,A2 = y 
            in A1 = A2 ∈ {Gamma, (phi1 ∧ phi2) ⊢ _})
7. Gamma, \/(map(λp.(fst(p));v)) ⊢ system-type(v)
8. ∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _})
9. ∀i:ℕ||v||. (u1 = system-type(v) ∈ {Gamma, (phi ∧ fst(v[i])) ⊢ _})
10. Gamma, \/(map(λp.(phi ∧ fst(p));v)) ⊢ u1
11. system-type(v) = system-type(v) ∈ {Gamma, \/(map(λp.(fst(p));v)) ⊢ _}
12. I : fset(ℕ)
13. rho : Gamma(I)
14. \/(map(λp.(phi ∧ fst(p));v))(rho) = 1 ∈ Point(face_lattice(I))
⊢ \/(map(λp.(fst(p));v))(rho) = 1 ∈ Point(face_lattice(I))

2
.....wf..... 
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. (∀y∈v.let phi1,A1 = <phi, u1> 
         in let phi2,A2 = y 
            in A1 = A2 ∈ {Gamma, (phi1 ∧ phi2) ⊢ _})
7. Gamma, \/(map(λp.(fst(p));v)) ⊢ system-type(v)
8. ∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _})
9. ∀i:ℕ||v||. (u1 = system-type(v) ∈ {Gamma, (phi ∧ fst(v[i])) ⊢ _})
10. Gamma, \/(map(λp.(phi ∧ fst(p));v)) ⊢ u1
11. system-type(v) = system-type(v) ∈ {Gamma, \/(map(λp.(fst(p));v)) ⊢ _}
12. I : fset(ℕ)
13. rho : Gamma(I)
⊢ \/(map(λp.(phi ∧ fst(p));v))(rho) ∈ Point(face_lattice(I))

---

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.  (\mforall{}y\mmember{}v.let  phi1,A1  =  <phi,  u1> 
                  in  let  phi2,A2  =  y 
                        in  A1  =  A2)
7.  Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));v))  \mvdash{}  system-type(v)
8.  \mforall{}i:\mBbbN{}||v||.  (system-type(v)  =  (snd(v[i])))
9.  \mforall{}i:\mBbbN{}||v||.  (u1  =  system-type(v))
10.  Gamma,  \mbackslash{}/(map(\mlambda{}p.(phi  \mwedge{}  fst(p));v))  \mvdash{}  u1
11.  system-type(v)  =  system-type(v)
\mvdash{}  \{Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));v))  \mvdash{}  \_\}  \msubseteq{}r  \{Gamma,  \mbackslash{}/(map(\mlambda{}p.(phi  \mwedge{}  fst(p));v))  \mvdash{}  \_\}


By

---

Latex:
(BLemma  `context-subset-subtype`  THEN  Auto)

---

Home Index