---

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

No Annotations
∀[I:fset(ℕ)]. ∀[phi:{formal-cube(I) ⊢ _:𝔽}].  (formal-cube(I), phi = I,phi(1) ∈ CubicalSet{j})
BY
{ (Intros
   THEN (BLemma `cubical_sets_equal` THENW Auto)
   THEN ((RepUR ``cubical-subset context-subset rep-sub-sheaf`` 0 THEN EqCD) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
⊢ (λI@0.{rho:formal-cube(I)(I@0)| phi(rho) = 1 ∈ Point(face_lattice(I@0))} )
= (λU.{f:cat-arrow(CubeCat) U I| (phi(1) f) = 1} )
∈ (fset(ℕ) ⟶ 𝕌{j'})

2
.....subterm..... T:t
2:n
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
⊢ (λI@0,J,f,rho. f(rho))
= (λU,U',f,ux. (cat-comp(CubeCat) U' U I f ux))
∈ (x:fset(ℕ)
  ⟶ y:fset(ℕ)
  ⟶ y ⟶ x
  ⟶ ((λI@0.{rho:formal-cube(I)(I@0)| phi(rho) = 1 ∈ Point(face_lattice(I@0))} ) x)
  ⟶ ((λI@0.{rho:formal-cube(I)(I@0)| phi(rho) = 1 ∈ Point(face_lattice(I@0))} ) y))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:\{formal-cube(I)  \mvdash{}  \_:\mBbbF{}\}].    (formal-cube(I),  phi  =  I,phi(1))


By

---

Latex:
(Intros
  THEN  (BLemma  `cubical\_sets\_equal`  THENW  Auto)
  THEN  ((RepUR  ``cubical-subset  context-subset  rep-sub-sheaf``  0  THEN  EqCD)  THENA  Auto))

---

Home Index