0 | ||| This module defines `Zero`, the zero category, which contains no
  1 | ||| objects and no morphisms.
  2 | module Control.Category.Instances.Zero
  3 |
  4 | import Control.Category
  5 | import Control.Category.Records
  6 |
  7 | %default total
  8 |
  9 | ||| The zero category, or initial category. This category contains
 10 | ||| no objects and no morphisms.
 11 | public export
 12 | data Zero : (a,b : Void) -> Type where
 13 |   
 14 | public export
 15 | Uninhabited (Zero a b) where
 16 |   uninhabited _ impossible
 17 |
 18 |
 19 | ------------------------------------------------------------
 20 | -- Interface Style
 21 | ------------------------------------------------------------
 22 |
 23 | public export
 24 | Category Zero where
 25 |   id {a} = void a
 26 |   (.) {a} = void a
 27 |
 28 | %hint
 29 | SemigroupoidZero : Semigroupoid Zero
 30 | SemigroupoidZero = FromCategory
 31 |
 32 | public export
 33 | Either (cat ~=~ Zero) (cat' ~=~ Zero) => CatFunctor cat cat' f where
 34 |   map @{Left Refl} {a} = void a
 35 |   map @{Right Refl} {a} = void (f a)
 36 |
 37 | public export
 38 | Either (catA ~=~ Zero) (Either (catB ~=~ Zero) (cat' ~=~ Zero)) =>
 39 |     CatBifunctor catA catB cat' f where
 40 |   bimap @{Left Refl} {a} = void a
 41 |   bimap @{Right (Left Refl)} {a'} = void a'
 42 |   bimap @{Right (Right Refl)} {a,a'} = void (f a a')
 43 |
 44 | public export
 45 | CatMonad Zero m where
 46 |   join {a} = void a
 47 |   unit {a} = void a
 48 |
 49 | public export
 50 | {ten,i : _} -> Monoidal Zero ten i where
 51 |   assoc = void i
 52 |   assoc' = void i
 53 |   unitl = void i
 54 |   unitl' = void i
 55 |   unitr = void i
 56 |   unitr' = void i
 57 |
 58 | public export
 59 | {ten,i : _} -> Braided Zero ten i where
 60 |   braid = void i
 61 |   braid' = void i
 62 |
 63 | public export
 64 | {ten,i : _} -> MonSymmetric Zero ten i where
 65 |   permute = void i
 66 |
 67 | public export
 68 | {ten,i : _} -> Cartesian Zero ten i where
 69 |   projl = void i
 70 |   projr = void i
 71 |   prod = void i
 72 |   split = void i
 73 |   elim = void i
 74 |
 75 | public export
 76 | {ten,i : _} -> Cocartesian Zero ten i where
 77 |   injl = void i
 78 |   injr = void i
 79 |   coprod = void i
 80 |   merge = void i
 81 |   intro = void i
 82 |
 83 | public export
 84 | {ten,hom,i : _} -> Closed Zero ten hom i where
 85 |   curry = void i
 86 |   uncurry = void i
 87 |
 88 | public export
 89 | {ten,i : _} -> Traced Zero ten i where
 90 |   tracel = void i
 91 |   tracer = void i
 92 |
 93 | public export
 94 | {add,mul,z,i : _} -> Bimonoidal Zero add mul z i where
 95 |   distribl = void i
 96 |   distribl' = void i
 97 |   distribr = void i
 98 |   distribr' = void i
 99 |   absorbl = void i
100 |   absorbl' = void i
101 |   absorbr = void i
102 |   absorbr' = void i
103 |
104 |
105 | ------------------------------------------------------------
106 | -- Record Style
107 | ------------------------------------------------------------
108 |
109 | namespace SemigroupoidR
110 |   public export
111 |   Zero : SemigroupoidR
112 |   Zero = MkSemigroupoidR Zero
113 |
114 | namespace CategoryR
115 |   public export
116 |   Zero : CategoryR
117 |   Zero = MkCategoryR Zero
118 |
119 | namespace FunctorR
120 |   public export
121 |   ZeroInitial : FunctorR Zero cat
122 |   ZeroInitial = MkFunctorR absurd
123 |