---

Step * of Lemma subset-trans_wf

No Annotations
∀[I,J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[psi:𝔽(I)].  (subset-trans(I;J;f;psi) ∈ J,(psi)<f> j⟶ I,psi)
BY
{ (InstLemma `face-presheaf_wf` [⌜parm{j}⌝]⋅
   THEN Intros
   THEN Unhide
   THEN Unfold `subset-trans` 0
   THEN DCubeSetMap ``cubical-subset rep-sub-sheaf`` 0
   THEN MemTypeCD) }

1
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
⊢ λK,g. f ⋅ g ∈ A:fset(ℕ) ⟶ {f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:A ⟶ I| (psi f) = 1} 

2
.....set predicate..... 
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
⊢ ∀A,B:fset(ℕ). ∀g:B ⟶ A.
    ((λx.(λK,g. f ⋅ g) A x ⋅ g) = (λx.((λK,g. f ⋅ g) B x ⋅ g)) ∈ ({f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:B ⟶ I| (psi f\000C) = 1} ))

3
.....wf..... 
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
6. trans : A:fset(ℕ) ⟶ {f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:A ⟶ I| (psi f) = 1} 
⊢ istype(∀A,B:fset(ℕ). ∀g:B ⟶ A.
           ((λx.trans A x ⋅ g) = (λx.(trans B x ⋅ g)) ∈ ({f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:B ⟶ I| (psi f) = 1} ))\000C)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[psi:\mBbbF{}(I)].    (subset-trans(I;J;f;psi)  \mmember{}  J,(psi)<f>  j{}\mrightarrow{}  I,psi)


By

---

Latex:
(InstLemma  `face-presheaf\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{}]\mcdot{}
  THEN  Intros
  THEN  Unhide
  THEN  Unfold  `subset-trans`  0
  THEN  DCubeSetMap  ``cubical-subset  rep-sub-sheaf``  0
  THEN  MemTypeCD)

---

Home Index