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