---

Step * 1 2 of Lemma csm-equal

.....wf..... 
1. A : CubicalSet
2. B : CubicalSet
3. f : A ⟶ B
4. g : I:(Cname List) ⟶ A(I) ⟶ B(I)
⊢ f = g ∈ (I:(Cname List) ⟶ A(I) ⟶ B(I)) ∈ ℙ
BY
{ (RepeatFor 2 (DVar `A')
   THEN RepeatFor 2 (DVar `B')
   THEN DVar `f'
   THEN All (RepUR ``cat-ob cat-arrow name-cat type-cat 
                     functor-ob cat-comp I-cube``)⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  (DVar  `A')
  THEN  RepeatFor  2  (DVar  `B')
  THEN  DVar  `f'
  THEN  All  (RepUR  ``cat-ob  cat-arrow  name-cat  type-cat 
                                      functor-ob  cat-comp  I-cube``)\mcdot{}
  THEN  Auto)

---

Home Index