---

Step * 1 1 of Lemma discrete-fun-at


1. A : Type
2. B : Type
3. I : fset(ℕ)
4. a : ()(I)
5. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
⊢ (f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (discr(A) ⟶ discr(B))(a)
BY
{ (All (RepUR ``cubical-fun cubical-fun-family discrete-cubical-type``)
   THEN (DVar `f' THEN RepUR ``cubical-type-at`` -2)
   THEN EqTypeCD
   THEN Auto) }

1
1. A : Type
2. B : Type
3. I : fset(ℕ)
4. a : ()(I)
5. f : I:fset(ℕ)
⟶ a:()(I)
⟶ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
6. ∀I,J:fset(ℕ). ∀f@0:J ⟶ I. ∀a:()(I).
     ((f I a a f@0)
     = (f J f@0(a))
     ∈ <λI,a. {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| 
               ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
       , λI,J,f,a,w,K,g. (w K f ⋅ g)
       >(f@0(a)))
⊢ (f I a) = (λJ,h,u. (f {} ⋅ {} 1 u)) ∈ (J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B)

2
1. A : Type
2. B : Type
3. I : fset(ℕ)
4. a : ()(I)
5. f : I:fset(ℕ)
⟶ a:()(I)
⟶ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
6. ∀I,J:fset(ℕ). ∀f@0:J ⟶ I. ∀a:()(I).
     ((f I a a f@0)
     = (f J f@0(a))
     ∈ <λI,a. {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| 
               ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
       , λI,J,f,a,w,K,g. (w K f ⋅ g)
       >(f@0(a)))
7. J : fset(ℕ)
8. K : fset(ℕ)
9. f@0 : J ⟶ I
10. g : K ⟶ J
11. u : A
⊢ (f I a J f@0 u) = (f I a K f@0 ⋅ g u) ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  I  :  fset(\mBbbN{})
4.  a  :  ()(I)
5.  f  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
\mvdash{}  (f  I  a)  =  (\mlambda{}J,h,u.  (f  \{\}  \mcdot{}  \{\}  1  u))


By

---

Latex:
(All  (RepUR  ``cubical-fun  cubical-fun-family  discrete-cubical-type``)
  THEN  (DVar  `f'  THEN  RepUR  ``cubical-type-at``  -2)
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index