---

Step * 1 1 1 of Lemma csm-equal


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)
BY
{ (InstLemma `cubical-set-is-functor` []
   THEN D -1
   THEN BLemma `nat-trans-equal`
   THEN Try ((RepUR ``cat-ob name-cat type-cat cat-arrow`` 0 THEN Fold `I-cube` 0 THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  CubicalSet
2.  B  :  CubicalSet
3.  f  :  nat-trans(NameCat;TypeCat;A;B)
4.  g  :  I:(Cname  List)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)
5.  f  =  g
\mvdash{}  f  =  g


By

---

Latex:
(InstLemma  `cubical-set-is-functor`  []
  THEN  D  -1
  THEN  BLemma  `nat-trans-equal`
  THEN  Try  ((RepUR  ``cat-ob  name-cat  type-cat  cat-arrow``  0  THEN  Fold  `I-cube`  0  THEN  Auto))
  THEN  Auto)

---

Home Index