---

Step * of Lemma discrete-map-is-constant2

No Annotations
∀[T:Type]. ∀[I:fset(ℕ)]. ∀[phi:𝔽(I)]. ∀[s:I,phi ⟶ discrete-cube(T)]. ∀[f:{f:I ⟶ I| (phi f) = 1} ].
  s = (λJ,g. (s I f)) ∈ I,phi ⟶ discrete-cube(T) 
  supposing ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((phi g) = 1 ⇒ (g = f ⋅ g ∈ J ⟶ I))
BY
{ (Intros
   THEN DCubeSetMap ``discrete-cube cubical-subset rep-sub-sheaf`` (-3)
   THEN D -3
   THEN DCubeSetMap ``discrete-cube cubical-subset rep-sub-sheaf`` 0
   THEN EqTypeCD
   THEN Try (Trivial)) }

1
1. T : Type
2. I : fset(ℕ)
3. phi : 𝔽(I)
4. s : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(s A x)) = (λx.(s B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T))
6. f : {f:I ⟶ I| (phi f) = 1} 
7. ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((phi g) = 1 ⇒ (g = f ⋅ g ∈ J ⟶ I))
⊢ s = (λJ,g. (s I f)) ∈ (A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T)

2
.....wf..... 
1. T : Type
2. I : fset(ℕ)
3. phi : 𝔽(I)
4. s : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
5. ∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(s A x)) = (λx.(s B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T))
6. f : {f:I ⟶ I| (phi f) = 1} 
7. ∀[J:fset(ℕ)]. ∀[g:J ⟶ I].  ((phi g) = 1 ⇒ (g = f ⋅ g ∈ J ⟶ I))
8. trans : A:fset(ℕ) ⟶ {f:A ⟶ I| (phi f) = 1}  ⟶ T
⊢ istype(∀A,B:fset(ℕ). ∀g:B ⟶ A.  ((λx.(trans A x)) = (λx.(trans B x ⋅ g)) ∈ ({f:A ⟶ I| (phi f) = 1}  ⟶ T)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:\mBbbF{}(I)].  \mforall{}[s:I,phi  {}\mrightarrow{}  discrete-cube(T)].  \mforall{}[f:\{f:I  {}\mrightarrow{}  I|  (phi  f)  =  1\}  ].
    s  =  (\mlambda{}J,g.  (s  I  f))  supposing  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[g:J  {}\mrightarrow{}  I].    ((phi  g)  =  1  {}\mRightarrow{}  (g  =  f  \mcdot{}  g))


By

---

Latex:
(Intros
  THEN  DCubeSetMap  ``discrete-cube  cubical-subset  rep-sub-sheaf``  (-3)
  THEN  D  -3
  THEN  DCubeSetMap  ``discrete-cube  cubical-subset  rep-sub-sheaf``  0
  THEN  EqTypeCD
  THEN  Try  (Trivial))

---

Home Index