{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The __discrete__ category on an 'Thin.Indexed' kind @k@ (@'DISCRETE' k@): the numbered inhabitants
-- of @k@ are the objects and the only arrows are identities ('Refl'). The numbering makes the
-- category decidable, and a 'Thin.Finite' kind gives an enumerable one, so that reachability along
-- a graph on a bare set of points can be computed. Its mirror image, the __codiscrete__ category
-- @CODISCRETE k@, has exactly one arrow between any two objects. All (co)limits that exist are
-- trivially computed.
module Proarrow.Category.Instance.Discrete where

import Data.Type.Equality (type (~~))
import Data.Type.Equality qualified as Eq
import Data.Type.Nat (snat)
import Prelude (type (~))

import Proarrow.Category.Enriched (EnrichedProfunctor (..))
import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Enriched.Quantale (Quantale (..), bottomTensor)
import Proarrow.Category.Enriched.Thin qualified as Thin
import Proarrow.Category.Instance.Bool (BOOL (..), If)
import Proarrow.Category.Instance.Cost (COST)
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Category.Topos (HasEpiMonoFactorization (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..), thinCoequalize)
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), UN, dimapDefault, obj)
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..), thinEqualize)
import Proarrow.Limit.Pullback (HasPullbacks (..))

type data DISCRETE k = D k

type Discrete :: CAT (DISCRETE k)
data Discrete a b where
  Refl :: (Ob a) => Discrete a a

-- | The discrete category with only identity arrows on the numbered inhabitants of @k@.
instance (Thin.Indexed k) => CategoryOf (DISCRETE k) where
  type (~>) = Discrete
  type Ob (a :: DISCRETE k) = Thin.KnownIndex a

instance (Thin.Indexed k) => Profunctor (Discrete :: CAT (DISCRETE k)) where
  dimap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k)
       (d :: DISCRETE k).
(c ~> a) -> (b ~> d) -> Discrete a b -> Discrete c d
dimap = (c ~> a) -> (b ~> d) -> Discrete a b -> Discrete c d
Discrete c a -> Discrete b d -> Discrete a b -> Discrete c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: DISCRETE k) (b :: DISCRETE k) r.
((Ob a, Ob b) => r) -> Discrete a b -> r
\\ Discrete a b
Refl = r
(Ob a, Ob b) => r
r
instance (Thin.Indexed k) => Promonad (Discrete :: CAT (DISCRETE k)) where
  id :: forall (a :: DISCRETE k). Ob a => Discrete a a
id = Discrete a a
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl
  Discrete b c
Refl . :: forall (b :: DISCRETE k) (c :: DISCRETE k) (a :: DISCRETE k).
Discrete b c -> Discrete a b -> Discrete a c
. Discrete a b
Refl = Discrete a c
Discrete a a
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl

instance (Thin.Indexed k) => Thin.ThinProfunctor (Discrete :: CAT (DISCRETE k)) where
  type HasArrow Discrete a b = (a ~~ b)
  arr :: forall (a :: DISCRETE k) (b :: DISCRETE k).
(Ob a, Ob b, HasArrow Discrete a b) =>
Discrete a b
arr = Discrete a a
Discrete a b
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl
  withArr :: forall (a :: DISCRETE k) (b :: DISCRETE k) r.
Discrete a b -> ((HasArrow Discrete a b, Ob a, Ob b) => r) -> r
withArr Discrete a b
Refl (HasArrow Discrete a b, Ob a, Ob b) => r
r = r
(HasArrow Discrete a b, Ob a, Ob b) => r
r

