---

Step * of Lemma nat-trans-equal

∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[A:nat-trans(C;D;F;G)]. ∀[B:A:cat-ob(C) ⟶ (cat-arrow(D) (functor-ob(F) A) 
                                                                                        (functor-ob(G) A))].
  A = B ∈ nat-trans(C;D;F;G) supposing A = B ∈ (A:cat-ob(C) ⟶ (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) A)))
BY
{ (Auto THEN DVar `A' THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F,G:Functor(C;D)].  \mforall{}[A:nat-trans(C;D;F;G)].
\mforall{}[B:A:cat-ob(C)  {}\mrightarrow{}  (cat-arrow(D)  (functor-ob(F)  A)  (functor-ob(G)  A))].
    A  =  B  supposing  A  =  B


By

---

Latex:
(Auto  THEN  DVar  `A'  THEN  EqTypeCD  THEN  Auto)

---

Home Index