---

Step * 1 of Lemma subset-iota_wf


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))
BY
{ (RepUR ``name-morph-satisfies`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  \mBbbF{}  \mmember{}  small\_cubical\_set\{j:l\}
2.  I  :  fset(\mBbbN{})
3.  psi  :  \mBbbF{}(I)
4.  trans  :  A:fset(\mBbbN{})  {}\mrightarrow{}  \{f:A  {}\mrightarrow{}  I|  (psi  f)  =  1\}    {}\mrightarrow{}  A  {}\mrightarrow{}  I
5.  A  :  fset(\mBbbN{})
6.  B  :  fset(\mBbbN{})
7.  g  :  B  {}\mrightarrow{}  A
8.  \mforall{}f:A  {}\mrightarrow{}  I.  ((psi  f)  =  1  \mmember{}  Type)
9.  x  :  A  {}\mrightarrow{}  I
10.  (psi  x)  =  1
\mvdash{}  ((psi)<x>)<g>  =  1


By

---

Latex:
(RepUR  ``name-morph-satisfies``  -1  THEN  Auto)

---

Home Index