---

Step * 1 1 of Lemma csm-equal


1. A : CubicalSet
2. B : CubicalSet
3. f : A ⟶ B
4. g : I:(Cname List) ⟶ A(I) ⟶ B(I)
5. f = g ∈ (I:(Cname List) ⟶ A(I) ⟶ B(I))
⊢ f = g ∈ A ⟶ B
BY
{ All (RepUR ``cube-set-map``) }

1
1. A : CubicalSet
2. B : CubicalSet
3. f : nat-trans(NameCat;TypeCat;A;B)
4. g : I:(Cname List) ⟶ A(I) ⟶ B(I)
5. f = g ∈ (I:(Cname List) ⟶ A(I) ⟶ B(I))
⊢ f = g ∈ nat-trans(NameCat;TypeCat;A;B)

---

Latex:

---

Latex:

1.  A  :  CubicalSet
2.  B  :  CubicalSet
3.  f  :  A  {}\mrightarrow{}  B
4.  g  :  I:(Cname  List)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)
5.  f  =  g
\mvdash{}  f  =  g


By

---

Latex:
All  (RepUR  ``cube-set-map``)

---

Home Index