---

Step * 2 1 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) ∧ (∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _}))
⊢ Gamma, \/(map(λp.(fst(p));[<phi, u1> / v])) ⊢ system-type([<phi, u1> / v])
∧ (∀i:ℕ||[<phi, u1> / v]||
     (system-type([<phi, u1> / v]) = (snd([<phi, u1> / v][i])) ∈ {Gamma, fst([<phi, u1> / v][i]) ⊢ _}))
BY
{ Assert ⌜Gamma, (phi ∧ \/(map(λp.(fst(p));v))) ⊢ u1 = system-type(v)⌝⋅ }

1
.....assertion..... 
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) ∧ (∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _}))
⊢ Gamma, (phi ∧ \/(map(λp.(fst(p));v))) ⊢ u1 = system-type(v)

2
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) ∧ (∀i:ℕ||v||. (system-type(v) = (snd(v[i])) ∈ {Gamma, fst(v[i]) ⊢ _}))
8. Gamma, (phi ∧ \/(map(λp.(fst(p));v))) ⊢ u1 = system-type(v)
⊢ Gamma, \/(map(λp.(fst(p));[<phi, u1> / v])) ⊢ system-type([<phi, u1> / v])
∧ (∀i:ℕ||[<phi, u1> / v]||
     (system-type([<phi, u1> / v]) = (snd([<phi, u1> / v][i])) ∈ {Gamma, fst([<phi, u1> / v][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)  \mwedge{}  (\mforall{}i:\mBbbN{}||v||.  (system-type(v)  =  (snd(v[i]))))
\mvdash{}  Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));[<phi,  u1>  /  v]))  \mvdash{}  system-type([<phi,  u1>  /  v])
\mwedge{}  (\mforall{}i:\mBbbN{}||[<phi,  u1>  /  v]||.  (system-type([<phi,  u1>  /  v])  =  (snd([<phi,  u1>  /  v][i]))))


By

---

Latex:
Assert  \mkleeneopen{}Gamma,  (phi  \mwedge{}  \mbackslash{}/(map(\mlambda{}p.(fst(p));v)))  \mvdash{}  u1  =  system-type(v)\mkleeneclose{}\mcdot{}

---

Home Index