---

Step * 1 1 1 1 2 1 1 of Lemma context-map-lemma2


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. I : fset(ℕ)
4. rho : Gamma(I)
5. i : ℕ
6. ¬i ∈ I
7. <s(rho)> ∈ I+i,s(phi(rho)) j⟶ Gamma, phi
8. ∀[u:{I+i,s(phi(rho)) ⊢ _:(𝕀)<s(rho)>}]. ((<s(rho)>;u) ∈ cube_set_map{[j | j]:l}(I+i,s(phi(rho)); Gamma, phi.𝕀))
9. (<s(rho)>;λJ,f. (f i)) ∈ cube_set_map{[j | j]:l}(I+i,s(phi(rho)); Gamma, phi.𝕀)
10. ∀[A,B:j⊢]. ∀[f:A j⟶ B]. ∀[g:I:fset(ℕ) ⟶ A(I) ⟶ B(I)].
      f = g ∈ A j⟶ B supposing f = g ∈ (I:fset(ℕ) ⟶ A(I) ⟶ B(I))
11. A : fset(ℕ)
12. f : A ⟶ I+i
13. (s(phi(rho)) f) = 1
14. phi(f(s(rho))) = 1 ∈ Point(face_lattice(A))
⊢ <f(s(rho)), (<i> s(rho) f)> ∈ alpha:Gamma, phi(A) × 𝕀(alpha)
BY
{ (Auto THEN (RWO "interval-type-at" 0 THENA Auto) THEN RepUR ``interval-presheaf`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  I  :  fset(\mBbbN{})
4.  rho  :  Gamma(I)
5.  i  :  \mBbbN{}
6.  \mneg{}i  \mmember{}  I
7.  <s(rho)>  \mmember{}  I+i,s(phi(rho))  j{}\mrightarrow{}  Gamma,  phi
8.  \mforall{}[u:\{I+i,s(phi(rho))  \mvdash{}  \_:(\mBbbI{})<s(rho)>\}]
          ((<s(rho)>u)  \mmember{}  cube\_set\_map\{[j  |  j]:l\}(I+i,s(phi(rho));  Gamma,  phi.\mBbbI{}))
9.  (<s(rho)>\mlambda{}J,f.  (f  i))  \mmember{}  cube\_set\_map\{[j  |  j]:l\}(I+i,s(phi(rho));  Gamma,  phi.\mBbbI{})
10.  \mforall{}[A,B:j\mvdash{}].  \mforall{}[f:A  j{}\mrightarrow{}  B].  \mforall{}[g:I:fset(\mBbbN{})  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)].    f  =  g  supposing  f  =  g
11.  A  :  fset(\mBbbN{})
12.  f  :  A  {}\mrightarrow{}  I+i
13.  (s(phi(rho))  f)  =  1
14.  phi(f(s(rho)))  =  1
\mvdash{}  <f(s(rho)),  (<i>  s(rho)  f)>  \mmember{}  alpha:Gamma,  phi(A)  \mtimes{}  \mBbbI{}(alpha)


By

---

Latex:
(Auto  THEN  (RWO  "interval-type-at"  0  THENA  Auto)  THEN  RepUR  ``interval-presheaf``  0  THEN  Auto)

---

Home Index