0 | ||| This module defines the opposite category, which is an operation
  1 | ||| on a category that flips the direction of its morphisms.
  2 | module Control.Category.Instances.Op
  3 |
  4 | import Control.Category
  5 | import Control.Category.Records
  6 |
  7 | %default total
  8 |
  9 | ||| The opposite category of `cat`.
 10 | public export
 11 | record Op (cat : a -> b -> Type)
 12 |           (x : b) (y : a) where
 13 |   constructor MkOp
 14 |   runOp : cat y x
 15 |
 16 |
 17 | ------------------------------------------------------------
 18 | -- Interface Style
 19 | ------------------------------------------------------------
 20 |
 21 | public export
 22 | Semigroupoid cat => Semigroupoid (Op cat) where
 23 |   MkOp f . MkOp g = MkOp (g . f)
 24 |
 25 | public export
 26 | Category cat => Category (Op cat) where
 27 |   id = MkOp id
 28 |   MkOp f . MkOp g = MkOp (g . f)
 29 |
 30 | public export
 31 | CatFunctor cat cat' f => CatFunctor (Op cat) (Op cat') f where
 32 |   map = MkOp . map . runOp
 33 |
 34 | public export
 35 | CatBifunctor catA catB cat' f => CatBifunctor (Op catA) (Op catB) (Op cat') f where
 36 |   bimap (MkOp f) (MkOp g) = MkOp $ bimap f g
 37 |
 38 | public export
 39 | {ten,i : _} -> Monoidal cat ten i => Monoidal (Op cat) ten i where
 40 |   assoc = MkOp assoc'
 41 |   assoc' = MkOp assoc
 42 |   unitl = MkOp unitl'
 43 |   unitl' = MkOp unitl
 44 |   unitr = MkOp unitr'
 45 |   unitr' = MkOp unitr
 46 |
 47 | public export
 48 | {ten,i : _} -> Braided cat ten i => Braided (Op cat) ten i where
 49 |   braid = MkOp braid'
 50 |   braid' = MkOp braid
 51 |
 52 | public export
 53 | {ten,i : _} -> Cocartesian cat ten i => Cartesian (Op cat) ten i where
 54 |   projl = MkOp injl
 55 |   projr = MkOp injr
 56 |   prod (MkOp f) (MkOp g) = MkOp $ coprod f g
 57 |   split = MkOp merge
 58 |   elim = MkOp $ intro {ten}
 59 |
 60 | public export
 61 | {ten,i : _} -> Cartesian cat ten i => Cocartesian (Op cat) ten i where
 62 |   injl = MkOp projl
 63 |   injr = MkOp projr
 64 |   coprod (MkOp f) (MkOp g) = MkOp $ prod f g
 65 |   merge = MkOp split
 66 |   intro = MkOp $ elim {ten}
 67 |
 68 | public export
 69 | {ten,i : _} -> Traced cat ten i => Traced (Op cat) ten i where
 70 |   tracel = MkOp . tracel . runOp
 71 |   tracer = MkOp . tracer . runOp
 72 |
 73 |
 74 | ------------------------------------------------------------
 75 | -- Record Style
 76 | ------------------------------------------------------------
 77 |
 78 | namespace SemigroupoidR
 79 |   public export
 80 |   Op : (cat : SemigroupoidR) -> SemigroupoidR
 81 |   Op (MkSemigroupoidR cat) = MkSemigroupoidR (Op cat)
 82 |
 83 | namespace CategoryR
 84 |   public export
 85 |   Op : (cat : CategoryR) -> CategoryR
 86 |   Op (MkCategoryR cat) = MkCategoryR (Op cat)
 87 |
 88 | namespace MonoidalR
 89 |   public export
 90 |   Op : (cat : MonoidalR) -> MonoidalR
 91 |   Op (MkMonoidalR cat ten i) = MkMonoidalR (Op cat) ten i
 92 |
 93 | namespace BraidedR
 94 |   public export
 95 |   Op : (cat : BraidedR) -> BraidedR
 96 |   Op (MkBraidedR cat ten i) = MkBraidedR (Op cat) ten i
 97 |
 98 | namespace CartesianR
 99 |   public export
100 |   Op : (cat : CocartesianR) -> CartesianR
101 |   Op (MkCocartesianR cat ten i) = MkCartesianR (Op cat) ten i
102 |
103 | namespace CocartesianR
104 |   public export
105 |   Op : (cat : CartesianR) -> CocartesianR
106 |   Op (MkCartesianR cat ten i) = MkCocartesianR (Op cat) ten i
107 |
108 | namespace TracedR
109 |   public export
110 |   Op : (cat : TracedR) -> TracedR
111 |   Op (MkTracedR cat ten i) = MkTracedR (Op cat) ten i
112 |
113 |
114 | namespace FunctorR
115 |   public export
116 |   Op : (f : FunctorR cat cat') -> FunctorR (Op cat) (Op cat')
117 |   Op {cat=MkCategoryR{},cat'=MkCategoryR{}} (MkFunctorR f) = MkFunctorR f
118 |