---

Step * 1 of Lemma cube+-


1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. I1 : fset(ℕ)
4. alpha : I1 ⟶ I
5. x1 : 𝕀(alpha)
⊢ <λj.if (j =z i) then x1 else alpha j fi , if (i =z i) then x1 else alpha i fi > = <alpha, x1> ∈ (alpha:I1 ⟶ I × 𝕀(I1)\000C)
BY
{ ((RWO "interval-type-at" (-1) THENA Auto)
   THEN ((Subst' (i =z i) ~ tt 0 THENA Auto) THEN Reduce 0)
   THEN (Enough to prove (λj.if (j =z i) then x1 else alpha j fi ) = alpha ∈ I1 ⟶ I
          Because (EqCD THEN Trivial))
   THEN RepUR ``interval-presheaf`` -1) }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. I1 : fset(ℕ)
4. alpha : I1 ⟶ I
5. x1 : Point(dM(I1))
⊢ (λj.if (j =z i) then x1 else alpha j fi ) = alpha ∈ I1 ⟶ I

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
3.  I1  :  fset(\mBbbN{})
4.  alpha  :  I1  {}\mrightarrow{}  I
5.  x1  :  \mBbbI{}(alpha)
\mvdash{}  <\mlambda{}j.if  (j  =\msubz{}  i)  then  x1  else  alpha  j  fi  ,  if  (i  =\msubz{}  i)  then  x1  else  alpha  i  fi  >  =  <alpha,  x1>


By

---

Latex:
((RWO  "interval-type-at"  (-1)  THENA  Auto)
  THEN  ((Subst'  (i  =\msubz{}  i)  \msim{}  tt  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (Enough  to  prove  (\mlambda{}j.if  (j  =\msubz{}  i)  then  x1  else  alpha  j  fi  )  =  alpha
                Because  (EqCD  THEN  Trivial))
  THEN  RepUR  ``interval-presheaf``  -1)

---

Home Index