---

Step * 2 of Lemma system-type-properties


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]) ⊢ _})))
BY
{ ((D 0 THENA Auto)
   THEN DVar `u'
   THEN Unfold `compatible-system` -1
   THEN (InstLemma `pairwise-cons` [⌜parm{[i' | j']}⌝;⌜phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}⌝;⌜<phi, u1>⌝;⌜v⌝;
         ⌜λ2phiA1 phiA2.let phi1,A1 = phiA1 
                        in let phi2,A2 = phiA2 
                           in A1 = A2 ∈ {Gamma, (phi1 ∧ phi2) ⊢ _}⌝]⋅
         THENA Auto
         )
   THEN (D -1 THEN Thin (-1) THEN RepeatFor 2 ((D -1 THENA Auto)))
   THEN Fold `compatible-system` (-2)
   THEN Thin (-3)
   THEN (D -3 THENA 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) ∧ (∀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]) ⊢ _}))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  u  :  phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\}
3.  v  :  (phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\})  List
4.  compatible-system\{i:l\}(Gamma;v)
{}\mRightarrow{}  (Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));v))  \mvdash{}  system-type(v)  \mwedge{}  (\mforall{}i:\mBbbN{}||v||.  (system-type(v)  =  (snd(v[i])))))
\mvdash{}  compatible-system\{i:l\}(Gamma;[u  /  v])
{}\mRightarrow{}  (Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));[u  /  v]))  \mvdash{}  system-type([u  /  v])
      \mwedge{}  (\mforall{}i:\mBbbN{}||[u  /  v]||.  (system-type([u  /  v])  =  (snd([u  /  v][i])))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  DVar  `u'
  THEN  Unfold  `compatible-system`  -1
  THEN  (InstLemma  `pairwise-cons`  [\mkleeneopen{}parm\{[i'  |  j']\}\mkleeneclose{};\mkleeneopen{}phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\}\mkleeneclose{};\mkleeneopen{}<phi
                                                                                                                                                                                        ,  u1
                                                                                                                                                                                        >\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}phiA1  phiA2.let  phi1,A1  =  phiA1 
                                            in  let  phi2,A2  =  phiA2 
                                                  in  A1  =  A2\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (D  -1  THEN  Thin  (-1)  THEN  RepeatFor  2  ((D  -1  THENA  Auto)))
  THEN  Fold  `compatible-system`  (-2)
  THEN  Thin  (-3)
  THEN  (D  -3  THENA  Auto))

---

Home Index