---

Step * 2 of Lemma discrete-function_wf


1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. f : {X ⊢ _:Πdiscr(A) discrete-family(A;a.B[a])}
⊢ ∀I,J:fset(ℕ). ∀f@0:J ⟶ I. ∀a:X(I).  ((f I a I 1) = (f J f@0(a) J 1) ∈ (a:A ⟶ B[a]))
BY
{ Auto }

1
1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. f : {X ⊢ _:Πdiscr(A) discrete-family(A;a.B[a])}
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f@0 : J ⟶ I
8. a : X(I)
⊢ (f I a I 1) = (f J f@0(a) J 1) ∈ (a:A ⟶ B[a])

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  X  :  CubicalSet\{j\}
4.  f  :  \{X  \mvdash{}  \_:\mPi{}discr(A)  discrete-family(A;a.B[a])\}
\mvdash{}  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f@0:J  {}\mrightarrow{}  I.  \mforall{}a:X(I).    ((f  I  a  I  1)  =  (f  J  f@0(a)  J  1))


By

---

Latex:
Auto

---

Home Index