---

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

.....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))
BY
{ RepeatFor 4 (((FunExt THEN Reduce 0) THENA Auto)) }

1
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)))
5. x : fset(ℕ)
6. y : fset(ℕ)
7. x1 : y ⟶ x
8. x2 : {f:x ⟶ I| (psi f) = 1} 
⊢ x2 ⋅ x1 = x1(x2) ∈ {f:y ⟶ I| (psi f) = 1} 

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{}  (\mlambda{}U,U',f,ux.  ux  \mcdot{}  f)  =  (\mlambda{}I@0,J,f,rho.  f(rho))


By

---

Latex:
RepeatFor  4  (((FunExt  THEN  Reduce  0)  THENA  Auto))

---

Home Index