---

Step * of Lemma subset-iota_wf

No Annotations
∀[I:fset(ℕ)]. ∀[psi:𝔽(I)].  (iota ∈ I,psi j⟶ formal-cube(I))
BY
{ (InstLemma `face-presheaf_wf` [⌜parm{j}⌝]⋅
   THEN Intros
   THEN Unhide
   THEN Unfold `subset-iota` 0
   THEN DCubeSetMap ``cubical-subset rep-sub-sheaf formal-cube`` 0
   THEN MemTypeCD
   THEN Try ((RepeatFor 3 ((D 0 THENL [Auto; Id])) THEN EqualityIsType1))
   THEN Auto
   THEN RepUR ``name-morph-satisfies`` 0
   THEN MemTypeCD
   THEN Auto
   THEN RWO "fl-morph-comp" 0
   THEN Auto
   THEN RepUR ``compose`` 0
   THEN Auto) }

1
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. psi : 𝔽(I)
4. trans : A:fset(ℕ) ⟶ {f:A ⟶ I| (psi f) = 1}  ⟶ A ⟶ I
5. A : fset(ℕ)
6. B : fset(ℕ)
7. g : B ⟶ A
8. ∀f:A ⟶ I. ((psi f) = 1 ∈ Type)
9. x : A ⟶ I
10. (psi x) = 1
⊢ ((psi)<x>)<g> = 1 ∈ Point(face_lattice(B))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[psi:\mBbbF{}(I)].    (iota  \mmember{}  I,psi  j{}\mrightarrow{}  formal-cube(I))


By

---

Latex:
(InstLemma  `face-presheaf\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{}]\mcdot{}
  THEN  Intros
  THEN  Unhide
  THEN  Unfold  `subset-iota`  0
  THEN  DCubeSetMap  ``cubical-subset  rep-sub-sheaf  formal-cube``  0
  THEN  MemTypeCD
  THEN  Try  ((RepeatFor  3  ((D  0  THENL  [Auto;  Id]))  THEN  EqualityIsType1))
  THEN  Auto
  THEN  RepUR  ``name-morph-satisfies``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  RWO  "fl-morph-comp"  0
  THEN  Auto
  THEN  RepUR  ``compose``  0
  THEN  Auto)

---

Home Index