-- | An arrow of @'DISCRETE' k@ is an equality. This also witnesses that the category is discrete:
-- it only typechecks because 'Thin.withEq' demands it.
withEq :: forall {k} (a :: DISCRETE k) b r. (Thin.Indexed k) => Discrete a b -> ((a ~~ b) => r) -> r
withEq :: forall {k} (a :: DISCRETE k) (b :: DISCRETE k) r.
Indexed k =>
Discrete a b -> ((a ~~ b) => r) -> r
withEq Discrete a b
p (a ~~ b) => r
r = (a ~> b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r.
Discrete k =>
(a ~> b) -> ((a ~ b) => r) -> r
forall (a :: DISCRETE k) (b :: DISCRETE k) r.
(a ~> b) -> ((a ~ b) => r) -> r
Thin.withEq a ~> b
Discrete a b
p r
(a ~ b) => r
(a ~~ b) => r
r

-- | Two points are equal exactly when their indices are.
instance (Thin.Indexed k) => Thin.DecidableProfunctor (Discrete :: CAT (DISCRETE k)) where
  type Holds (Discrete :: CAT (DISCRETE k)) a b = Thin.Equal a b
  decide :: forall (a :: DISCRETE k) (b :: DISCRETE k).
(Ob a, Ob b) =>
Decision Discrete a b (Holds Discrete a b)
decide @a @b = ((a :~: b) -> Discrete a b)
-> Decision (:~:) a b (NatEq (Index (UN D a)) (Index (UN D b)))
-> Decision Discrete a b (NatEq (Index (UN D a)) (Index (UN D b)))
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
Thin.mapDecision (\a :~: b
Eq.Refl -> Discrete a b
Discrete b b
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl) (forall {k} (a :: k) (b :: k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
forall (a :: DISCRETE k) (b :: DISCRETE k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
Thin.decideEq @a @b)
  toHolds :: forall (a :: DISCRETE k) (b :: DISCRETE k) r.
Discrete a b -> ((Holds Discrete a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds @a Discrete a b
Refl (Holds Discrete a b ~ 'TRU, Ob a, Ob b) => r
r = SNat (Index (UN D a))
-> ((NatEq (Index (UN D a)) (Index (UN D a)) ~ 'TRU) => r) -> r
forall (n :: Nat) r. SNat n -> ((NatEq n n ~ 'TRU) => r) -> r
Thin.withNatEqRefl (forall (n :: Nat). SNatI n => SNat n
snat @(Thin.Index a)) r
(Holds Discrete a b ~ 'TRU, Ob a, Ob b) => r
(NatEq (Index (UN D a)) (Index (UN D a)) ~ 'TRU) => r
r

-- | The hom-object of the discrete category in a quantale: the unit on the diagonal, the bottom off
-- it. Points are at distance @0@ from themselves and infinitely far from each other: the discrete
-- category is a (discrete) Lawvere metric space, the base for shortest paths on a bare set of points.
type Delta :: forall (v :: Kind) -> BOOL -> v
type Delta v c = If c (Unit :: v) InitialObject

-- | The action of the discrete base on a matrix over the points: on the diagonal the 'Delta' is the
-- unit and the action is the unitor, off it the 'Delta' is the bottom and the action absorbs. The
-- argument says how the matrix is reindexed on the diagonal.
deltaAct
  :: forall {k} {v} (x :: k) y (w :: v) w'
   . (Quantale v, Thin.KnownIndex x, Thin.KnownIndex y, Ob w, Ob w')
  => ((x ~ y) => w Eq.:~: w') -> (Delta v (Thin.Equal x y) ** w) ~> w'
deltaAct :: forall {k} {v} (x :: k) (y :: k) (w :: v) (w' :: v).
(Quantale v, KnownIndex x, KnownIndex y, Ob w, Ob w') =>
((x ~ y) => w :~: w') -> (Delta v (Equal x y) ** w) ~> w'
deltaAct (x ~ y) => w :~: w'
eq = case forall (a :: k) (b :: k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
forall {k} (a :: k) (b :: k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
Thin.decideEq @x @y of
  Thin.Yes x :~: y
Eq.Refl -> case w :~: w'
(x ~ y) => w :~: w'
eq of w :~: w'
Eq.Refl -> forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @v @w
  Decision (:~:) x y (Equal x y)
Thin.No -> forall (x :: v) (y :: v).
(Quantale v, Ob x, Ob y) =>
(InitialObject ** x) ~> y
forall {v} (x :: v) (y :: v).
(Quantale v, Ob x, Ob y) =>
(InitialObject ** x) ~> y
bottomTensor @w @w'

instance (Thin.Indexed k) => EnrichedProfunctor COST (Discrete :: CAT (DISCRETE k)) where
  type ProObj COST (Discrete :: CAT (DISCRETE k)) a b = Delta COST (Thin.Equal a b)
  withProObj :: forall (a :: DISCRETE k) (b :: DISCRETE k) r.
(Ob a, Ob b) =>
(Ob (ProObj COST Discrete a b) => r) -> r
withProObj @a @b Ob (ProObj COST Discrete a b) => r
r = case forall {k} (a :: k) (b :: k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
forall (a :: DISCRETE k) (b :: DISCRETE k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
Thin.decideEq @a @b of
    Thin.Yes a :~: b
Eq.Refl -> r
Ob (ProObj COST Discrete a b) => r
r
    Decision (:~:) a b (Equal a b)
Thin.No -> r
Ob (ProObj COST Discrete a b) => r
r
  underlying :: forall (a :: DISCRETE k) (b :: DISCRETE k).
Discrete a b -> Unit ~> ProObj COST Discrete a b
underlying @a Discrete a b
Refl = SNat (Index (UN D a))
-> ((NatEq (Index (UN D a)) (Index (UN D a)) ~ 'TRU) =>
    GTE (C 0) (If (NatEq (Index (UN D a)) (Index (UN D a))) (C 0) INF))
-> GTE
     (C 0) (If (NatEq (Index (UN D a)) (Index (UN D a))) (C 0) INF)
forall (n :: Nat) r. SNat n -> ((NatEq n n ~ 'TRU) => r) -> r
Thin.withNatEqRefl (forall (n :: Nat). SNatI n => SNat n
snat @(Thin.Index a)) (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COST). (CategoryOf COST, Ob a) => Obj a
obj @(Unit :: COST))
  enriched :: forall (a :: DISCRETE k) (b :: DISCRETE k).
(Ob a, Ob b) =>
(Unit ~> ProObj COST Discrete a b) -> Discrete a b
enriched @a @b Unit ~> ProObj COST Discrete a b
f = case forall {k} (a :: k) (b :: k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
forall (a :: DISCRETE k) (b :: DISCRETE k).
(KnownIndex a, KnownIndex b) =>
Decision (:~:) a b (Equal a b)
Thin.decideEq @a @b of
    Thin.Yes a :~: b
Eq.Refl -> Discrete a a
Discrete a b
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl
    Decision (:~:) a b (Equal a b)
Thin.No -> forall v r. Quantale v => (Unit ~> InitialObject) -> r
unitIsNotBottom @COST Unit ~> InitialObject
Unit ~> ProObj COST Discrete a b
f
  rmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k).
(Ob a, Ob b, Ob c) =>
(HomObj COST b c ** ProObj COST Discrete a b)
~> ProObj COST Discrete a c
rmap @a @b @c =
    forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: DISCRETE k +-> DISCRETE k) (a :: DISCRETE k)
       (b :: DISCRETE k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @COST @(Discrete :: CAT (DISCRETE k)) @a @b
      ( forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: DISCRETE k +-> DISCRETE k) (a :: DISCRETE k)
       (b :: DISCRETE k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @COST @(Discrete :: CAT (DISCRETE k)) @a @c
          (forall {k} {v} (x :: k) (y :: k) (w :: v) (w' :: v).
(Quantale v, KnownIndex x, KnownIndex y, Ob w, Ob w') =>
((x ~ y) => w :~: w') -> (Delta v (Equal x y) ** w) ~> w'
forall (x :: DISCRETE k) (y :: DISCRETE k) (w :: COST)
       (w' :: COST).
(Quantale COST, KnownIndex x, KnownIndex y, Ob w, Ob w') =>
((x ~ y) => w :~: w') -> (Delta COST (Equal x y) ** w) ~> w'
deltaAct @b @c @(Delta COST (Thin.Equal a b)) @(Delta COST (Thin.Equal a c)) If (NatEq (Index (UN D a)) (Index (UN D c))) (C 0) INF
:~: If (NatEq (Index (UN D a)) (Index (UN D c))) (C 0) INF
Delta COST (Equal a b) :~: Delta COST (Equal a c)
(b ~ c) => Delta COST (Equal a b) :~: Delta COST (Equal a c)
forall {k} (a :: k). a :~: a
Eq.Refl)
      )
  lmap :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k).
(Ob a, Ob b, Ob c) =>
(HomObj COST c a ** ProObj COST Discrete a b)
~> ProObj COST Discrete c b
lmap @a @b @c =
    forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: DISCRETE k +-> DISCRETE k) (a :: DISCRETE k)
       (b :: DISCRETE k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @COST @(Discrete :: CAT (DISCRETE k)) @a @b
      ( forall {j} {k} v (p :: j +-> k) (a :: k) (b :: j) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
forall v (p :: DISCRETE k +-> DISCRETE k) (a :: DISCRETE k)
       (b :: DISCRETE k) r.
(EnrichedProfunctor v p, Ob a, Ob b) =>
(Ob (ProObj v p a b) => r) -> r
withProObj @COST @(Discrete :: CAT (DISCRETE k)) @c @b
          (forall {k} {v} (x :: k) (y :: k) (w :: v) (w' :: v).
(Quantale v, KnownIndex x, KnownIndex y, Ob w, Ob w') =>
((x ~ y) => w :~: w') -> (Delta v (Equal x y) ** w) ~> w'
forall (x :: DISCRETE k) (y :: DISCRETE k) (w :: COST)
       (w' :: COST).
(Quantale COST, KnownIndex x, KnownIndex y, Ob w, Ob w') =>
((x ~ y) => w :~: w') -> (Delta COST (Equal x y) ** w) ~> w'
deltaAct @c @a @(Delta COST (Thin.Equal a b)) @(Delta COST (Thin.Equal c b)) If (NatEq (Index (UN D a)) (Index (UN D b))) (C 0) INF
:~: If (NatEq (Index (UN D a)) (Index (UN D b))) (C 0) INF
Delta COST (Equal a b) :~: Delta COST (Equal c b)
(c ~ a) => Delta COST (Equal a b) :~: Delta COST (Equal c b)
forall {k} (a :: k). a :~: a
Eq.Refl)
      )

instance (Thin.Indexed k) => Thin.Indexed (DISCRETE k) where
  type Index (a :: DISCRETE k) = Thin.Index (UN D a)
  type At (DISCRETE k) i = Thin.FmapWrap D (Thin.At k i)

instance (Thin.Finite k) => Thin.Finite (DISCRETE k) where
  type Objects (DISCRETE k) = Thin.MapWrap D (Thin.Objects k)
  finite :: IndexedList (Objects (DISCRETE k))
finite = forall {j} {k} (w :: j -> k).
(Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects j))
forall (w :: k -> DISCRETE k).
(Finite k, forall (a :: k). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects k))
Thin.wrapFinite @D
  withAtLookup :: forall (i :: Nat) r.
SNat i
-> ((Lookup (Objects (DISCRETE k)) i ~ At (DISCRETE k) i) => r)
-> r
withAtLookup = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: k -> DISCRETE k) (i :: Nat) r.
Finite k =>
SNat i
-> ((Lookup (MapWrap w (Objects k)) i ~ FmapWrap w (At k i)) => r)
-> r
Thin.withWrapAtLookup @D

instance (Thin.Finite k) => Thin.Enumerable (DISCRETE k) where
  withIndex :: forall (a :: DISCRETE k) r. Ob a => (KnownIndex a => r) -> r
withIndex KnownIndex a => r
r = r
KnownIndex a => r
r
  withOb :: forall (a :: DISCRETE k) r. KnownIndex a => (Ob a => r) -> r
withOb Ob a => r
r = r
Ob a => r
r

instance (Thin.Indexed k) => DaggerProfunctor (Discrete :: CAT (DISCRETE k)) where
  dagger :: forall (a :: DISCRETE k) (b :: DISCRETE k).
Discrete a b -> Discrete b a
dagger Discrete a b
Refl = Discrete b a
Discrete b b
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl

instance (Thin.Indexed k) => HasEqualizers (DISCRETE k) where
  equalize :: forall (a :: DISCRETE k) (b :: DISCRETE k) r.
(a ~> b)
-> (a ~> b) -> (forall (e :: DISCRETE k). (e ~> a) -> r) -> r
equalize = (a ~> b)
-> (a ~> b) -> (forall (e :: DISCRETE k). (e ~> a) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
thinEqualize
  factorEqualizer :: forall (e :: DISCRETE k) (x :: DISCRETE k) (e' :: DISCRETE k).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer e ~> x
Discrete e x
Refl e' ~> x
Discrete e' e
Refl = e' ~> e
Discrete e' e'
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl

instance (Thin.Indexed k) => HasCoequalizers (DISCRETE k) where
  coequalize :: forall (a :: DISCRETE k) (b :: DISCRETE k) r.
(a ~> b)
-> (a ~> b) -> (forall (c :: DISCRETE k). (b ~> c) -> r) -> r
coequalize = (a ~> b)
-> (a ~> b) -> (forall (c :: DISCRETE k). (b ~> c) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
thinCoequalize
  factorCoequalizer :: forall (c :: DISCRETE k) (x :: DISCRETE k) (c' :: DISCRETE k).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer x ~> c
Discrete x c
Refl x ~> c'
Discrete x c'
Refl = c ~> c'
Discrete x x
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl

instance (Thin.Indexed k) => HasPullbacks (DISCRETE k) where
  pullback :: forall (o :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: DISCRETE k). (p ~> a) -> (p ~> b) -> r)
-> r
pullback a ~> o
Discrete a o
Refl b ~> o
Discrete b a
Refl forall (p :: DISCRETE k). (p ~> a) -> (p ~> b) -> r
k = (b ~> a) -> (b ~> b) -> r
forall (p :: DISCRETE k). (p ~> a) -> (p ~> b) -> r
k b ~> a
Discrete b b
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl b ~> b
Discrete b b
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl
  factorPullback :: forall (a :: DISCRETE k) (b :: DISCRETE k) (p :: DISCRETE k)
       (q :: DISCRETE k).
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullback p ~> a
Discrete p a
Refl p ~> b
Discrete p b
Refl q ~> a
Discrete q p
Refl q ~> b
Discrete q q
Refl = q ~> p
Discrete q q
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl

instance (Thin.Indexed k) => HasPushouts (DISCRETE k) where
  pushout :: forall (o :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: DISCRETE k). (a ~> p) -> (b ~> p) -> r)
-> r
pushout o ~> a
Discrete o a
Refl o ~> b
Discrete o b
Refl forall (p :: DISCRETE k). (a ~> p) -> (b ~> p) -> r
k = (a ~> o) -> (b ~> o) -> r
forall (p :: DISCRETE k). (a ~> p) -> (b ~> p) -> r
k a ~> o
Discrete o o
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl b ~> o
Discrete o o
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl
  factorPushout :: forall (a :: DISCRETE k) (b :: DISCRETE k) (p :: DISCRETE k)
       (q :: DISCRETE k).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout a ~> p
Discrete a p
Refl b ~> p
Discrete b a
Refl a ~> q
Discrete b q
Refl b ~> q
Discrete b b
Refl = p ~> q
Discrete b b
forall {k} (a :: DISCRETE k). Ob a => Discrete a a
Refl

instance (Thin.Indexed k) => HasEpiMonoFactorization (DISCRETE k)

type data CODISCRETE k = CD k

type Codiscrete :: CAT (CODISCRETE k)
data Codiscrete a b where
  Arr :: (Ob a, Ob b) => Codiscrete a b

-- | The codiscrete category has exactly one arrow between any two objects, the numbered inhabitants
-- of @k@. The numbering makes it enumerable, so its closure can be computed.
instance (Thin.Indexed k) => CategoryOf (CODISCRETE k) where
  type (~>) = Codiscrete
  type Ob (a :: CODISCRETE k) = Thin.KnownIndex a

instance (Thin.Indexed k) => Profunctor (Codiscrete :: CAT (CODISCRETE k)) where
  dimap :: forall (c :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k)
       (d :: CODISCRETE k).
(c ~> a) -> (b ~> d) -> Codiscrete a b -> Codiscrete c d
dimap = (c ~> a) -> (b ~> d) -> Codiscrete a b -> Codiscrete c d
Codiscrete c a
-> Codiscrete b d -> Codiscrete a b -> Codiscrete c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r.
((Ob a, Ob b) => r) -> Codiscrete a b -> r
\\ Codiscrete a b
Arr = r
(Ob a, Ob b) => r
r
instance (Thin.Indexed k) => Promonad (Codiscrete :: CAT (CODISCRETE k)) where
  id :: forall (a :: CODISCRETE k). Ob a => Codiscrete a a
id = Codiscrete a a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  Codiscrete b c
Arr . :: forall (b :: CODISCRETE k) (c :: CODISCRETE k) (a :: CODISCRETE k).
Codiscrete b c -> Codiscrete a b -> Codiscrete a c
. Codiscrete a b
Arr = Codiscrete a c
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr

instance (Thin.Indexed k) => Thin.ThinProfunctor (Codiscrete :: CAT (CODISCRETE k))

instance (Thin.Indexed k) => Thin.DecidableProfunctor (Codiscrete :: CAT (CODISCRETE k)) where
  type Holds Codiscrete a b = TRU
  decide :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Decision Codiscrete a b (Holds Codiscrete a b)
decide = Codiscrete a b -> Decision Codiscrete a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Thin.Yes Codiscrete a b
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  toHolds :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r.
Codiscrete a b
-> ((Holds Codiscrete a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds Codiscrete a b
Arr (Holds Codiscrete a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds Codiscrete a b ~ 'TRU, Ob a, Ob b) => r
r

-- | Witnesses that @'CODISCRETE' k@ really is codiscrete: this only typechecks if 'Codiscrete' is a
-- 'Thin.CodiscreteProfunctor', so the definition is the check.
anyArr :: forall {k} (a :: CODISCRETE k) b. (Thin.Indexed k, Ob a, Ob b) => Codiscrete a b
anyArr :: forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Indexed k, Ob a, Ob b) =>
Codiscrete a b
anyArr = Codiscrete a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Thin.anyArr

instance (Thin.Indexed k) => Thin.Indexed (CODISCRETE k) where
  type Index (a :: CODISCRETE k) = Thin.Index (UN CD a)
  type At (CODISCRETE k) i = Thin.FmapWrap CD (Thin.At k i)

instance (Thin.Finite k) => Thin.Finite (CODISCRETE k) where
  type Objects (CODISCRETE k) = Thin.MapWrap CD (Thin.Objects k)
  finite :: IndexedList (Objects (CODISCRETE k))
finite = forall {j} {k} (w :: j -> k).
(Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects j))
forall (w :: k -> CODISCRETE k).
(Finite k, forall (a :: k). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects k))
Thin.wrapFinite @CD
  withAtLookup :: forall (i :: Nat) r.
SNat i
-> ((Lookup (Objects (CODISCRETE k)) i ~ At (CODISCRETE k) i) => r)
-> r
withAtLookup = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: k -> CODISCRETE k) (i :: Nat) r.
Finite k =>
SNat i
-> ((Lookup (MapWrap w (Objects k)) i ~ FmapWrap w (At k i)) => r)
-> r
Thin.withWrapAtLookup @CD

instance (Thin.Finite k) => Thin.Enumerable (CODISCRETE k) where
  withIndex :: forall (a :: CODISCRETE k) r. Ob a => (KnownIndex a => r) -> r
withIndex KnownIndex a => r
r = r
KnownIndex a => r
r
  withOb :: forall (a :: CODISCRETE k) r. KnownIndex a => (Ob a => r) -> r
withOb Ob a => r
r = r
Ob a => r
r

instance (Thin.Indexed k) => DaggerProfunctor (Codiscrete :: CAT (CODISCRETE k)) where
  dagger :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
Codiscrete a b -> Codiscrete b a
dagger Codiscrete a b
Arr = Codiscrete b a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr

instance (Thin.Indexed k) => HasEqualizers (CODISCRETE k) where
  equalize :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r.
(a ~> b)
-> (a ~> b) -> (forall (e :: CODISCRETE k). (e ~> a) -> r) -> r
equalize = (a ~> b)
-> (a ~> b) -> (forall (e :: CODISCRETE k). (e ~> a) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (e :: k). (e ~> a) -> r) -> r
thinEqualize
  factorEqualizer :: forall (e :: CODISCRETE k) (x :: CODISCRETE k)
       (e' :: CODISCRETE k).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer e ~> x
Codiscrete e x
Arr e' ~> x
Codiscrete e' x
Arr = e' ~> e
Codiscrete e' e
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr

instance (Thin.Indexed k) => HasCoequalizers (CODISCRETE k) where
  coequalize :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r.
(a ~> b)
-> (a ~> b) -> (forall (c :: CODISCRETE k). (b ~> c) -> r) -> r
coequalize = (a ~> b)
-> (a ~> b) -> (forall (c :: CODISCRETE k). (b ~> c) -> r) -> r
forall {k} (a :: k) (b :: k) r.
Thin k =>
(a ~> b) -> (a ~> b) -> (forall (c :: k). (b ~> c) -> r) -> r
thinCoequalize
  factorCoequalizer :: forall (c :: CODISCRETE k) (x :: CODISCRETE k)
       (c' :: CODISCRETE k).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer x ~> c
Codiscrete x c
Arr x ~> c'
Codiscrete x c'
Arr = c ~> c'
Codiscrete c c'
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr

instance (Thin.Indexed k) => HasPullbacks (CODISCRETE k) where
  pullback :: forall (o :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k)
       r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: CODISCRETE k). (p ~> a) -> (p ~> b) -> r)
-> r
pullback @o a ~> o
Codiscrete a o
Arr b ~> o
Codiscrete b o
Arr forall (p :: CODISCRETE k). (p ~> a) -> (p ~> b) -> r
k = forall (p :: CODISCRETE k). (p ~> a) -> (p ~> b) -> r
k @o o ~> a
Codiscrete o a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr o ~> b
Codiscrete o b
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  factorPullback :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) (p :: CODISCRETE k)
       (q :: CODISCRETE k).
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullback p ~> a
Codiscrete p a
Arr p ~> b
Codiscrete p b
Arr q ~> a
Codiscrete q a
Arr q ~> b
Codiscrete q b
Arr = q ~> p
Codiscrete q p
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr

instance (Thin.Indexed k) => HasPushouts (CODISCRETE k) where
  pushout :: forall (o :: CODISCRETE k) (a :: CODISCRETE k) (b :: CODISCRETE k)
       r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: CODISCRETE k). (a ~> p) -> (b ~> p) -> r)
-> r
pushout @o o ~> a
Codiscrete o a
Arr o ~> b
Codiscrete o b
Arr forall (p :: CODISCRETE k). (a ~> p) -> (b ~> p) -> r
k = forall (p :: CODISCRETE k). (a ~> p) -> (b ~> p) -> r
k @o a ~> o
Codiscrete a o
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr b ~> o
Codiscrete b o
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  factorPushout :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) (p :: CODISCRETE k)
       (q :: CODISCRETE k).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout a ~> p
Codiscrete a p
Arr b ~> p
Codiscrete b p
Arr a ~> q
Codiscrete a q
Arr b ~> q
Codiscrete b q
Arr = p ~> q
Codiscrete p q
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr

instance (Thin.Indexed k) => HasEpiMonoFactorization (CODISCRETE k)

-- | Any object works as the product of any two objects here, since every hom-set is a singleton.
instance (Thin.Indexed k) => HasBinaryProducts (CODISCRETE k) where
  type a && b = a
  withObProd :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
(a && b) ~> a
fst = (a && b) ~> a
Codiscrete a a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  snd :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
(a && b) ~> b
snd = (a && b) ~> b
Codiscrete a b
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  a ~> x
Codiscrete a x
Arr &&& :: forall (a :: CODISCRETE k) (x :: CODISCRETE k) (y :: CODISCRETE k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
Codiscrete a y
Arr = a ~> (x && y)
Codiscrete a x
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr

-- | Dual to the 'HasBinaryProducts' instance above.
instance (Thin.Indexed k) => HasBinaryCoproducts (CODISCRETE k) where
  type a || b = a
  withObCoprod :: forall (a :: CODISCRETE k) (b :: CODISCRETE k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
a ~> (a || b)
lft = a ~> (a || b)
Codiscrete a a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  rgt :: forall (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
b ~> (a || b)
rgt = b ~> (a || b)
Codiscrete b a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr
  x ~> a
Codiscrete x a
Arr ||| :: forall (x :: CODISCRETE k) (a :: CODISCRETE k) (y :: CODISCRETE k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
Codiscrete y a
Arr = (x || y) ~> a
Codiscrete x a
forall {k} (a :: CODISCRETE k) (b :: CODISCRETE k).
(Ob a, Ob b) =>
Codiscrete a b
Arr