---

Step * of Lemma csm-equal

∀[A,B:CubicalSet]. ∀[f:A ⟶ B]. ∀[g:I:(Cname List) ⟶ A(I) ⟶ B(I)].
  f = g ∈ A ⟶ B supposing f = g ∈ (I:(Cname List) ⟶ A(I) ⟶ B(I))
BY
{ RepeatFor 4 (Intro) }

1
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))

---

Latex:

---

Latex:
\mforall{}[A,B:CubicalSet].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[g:I:(Cname  List)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)].    f  =  g  supposing  f  =  g


By

---

Latex:
RepeatFor  4  (Intro)

---

Home Index