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 : _} -> MonSymmetric cat ten i => MonSymmetric (Op cat) ten i where
 54 |   permute p = MkOp $ replace {p = cat _ . TenSeq ten i}
 55 |     (trans (sym $ permuteListComp xs (inverse p) p) $
 56 |       trans (cong (permuteList xs) (compInvLeft p)) $
 57 |         permuteListId xs) $
 58 |     permute {cat,ten,xs = permuteList xs p} $ inverse $ rewrite permuteListLength xs p in p
 59 |
 60 | public export
 61 | {ten,i : _} -> Cocartesian cat ten i => Cartesian (Op cat) ten i where
 62 |   projl = MkOp injl
 63 |   projr = MkOp injr
 64 |   prod (MkOp f) (MkOp g) = MkOp $ coprod f g
 65 |   split = MkOp merge
 66 |   elim = MkOp $ intro {ten}
 67 |
 68 | public export
 69 | {ten,i : _} -> Cartesian cat ten i => Cocartesian (Op cat) ten i where
 70 |   injl = MkOp projl
 71 |   injr = MkOp projr
 72 |   coprod (MkOp f) (MkOp g) = MkOp $ prod f g
 73 |   merge = MkOp split
 74 |   intro = MkOp $ elim {ten}
 75 |
 76 | public export
 77 | {ten,i : _} -> Traced cat ten i => Traced (Op cat) ten i where
 78 |   tracel = MkOp . tracel . runOp
 79 |   tracer = MkOp . tracer . runOp
 80 |
 81 |
 82 | ------------------------------------------------------------
 83 | -- Record Style
 84 | ------------------------------------------------------------
 85 |
 86 | namespace SemigroupoidR
 87 |   public export
 88 |   Op : (cat : SemigroupoidR) -> SemigroupoidR
 89 |   Op (MkSemigroupoidR cat) = MkSemigroupoidR (Op cat)
 90 |
 91 | namespace CategoryR
 92 |   public export
 93 |   Op : (cat : CategoryR) -> CategoryR
 94 |   Op (MkCategoryR cat) = MkCategoryR (Op cat)
 95 |
 96 | namespace MonoidalR
 97 |   public export
 98 |   Op : (cat : MonoidalR) -> MonoidalR
 99 |   Op (MkMonoidalR cat ten i) = MkMonoidalR (Op cat) ten i
100 |
101 | namespace BraidedR
102 |   public export
103 |   Op : (cat : BraidedR) -> BraidedR
104 |   Op (MkBraidedR cat ten i) = MkBraidedR (Op cat) ten i
105 |
106 | namespace CartesianR
107 |   public export
108 |   Op : (cat : CocartesianR) -> CartesianR
109 |   Op (MkCocartesianR cat ten i) = MkCartesianR (Op cat) ten i
110 |
111 | namespace CocartesianR
112 |   public export
113 |   Op : (cat : CartesianR) -> CocartesianR
114 |   Op (MkCartesianR cat ten i) = MkCocartesianR (Op cat) ten i
115 |
116 | namespace TracedR
117 |   public export
118 |   Op : (cat : TracedR) -> TracedR
119 |   Op (MkTracedR cat ten i) = MkTracedR (Op cat) ten i
120 |
121 |
122 | namespace FunctorR
123 |   public export
124 |   Op : (f : FunctorR cat cat') -> FunctorR (Op cat) (Op cat')
125 |   Op {cat=MkCategoryR{},cat'=MkCategoryR{}} (MkFunctorR f) = MkFunctorR f
126 |