Description: Definition of the operation generating opposite functors. Definition 3.41 of Adamek p. 39. The object part of the functor is unchanged while the morphism part is transposed due to reversed direction of arrows in the opposite category. The opposite functor is a functor on opposite categories ( oppfoppc ). (Contributed by Zhi Wang, 4-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-oppf | |- oppFunc = ( f e. _V , g e. _V |-> <. f , tpos g >. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | coppf | |- oppFunc |
|
| 1 | vf | |- f |
|
| 2 | cvv | |- _V |
|
| 3 | vg | |- g |
|
| 4 | 1 | cv | |- f |
| 5 | 3 | cv | |- g |
| 6 | 5 | ctpos | |- tpos g |
| 7 | 4 6 | cop | |- <. f , tpos g >. |
| 8 | 1 3 2 2 7 | cmpo | |- ( f e. _V , g e. _V |-> <. f , tpos g >. ) |
| 9 | 0 8 | wceq | |- oppFunc = ( f e. _V , g e. _V |-> <. f , tpos g >. ) |