:PROPERTIES: :ID: 89e1f424-4500-44c8-b60e-70269b4a2b1d :mtime: 20240111103142 :ctime: 20240111103140 :END: #+title: Opposite Category #+filetags: :public:project: * Definition of an Opposite Category Let $C$ be a [[id:12d70e9c-5793-47b3-8db0-8bc83c0f3925][Category]]. The opposite category, written as $C^{op}$, has all the arrows reversed, specifically 1) The objects of $C^{op}$ are the objects of $C$ 2) The arrows of $C^{op}$ are the reversed/flipped arrows of $C$ 3) The identity arrow of $C^{op}$ is the identity arrow of $C$. 4) The composition on $C^{op}$ is reversed composition on $C$. Also, the consistency conditions of a category are satisfied. 1) Identity cancellation on $C^{op}$ follows from identity cancaellation on $C$ 2) Associativity on $C^{op}$ follows from associtivity on $C$ * Opposite Category in Agda #+BEGIN_SRC agda oppositeCategory : (_⇨_ : obj → obj → Type ℓ) → Category _⇨_ → Category (flip _⇨_) oppositeCategory arr cat = record { id = id cat ; _≫_ = flip (_≫_ cat) ; id-right = id-left cat ; id-left = id-right cat ; assoc = λ f g h → sym (assoc cat h g f)} #+END_SRC