---

Step * of Lemma mk-nat-trans_wf

∀[C,D:SmallCategory]. ∀[F,G:Functor(C;D)]. ∀[trans:A:cat-ob(C) ⟶ (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) A))].
  x |→ trans[x] ∈ nat-trans(C;D;F;G) 
  supposing ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
              ((cat-comp(D) (functor-ob(F) A) (functor-ob(G) A) (functor-ob(G) B) trans[A] (functor-arrow(G) A B g))
              = (cat-comp(D) (functor-ob(F) A) (functor-ob(F) B) (functor-ob(G) B) (functor-arrow(F) A B g) trans[B])
              ∈ (cat-arrow(D) (functor-ob(F) A) (functor-ob(G) B)))
BY
{ (Auto THEN MemTypeCD THEN Auto THEN RepUR ``mk-nat-trans`` 0 THEN Try (BackThruSomeHyp) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto  THEN  RepUR  ``mk-nat-trans``  0  THEN  Try  (BackThruSomeHyp)  THEN  Auto)

---

Home Index