---

Step * 1 of Lemma csm-equal


1. [A] : CubicalSet
2. [B] : CubicalSet
3. [f] : A ⟶ B
4. [g] : I:(Cname List) ⟶ A(I) ⟶ B(I)
⊢ f = g ∈ A ⟶ B supposing f = g ∈ (I:(Cname List) ⟶ A(I) ⟶ B(I))
BY
{ D 0 }

1
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

2
.....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)) ∈ ℙ

---

Latex:

---

Latex:

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  supposing  f  =  g


By

---

Latex:
D  0

---

Home Index