---

Step * 3 of Lemma cubical-subset-is-context-subset


1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ I,psi = formal-cube(I), λJ,f. f(psi) ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
BY
{ ((RepUR ``cubical-subset context-subset rep-sub-sheaf cube-cat`` 0 THEN EqCD) THENA Auto) }

1
.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ (λU.{f:U ⟶ I| (psi f) = 1} )
= (λI@0.{rho:formal-cube(I)(I@0)| λJ,f. f(psi)(rho) = 1 ∈ Point(face_lattice(I@0))} )
∈ (fset(ℕ) ⟶ 𝕌{j'})

2
.....subterm..... T:t
2:n
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ (λU,U',f,ux. ux ⋅ f)
= (λI@0,J,f,rho. f(rho))
∈ (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ ((λU.{f:U ⟶ I| (psi f) = 1} ) x) ⟶ ((λU.{f:U ⟶ I| (psi f) = 1} ) y))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  formal-cube(I)  j\mvdash{}
4.  \mforall{}[X,Y:j\mvdash{}].    X  =  Y  supposing  X  =  Y
\mvdash{}  I,psi  =  formal-cube(I),  \mlambda{}J,f.  f(psi)


By

---

Latex:
((RepUR  ``cubical-subset  context-subset  rep-sub-sheaf  cube-cat``  0  THEN  EqCD)  THENA  Auto)

---

Home Index