0 | ||| This module defines `Zero`, the one category, which contains one
  1 | ||| single object and one identity morphism.
  2 | module Control.Category.Instances.One
  3 |
  4 | import Control.Category
  5 | import Control.Category.Records
  6 |
  7 | %default total
  8 |
  9 | ||| The one category, or terminal category. This category contains one
 10 | ||| object and one identity morphism.
 11 | public export
 12 | data One : (a,b : ()) -> Type where
 13 |   MkOne : One () ()
 14 |
 15 | public export %inline
 16 | mkOne : One a b
 17 | mkOne {a=(),b=()} = MkOne
 18 |
 19 | public export
 20 | UnitOp : a -> ()
 21 | UnitOp _ = ()
 22 |
 23 | public export
 24 | UnitOp2 : a -> b -> ()
 25 | UnitOp2 _ _ = ()
 26 |
 27 |
 28 | ------------------------------------------------------------
 29 | -- Interface Style
 30 | ------------------------------------------------------------
 31 |
 32 | public export
 33 | Category One where
 34 |   id {a=()} = MkOne
 35 |   MkOne . MkOne = MkOne
 36 |
 37 | %hint
 38 | SemigroupoidOne : Semigroupoid One
 39 | SemigroupoidOne = FromCategory
 40 |
 41 |
 42 | public export
 43 | CatFunctor cat One UnitOp where
 44 |   map _ = MkOne
 45 |
 46 | public export
 47 | CatMonad One UnitOp where
 48 |   unit {a=()} = MkOne
 49 |   join = MkOne
 50 |
 51 | public export
 52 | CatBifunctor catA catB One UnitOp2 where
 53 |   bimap _ _ = MkOne
 54 |
 55 | public export
 56 | Monoidal One UnitOp2 () where
 57 |   assoc = MkOne
 58 |   assoc' = MkOne
 59 |   unitl {a=()} = MkOne
 60 |   unitl' {a=()} = MkOne
 61 |   unitr {a=()} = MkOne
 62 |   unitr' {a=()} = MkOne
 63 |
 64 | public export
 65 | Braided One UnitOp2 () where
 66 |   braid = MkOne
 67 |   braid' = MkOne
 68 |
 69 | public export
 70 | MonSymmetric One UnitOp2 () where
 71 |   permute _ = mkOne
 72 |
 73 | public export
 74 | Cartesian One UnitOp2 () where
 75 |   projl {a=()} = MkOne
 76 |   projr {b=()} = MkOne
 77 |   prod {a=()} _ _ = MkOne
 78 |   split {a=()} = MkOne
 79 |   elim {a=()} = MkOne
 80 |
 81 | public export
 82 | Cocartesian One UnitOp2 () where
 83 |   injl {a=()} = MkOne
 84 |   injr {b=()} = MkOne
 85 |   coprod {b=()} _ _ = MkOne
 86 |   merge {a=()} = MkOne
 87 |   intro {a=()} = MkOne
 88 |
 89 | public export
 90 | Closed One UnitOp2 UnitOp2 () where
 91 |   curry {a=()} _ = MkOne
 92 |   uncurry {c=()} _ = MkOne
 93 |
 94 | public export
 95 | Traced One UnitOp2 () where
 96 |   tracel {b=(),c=()} _ = MkOne
 97 |   tracer {a=(),b=()} _ = MkOne
 98 |
 99 | public export
100 | Bimonoidal One UnitOp2 UnitOp2 () () where
101 |   distribl = MkOne
102 |   distribl' = MkOne
103 |   distribr = MkOne
104 |   distribr' = MkOne
105 |   absorbl = MkOne
106 |   absorbl' = MkOne
107 |   absorbr = MkOne
108 |   absorbr' = MkOne
109 |
110 |
111 | ------------------------------------------------------------
112 | -- Record Style
113 | ------------------------------------------------------------
114 |
115 | namespace SemigroupoidR
116 |   public export
117 |   One : SemigroupoidR
118 |   One = MkSemigroupoidR One
119 |
120 | namespace CategoryR
121 |   public export
122 |   One : CategoryR
123 |   One = MkCategoryR One
124 |
125 | namespace MonoidalR
126 |   public export
127 |   One : MonoidalR
128 |   One = MkMonoidalR One UnitOp2 ()
129 |
130 | namespace BraidedR
131 |   public export
132 |   One : BraidedR
133 |   One = MkBraidedR One UnitOp2 ()
134 |
135 | namespace SymmetricR
136 |   public export
137 |   One : SymmetricR
138 |   One = MkSymmetricR One UnitOp2 ()
139 |
140 | namespace CartesianR
141 |   public export
142 |   One : CartesianR
143 |   One = MkCartesianR One UnitOp2 ()
144 |
145 | namespace CocartesianR
146 |   public export
147 |   One : CocartesianR
148 |   One = MkCocartesianR One UnitOp2 ()
149 |
150 | namespace ClosedR
151 |   public export
152 |   One : ClosedR
153 |   One = MkClosedR One UnitOp2 UnitOp2 ()
154 |
155 | namespace TracedR
156 |   public export
157 |   One : TracedR
158 |   One = MkTracedR One UnitOp2 ()
159 |
160 | namespace BimonoidalR
161 |   public export
162 |   One : BimonoidalR
163 |   One = MkBimonoidalR One UnitOp2 UnitOp2 () ()
164 |
165 | namespace RigCategoryR
166 |   public export
167 |   One : RigCategoryR
168 |   One = MkRigCategoryR One UnitOp2 UnitOp2 () ()
169 |
170 | namespace SymRigCategoryR
171 |   public export
172 |   One : SymRigCategoryR
173 |   One = MkSymRigCategoryR One UnitOp2 UnitOp2 () ()
174 |
175 | namespace DistributiveR
176 |   public export
177 |   One : DistributiveR
178 |   One = MkDistributiveR One UnitOp2 UnitOp2 () ()
179 |
180 |
181 | namespace FunctorR
182 |   public export
183 |   OneTerminal : FunctorR cat One
184 |   OneTerminal = MkFunctorR UnitOp
185 |
186 | namespace MonadR
187 |   public export
188 |   OneM : MonadR One
189 |   OneM = MkMonadR UnitOp
190 |
191 | namespace BifunctorR
192 |   public export
193 |   OneBi : BifunctorR catA catB One
194 |   OneBi = MkBifunctorR UnitOp2
195 |