---

Step * 1 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,alpha. (f I alpha I 1) ∈ I:fset(ℕ) ⟶ a:X(I) ⟶ a:A ⟶ B[a]
BY
{ (DVar `f'
   THEN All (RepUR ``cubical-pi cubical-pi-family``)
   THEN RepeatFor 2 (((FunExt THENA Auto) THEN Reduce 0))
   THEN InferEqualType
   THEN Auto) }

1
1. A : Type
2. B : A ⟶ Type
3. X : CubicalSet{j}
4. f : I:fset(ℕ)
⟶ a:X(I)
⟶ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:discr(A)(f(a)) ⟶ discrete-family(A;a.B[a])((f(a);u))| 
    ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:discr(A)(f(a)).
      ((w J f u (f(a);u) g) = (w K f ⋅ g (u f(a) g)) ∈ discrete-family(A;a.B[a])(g((f(a);u))))} 
5. ∀I,J:fset(ℕ). ∀f@0:J ⟶ I. ∀a:X(I).
     ((λK,g. (f I a K f@0 ⋅ g))
     = (f J f@0(a))
     ∈ {w:J@0:fset(ℕ) ⟶ f:J@0 ⟶ J ⟶ u:discr(A)(f(f@0(a))) ⟶ discrete-family(A;a.B[a])((f(f@0(a));u))| 
        ∀J@0,K:fset(ℕ). ∀f:J@0 ⟶ J. ∀g:K ⟶ J@0. ∀u:discr(A)(f(f@0(a))).
          ((w J@0 f u (f(f@0(a));u) g) = (w K f ⋅ g (u f(f@0(a)) g)) ∈ discrete-family(A;a.B[a])(g((f(f@0(a));u))))} )
6. I : fset(ℕ)
7. a : X(I)
⊢ (u:discr(A)(1(a)) ⟶ discrete-family(A;a.B[a])((1(a);u))) = (a:A ⟶ B[a]) ∈ Type

---

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{}  \mlambda{}I,alpha.  (f  I  alpha  I  1)  \mmember{}  I:fset(\mBbbN{})  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  a:A  {}\mrightarrow{}  B[a]


By

---

Latex:
(DVar  `f'
  THEN  All  (RepUR  ``cubical-pi  cubical-pi-family``)
  THEN  RepeatFor  2  (((FunExt  THENA  Auto)  THEN  Reduce  0))
  THEN  InferEqualType
  THEN  Auto)

---

Home Index