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 {a} = void a
 52 |   assoc' {a} = void a
 53 |   unitl {a} = void a
 54 |   unitl' {a} = void a
 55 |   unitr {a} = void a
 56 |   unitr' {a} = void a
 57 |
 58 | public export
 59 | {ten,i : _} -> Braided Zero ten i where
 60 |   braid {a} = void a
 61 |   braid' {a} = void a
 62 |
 63 | public export
 64 | {ten,i : _} -> Cartesian Zero ten i where
 65 |   projl {a} = void a
 66 |   projr {a} = void a
 67 |   prod {a} = void a
 68 |   split {a} = void a
 69 |   elim {a} = void a
 70 |
 71 | public export
 72 | {ten,i : _} -> Cocartesian Zero ten i where
 73 |   injl {a} = void a
 74 |   injr {a} = void a
 75 |   coprod {a} = void a
 76 |   merge {a} = void a
 77 |   intro {a} = void a
 78 |
 79 | public export
 80 | {ten,hom,i : _} -> Closed Zero ten hom i where
 81 |   curry {a} = void a
 82 |   uncurry {a} = void a
 83 |
 84 | public export
 85 | {ten,i : _} -> Traced Zero ten i where
 86 |   tracel {a} = void a
 87 |   tracer {a} = void a
 88 |
 89 | public export
 90 | {add,mul,z,i : _} -> Bimonoidal Zero add mul z i where
 91 |   distribl {a} = void a
 92 |   distribl' {a} = void a
 93 |   distribr {a} = void a
 94 |   distribr' {a} = void a
 95 |   absorbl {a} = void a
 96 |   absorbl' {a} = void a
 97 |   absorbr {a} = void a
 98 |   absorbr' {a} = void a
 99 |
100 |
101 | ------------------------------------------------------------
102 | -- Record Style
103 | ------------------------------------------------------------
104 |
105 | namespace SemigroupoidR
106 |   public export
107 |   Zero : SemigroupoidR
108 |   Zero = MkSemigroupoidR Zero
109 |
110 | namespace CategoryR
111 |   public export
112 |   Zero : CategoryR
113 |   Zero = MkCategoryR Zero
114 |
115 | namespace FunctorR
116 |   public export
117 |   ZeroInitial : FunctorR Zero cat
118 |   ZeroInitial = MkFunctorR absurd
119 |