---

Step * of Lemma pscm-equal

No Annotations
∀[C:SmallCategory]. ∀[A,B:ps_context{j:l}(C)]. ∀[f:psc_map{j:l}(C; A; B)]. ∀[g:I:cat-ob(C) ⟶ A(I) ⟶ B(I)].
  f = g ∈ psc_map{j:l}(C; A; B) supposing f = g ∈ (I:cat-ob(C) ⟶ A(I) ⟶ B(I))
BY
{ (RepeatFor 5 (Intro) THEN D 0 THEN Try ((Unfold `psc_map` 0 THEN BLemma `nat-trans-equal`)) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[A,B:ps\_context\{j:l\}(C)].  \mforall{}[f:psc\_map\{j:l\}(C;  A;  B)].  \mforall{}[g:I:cat-ob(C)
                                                                                                                                                              {}\mrightarrow{}  A(I)
                                                                                                                                                              {}\mrightarrow{}  B(I)].
    f  =  g  supposing  f  =  g


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  D  0
  THEN  Try  ((Unfold  `psc\_map`  0  THEN  BLemma  `nat-trans-equal`))
  THEN  Auto)

---

Home Index