Description: A natural transformation is a function on the objects of C . (Contributed by Mario Carneiro, 6-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | natrcl.1 | ||
natixp.2 | |||
natixp.b | |||
Assertion | natfn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | natrcl.1 | ||
2 | natixp.2 | ||
3 | natixp.b | ||
4 | eqid | ||
5 | 1 2 3 4 | natixp | |
6 | ixpfn | ||
7 | 5 6 | syl |