Control.Category.Instances.Op

This module defines the opposite category, which is an operation
on a category that flips the direction of its morphisms.

Definitions

record Op : (a -> b -> Type) -> b -> a -> Type

  The opposite category of `cat`.

Totality: total
Visibility: public export
Constructor: 

MkOp : cat y x -> Op cat x y

Projection: 

.runOp : Op cat x y -> cat y x

Hints:

Braided cat ten i => Braided (Op cat) ten i

Cocartesian cat ten i => Cartesian (Op cat) ten i

CatBifunctor catA catB cat' f => CatBifunctor (Op catA) (Op catB) (Op cat') f

CatFunctor cat cat' f => CatFunctor (Op cat) (Op cat') f

Category cat => Category (Op cat)

Cartesian cat ten i => Cocartesian (Op cat) ten i

MonSymmetric cat ten i => MonSymmetric (Op cat) ten i

Monoidal cat ten i => Monoidal (Op cat) ten i

Semigroupoid cat => Semigroupoid (Op cat)

Traced cat ten i => Traced (Op cat) ten i

.runOp : Op cat x y -> cat y x

Totality: total
Visibility: public export

runOp : Op cat x y -> cat y x

Totality: total
Visibility: public export

Op : SemigroupoidR -> SemigroupoidR

Totality: total
Visibility: public export

Op : CategoryR -> CategoryR

Totality: total
Visibility: public export

Op : MonoidalR -> MonoidalR

Totality: total
Visibility: public export

Op : BraidedR -> BraidedR

Totality: total
Visibility: public export

Op : CocartesianR -> CartesianR

Totality: total
Visibility: public export

Op : CartesianR -> CocartesianR

Totality: total
Visibility: public export

Op : TracedR -> TracedR

Totality: total
Visibility: public export

Op : FunctorR cat cat' -> FunctorR (Op cat) (Op cat')

Totality: total
Visibility: public export