---

Step * 1 of Lemma pi-comp-nu_wf


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. J : fset(ℕ)
8. f : J ⟶ I
9. u1 : A(f((i1)(rho)))
10. j : {j:ℕ| ¬j ∈ J} 
⊢ let v' = fill_from_comp(Gamma;A;cA) J j f,i=1-j(rho) 0 () u1 in
      (v' f,i=1-j(rho) r_j) ∈ A(r_j(f,i=1-j(rho)))
BY
{ (RenameVar `u' (-2)
   THEN RepUR ``let`` 0
   THEN (GenConclTerm ⌜fill_from_comp(Gamma;A;cA) J j f,i=1-j(rho) 0 () u⌝⋅
         THENA ((Auto
                 THEN Try (Complete ((InstLemma `section-iota_wf` [⌜Gamma⌝;⌜A⌝;⌜J+j⌝;⌜f,i=1-j(rho)⌝;⌜a⌝;⌜s(0)⌝]⋅
                                      THEN Auto
                                      )))
                 )
                THEN Try ((MemTypeCD
                           THEN Auto
                           THEN D 0
                           THEN Auto
                           THEN (CubicalSubsetICube (-1) THENA Auto)
                           THEN Unfold `name-morph-satisfies` -1
                           THEN (RWO "fl-morph-0" (-1) THENA Auto)
                           THEN (Assert ⌜False⌝⋅ THEN Auto)
                           THEN MoveToConcl (-1)
                           THEN Fold `not` 0
                           THEN Auto))
                )
         )) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ CompOp(A)
4. I : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. rho : Gamma(I+i)
7. J : fset(ℕ)
8. f : J ⟶ I
9. u : A(f((i1)(rho)))
10. j : {j:ℕ| ¬j ∈ J} 
11. v : {a:A(f,i=1-j(rho))| 
         (section-iota(Gamma;A;J+j;f,i=1-j(rho);a) = () ∈ {J+j,s(0) ⊢ _:(A)<f,i=1-j(rho)> o iota})
         ∧ ((a f,i=1-j(rho) (j0)) = u ∈ A((j0)(f,i=1-j(rho))))} 
12. (fill_from_comp(Gamma;A;cA) J j f,i=1-j(rho) 0 () u)
= v
∈ {a:A(f,i=1-j(rho))| 
   (section-iota(Gamma;A;J+j;f,i=1-j(rho);a) = () ∈ {J+j,s(0) ⊢ _:(A)<f,i=1-j(rho)> o iota})
   ∧ ((a f,i=1-j(rho) (j0)) = u ∈ A((j0)(f,i=1-j(rho))))} 
⊢ (v f,i=1-j(rho) r_j) ∈ A(r_j(f,i=1-j(rho)))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  Gamma  \mvdash{}  CompOp(A)
4.  I  :  fset(\mBbbN{})
5.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
6.  rho  :  Gamma(I+i)
7.  J  :  fset(\mBbbN{})
8.  f  :  J  {}\mrightarrow{}  I
9.  u1  :  A(f((i1)(rho)))
10.  j  :  \{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\} 
\mvdash{}  let  v'  =  fill\_from\_comp(Gamma;A;cA)  J  j  f,i=1-j(rho)  0  ()  u1  in
            (v'  f,i=1-j(rho)  r\_j)  \mmember{}  A(r\_j(f,i=1-j(rho)))


By

---

Latex:
(RenameVar  `u'  (-2)
  THEN  RepUR  ``let``  0
  THEN  (GenConclTerm  \mkleeneopen{}fill\_from\_comp(Gamma;A;cA)  J  j  f,i=1-j(rho)  0  ()  u\mkleeneclose{}\mcdot{}
              THENA  ((Auto
                              THEN  Try  (Complete  ((InstLemma  `section-iota\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}J+j\mkleeneclose{};\mkleeneopen{}f,i=1-j(rho)\mkleeneclose{};
                                                                        \mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}s(0)\mkleeneclose{}]\mcdot{}
                                                                        THEN  Auto
                                                                        )))
                              )
                            THEN  Try  ((MemTypeCD
                                                  THEN  Auto
                                                  THEN  D  0
                                                  THEN  Auto
                                                  THEN  (CubicalSubsetICube  (-1)  THENA  Auto)
                                                  THEN  Unfold  `name-morph-satisfies`  -1
                                                  THEN  (RWO  "fl-morph-0"  (-1)  THENA  Auto)
                                                  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                                                  THEN  MoveToConcl  (-1)
                                                  THEN  Fold  `not`  0
                                                  THEN  Auto))
                            )
              ))

---

Home Index