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