{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}

-- | The Lawvere __cost__ category: extended natural numbers (@'C' n@ or 'INF') as a thin category
-- with an arrow @a '~>' b@ exactly when @a >= b@ ('GTE'). Addition of costs provides a symmetric
-- monoidal structure with @'C' 0@ as unit (and terminal object; 'INF' is initial), so categories
-- enriched in @COST@ are generalized (Lawvere) metric spaces.
module Proarrow.Category.Instance.Cost where

import Data.Proxy (Proxy (..))
import Data.Type.Ord (OrderingI (..), type Max, type Min, type (<=), type (<=?))
import GHC.TypeNats (KnownNat, Nat, cmpNat, natVal, withKnownNat, withSomeSNat, type SNat, type (+))
import Unsafe.Coerce (unsafeCoerce)
import Prelude (Num ((+)), error, ($))

import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), Decision (..), ThinProfunctor (..))
import Proarrow.Category.Instance.Bool (BOOL (..), FromBool)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Category.Topos (HasEpiMonoFactorization (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..), factorPushoutDefault, thinCoequalize)
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts (..), thinPushout)
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, obj, (//))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..), factorPullbackDefault, thinEqualize)
import Proarrow.Limit.Pullback (HasPullbacks (..), thinPullback)
import Proarrow.Limit.Terminal (HasTerminalObject (..))

type data COST = C Nat | INF

data SCost n where
  SC :: (KnownNat n) => SCost (C n)
  SINF :: SCost INF

type GTE :: CAT COST
data GTE a b where
  Inf :: (Ob a) => GTE INF a
  GTE :: (KnownNat a, KnownNat b, b <= a) => GTE (C a) (C b)

lteTrans :: forall (a :: Nat) b c r. (a <= b, b <= c, KnownNat a, KnownNat c) => ((a <= c) => r) -> r
lteTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat) r.
(a <= b, b <= c, KnownNat a, KnownNat c) =>
((a <= c) => r) -> r
lteTrans (a <= c) => r
r = case Proxy a -> Proxy c -> OrderingI a c
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) (Proxy c
forall {k} (t :: k). Proxy t
Proxy :: Proxy c) of
  OrderingI a c
LTI -> r
(a <= c) => r
r
  OrderingI a c
EQI -> r
(a <= c) => r
r
  OrderingI a c
GTI -> [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"lteTrans: broken transitivity"

plusMonotone
  :: forall (a :: Nat) b c d r. (a <= b, c <= d, KnownNat (a + c), KnownNat (b + d)) => (((a + c) <= (b + d)) => r) -> r
plusMonotone :: forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat) r.
(a <= b, c <= d, KnownNat (a + c), KnownNat (b + d)) =>
(((a + c) <= (b + d)) => r) -> r
plusMonotone ((a + c) <= (b + d)) => r
r = case Proxy (a + c) -> Proxy (b + d) -> OrderingI (a + c) (b + d)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy (a + c)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (a + c)) (Proxy (b + d)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (b + d)) of
  OrderingI (a + c) (b + d)
LTI -> r
((a + c) <= (b + d)) => r
r
  OrderingI (a + c) (b + d)
EQI -> r
((a + c) <= (b + d)) => r
r
  OrderingI (a + c) (b + d)
GTI -> [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"plusMonotone: broken monotonicity"

withPlusIsNat :: forall a b r. (KnownNat a, KnownNat b) => ((KnownNat (a + b)) => r) -> r
withPlusIsNat :: forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat = SNat (a + b) -> (KnownNat (a + b) => r) -> r
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat (a + b)
ab
  where
    ab :: SNat (a + b)
    ab :: SNat (a + b)
ab = Nat -> (forall (n :: Nat). SNat n -> SNat (a + b)) -> SNat (a + b)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat (Proxy a -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Proxy b -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b)) SNat n -> SNat (a + b)
forall (n :: Nat). SNat n -> SNat (a + b)
forall a b. a -> b
unsafeCoerce

class IsCost (a :: COST) where
  sing :: SCost a
instance (KnownNat n) => IsCost (C n) where
  sing :: SCost (C n)
sing = SCost (C n)
forall (n :: Nat). KnownNat n => SCost (C n)
SC
instance IsCost INF where
  sing :: SCost INF
sing = SCost INF
SINF

instance Profunctor GTE where
  dimap :: forall (c :: COST) (a :: COST) (b :: COST) (d :: COST).
(c ~> a) -> (b ~> d) -> GTE a b -> GTE c d
dimap = (c ~> a) -> (b ~> d) -> GTE a b -> GTE c d
GTE c a -> GTE b d -> GTE a b -> GTE 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 :: COST) (b :: COST) r.
((Ob a, Ob b) => r) -> GTE a b -> r
\\ GTE a b
Inf = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ GTE a b
GTE = r
(Ob a, Ob b) => r
r
instance Promonad GTE where
  id :: forall (a :: COST). Ob a => GTE a a
id @a = case forall (a :: COST). IsCost a => SCost a
sing @a of
    SCost a
SINF -> GTE a a
GTE INF a
forall (a :: COST). Ob a => GTE INF a
Inf
    SCost a
SC -> GTE a a
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  GTE b c
f . :: forall (b :: COST) (c :: COST) (a :: COST).
GTE b c -> GTE a b -> GTE a c
. GTE a b
Inf = GTE a c
GTE INF c
(Ob b, Ob c) => GTE a c
forall (a :: COST). Ob a => GTE INF a
Inf ((Ob b, Ob c) => GTE a c) -> GTE b c -> GTE a c
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COST) (b :: COST) r.
((Ob a, Ob b) => r) -> GTE a b -> r
\\ GTE b c
f
  GTE @b @c . GTE @a = forall (a :: Nat) (b :: Nat) (c :: Nat) r.
(a <= b, b <= c, KnownNat a, KnownNat c) =>
((a <= c) => r) -> r
lteTrans @c @b @a GTE a c
GTE (C a) (C b)
(b <= a) => GTE a c
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE

-- | Cost category. Categories enriched in the cost category are lawvere metric spaces.
instance CategoryOf COST where
  type (~>) = GTE
  type Ob a = (IsCost a)

instance ThinProfunctor GTE

-- | Decided by comparing the naturals; @INF@ is below everything.
instance DecidableProfunctor GTE where
  type Holds GTE INF b = TRU
  type Holds GTE (C a) INF = FLS
  type Holds GTE (C a) (C b) = FromBool (b <=? a)
  decide :: forall (a :: COST) (b :: COST).
(Ob a, Ob b) =>
Decision GTE a b (Holds GTE a b)
decide @a @b = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> GTE a b -> Decision GTE a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes GTE a b
GTE INF b
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
SC, SCost b
SINF) -> Decision GTE a b 'FLS
Decision GTE a b (Holds GTE a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
    (SC @x, SC @y) -> case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy y) (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy x) of
      OrderingI n n
LTI -> GTE a b -> Decision GTE a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes GTE a b
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI n n
EQI -> GTE a b -> Decision GTE a b 'TRU
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Decision p a b 'TRU
Yes GTE a b
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI n n
GTI -> Decision GTE a b 'FLS
Decision GTE a b (Holds GTE a b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Decision p a b 'FLS
No
  toHolds :: forall (a :: COST) (b :: COST) r.
GTE a b -> ((Holds GTE a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds GTE a b
Inf (Holds GTE a b ~ 'TRU, Ob a, Ob b) => r
r = r
(Holds GTE a b ~ 'TRU, Ob a, Ob b) => r
r
  toHolds (GTE @x @y) (Holds GTE a b ~ 'TRU, Ob a, Ob b) => r
r = case Proxy b -> Proxy a -> OrderingI b a
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy y) (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy x) of
    OrderingI b a
LTI -> r
(Holds GTE a b ~ 'TRU, Ob a, Ob b) => r
r
    OrderingI b a
EQI -> r
(Holds GTE a b ~ 'TRU, Ob a, Ob b) => r
r

instance HasTerminalObject COST where
  type TerminalObject = C 0
  terminate :: forall (a :: COST). Ob a => a ~> TerminalObject
terminate @a = case forall (a :: COST). IsCost a => SCost a
sing @a of
    SCost a
SINF -> a ~> TerminalObject
GTE INF (C 0)
forall (a :: COST). Ob a => GTE INF a
Inf
    SC @b -> case Proxy 0 -> Proxy n -> OrderingI 0 n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy 0
forall {k} (t :: k). Proxy t
Proxy :: Proxy 0) (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b) of
      OrderingI 0 n
LTI -> a ~> TerminalObject
GTE (C n) (C 0)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI 0 n
EQI -> a ~> TerminalObject
GTE (C 0) (C 0)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI 0 n
GTI -> [Char] -> GTE (C n) (C 0)
forall a. HasCallStack => [Char] -> a
error [Char]
"terminate: found a Nat smaller than 0"

instance HasInitialObject COST where
  type InitialObject = INF
  initiate :: forall (a :: COST). Ob a => InitialObject ~> a
initiate = InitialObject ~> a
GTE INF a
forall (a :: COST). Ob a => GTE INF a
Inf

instance HasBinaryProducts COST where
  type INF && b = INF
  type a && INF = INF
  type C a && C b = C (Max a b)
  withObProd :: forall (a :: COST) (b :: COST) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> r
Ob (a && b) => r
r
    (SCost a
_, SCost b
SINF) -> r
Ob (a && b) => r
r
    (SC @a', SC @b') -> case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b') of
      OrderingI n n
LTI -> r
Ob (a && b) => r
r
      OrderingI n n
EQI -> r
Ob (a && b) => r
r
      OrderingI n n
GTI -> r
Ob (a && b) => r
r
  fst :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => (a && b) ~> a
fst @a @b = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> (a && b) ~> a
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
SINF) -> (a && b) ~> a
GTE INF a
forall (a :: COST). Ob a => GTE INF a
Inf
    (SC @a', SC @b') -> case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b') of
      OrderingI n n
LTI -> (a && b) ~> a
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI n n
EQI -> (a && b) ~> a
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI n n
GTI -> (a && b) ~> a
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  snd :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => (a && b) ~> b
snd @a @b = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> (a && b) ~> b
GTE INF b
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
SINF) -> (a && b) ~> b
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SC @a', SC @b') -> case (Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b'), Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a')) of
      (OrderingI n n
LTI, OrderingI n n
_) -> (a && b) ~> b
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      (OrderingI n n
EQI, OrderingI n n
_) -> (a && b) ~> b
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      (OrderingI n n
GTI, OrderingI n n
LTI) -> (a && b) ~> b
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      (OrderingI n n
GTI, OrderingI n n
GTI) -> [Char] -> GTE (C n) (C n)
forall a. HasCallStack => [Char] -> a
error [Char]
"snd: found 2 nats greater than eachother"
  &&& :: forall (a :: COST) (x :: COST) (y :: COST).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
(&&&) @_ @x @y a ~> x
l a ~> y
r = a ~> x
GTE a x
l GTE a x -> ((Ob a, Ob x) => GTE a (x && y)) -> GTE a (x && y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a ~> y
GTE a y
r GTE a y -> ((Ob a, Ob y) => GTE a (x && y)) -> GTE a (x && y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @x @y ((Ob (x && y) => GTE a (x && y)) -> GTE a (x && y))
-> (Ob (x && y) => GTE a (x && y)) -> GTE a (x && y)
forall a b. (a -> b) -> a -> b
$ case (a ~> x
GTE a x
l, a ~> y
GTE a y
r) of
    (GTE a x
Inf, GTE a y
_) -> GTE a (x && y)
GTE INF (x && y)
forall (a :: COST). Ob a => GTE INF a
Inf
    (GTE @_ @x', GTE @_ @y') -> case Proxy b -> Proxy b -> OrderingI b b
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy x') (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy y') of
      OrderingI b b
LTI -> GTE a (x && y)
GTE (C a) (C b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI b b
EQI -> GTE a (x && y)
GTE (C a) (C b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI b b
GTI -> GTE a (x && y)
GTE (C a) (C b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE

instance HasBinaryCoproducts COST where
  type INF || b = b
  type a || INF = a
  type C a || C b = C (Min a b)
  withObCoprod :: forall (a :: COST) (b :: COST) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> r
Ob (a || b) => r
r
    (SCost a
_, SCost b
SINF) -> r
Ob (a || b) => r
r
    (SC @a', SC @b') -> case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b') of
      OrderingI n n
LTI -> r
Ob (a || b) => r
r
      OrderingI n n
EQI -> r
Ob (a || b) => r
r
      OrderingI n n
GTI -> r
Ob (a || b) => r
r
  lft :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => a ~> (a || b)
lft @a @b = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> a ~> (a || b)
GTE INF b
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
SINF) -> a ~> (a || b)
GTE a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    (SC @a', SC @b') -> case (Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b'), Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a')) of
      (OrderingI n n
LTI, OrderingI n n
_) -> a ~> (a || b)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      (OrderingI n n
EQI, OrderingI n n
_) -> a ~> (a || b)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      (OrderingI n n
GTI, OrderingI n n
LTI) -> a ~> (a || b)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      (OrderingI n n
GTI, OrderingI n n
GTI) -> [Char] -> GTE (C n) (C n)
forall a. HasCallStack => [Char] -> a
error [Char]
"lft: found 2 nats greater than eachother"
  rgt :: forall (a :: COST) (b :: COST). (Ob a, Ob b) => b ~> (a || b)
rgt @a @b = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> b ~> (a || b)
GTE b b
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    (SCost a
_, SCost b
SINF) -> b ~> (a || b)
GTE INF a
forall (a :: COST). Ob a => GTE INF a
Inf
    (SC @a', SC @b') -> case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b') of
      OrderingI n n
LTI -> b ~> (a || b)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI n n
EQI -> b ~> (a || b)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI n n
GTI -> b ~> (a || b)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  ||| :: forall (x :: COST) (a :: COST) (y :: COST).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
(|||) @x @y x ~> a
l y ~> a
r = x ~> a
GTE x a
l GTE x a -> ((Ob x, Ob a) => GTE (x || y) a) -> GTE (x || y) a
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// y ~> a
GTE y a
r GTE y a -> ((Ob y, Ob a) => GTE (x || y) a) -> GTE (x || y) a
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @y ((Ob (x ** a) => GTE (x || y) a) -> GTE (x || y) a)
-> (Ob (x ** a) => GTE (x || y) a) -> GTE (x || y) a
forall a b. (a -> b) -> a -> b
$ case (x ~> a
GTE x a
l, y ~> a
GTE y a
r) of
    (GTE x a
Inf, GTE y a
_) -> y ~> a
GTE (x || y) a
r
    (GTE x a
_, GTE y a
Inf) -> x ~> a
GTE (x || y) a
l
    (GTE @x', GTE @y') -> case Proxy a -> Proxy a -> OrderingI a a
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy x') (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy y') of
      OrderingI a a
LTI -> GTE (x || y) a
GTE (C a) (C b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI a a
EQI -> GTE (x || y) a
GTE (C a) (C b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
      OrderingI a a
GTI -> GTE (x || y) a
GTE (C a) (C b)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE

instance MonoidalProfunctor GTE where
  one :: GTE Unit Unit
one = GTE Unit Unit
GTE (C 0) (C 0)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  (**) :: forall x1 x2 y1 y2. GTE x1 x2 -> GTE y1 y2 -> GTE (x1 ** y1) (x2 ** y2)
  GTE x1 x2
l ** :: forall (x1 :: COST) (x2 :: COST) (y1 :: COST) (y2 :: COST).
GTE x1 x2 -> GTE y1 y2 -> GTE (x1 ** y1) (x2 ** y2)
** GTE y1 y2
r = case (GTE x1 x2
l, GTE y1 y2
r) of
    (GTE x1 x2
Inf, GTE y1 y2
_) -> GTE y1 y2
r GTE y1 y2
-> ((Ob y1, Ob y2) => GTE INF (x2 ** y2)) -> GTE INF (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x2 @y2 GTE INF (x2 ** y2)
Ob (x2 ** y2) => GTE INF (x2 ** y2)
forall (a :: COST). Ob a => GTE INF a
Inf
    (GTE x1 x2
_, GTE y1 y2
Inf) -> GTE x1 x2
l GTE x1 x2
-> ((Ob x1, Ob x2) => GTE INF (x2 ** y2)) -> GTE INF (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x2 @y2 GTE INF (x2 ** y2)
Ob (x2 ** y2) => GTE INF (x2 ** y2)
forall (a :: COST). Ob a => GTE INF a
Inf
    (GTE @a @b, GTE @c @d) -> forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a @c ((KnownNat (a + a) => GTE (x1 ** y1) (x2 ** y2))
 -> GTE (x1 ** y1) (x2 ** y2))
-> (KnownNat (a + a) => GTE (x1 ** y1) (x2 ** y2))
-> GTE (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @b @d ((KnownNat (b + b) => GTE (x1 ** y1) (x2 ** y2))
 -> GTE (x1 ** y1) (x2 ** y2))
-> (KnownNat (b + b) => GTE (x1 ** y1) (x2 ** y2))
-> GTE (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$ forall (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat) r.
(a <= b, c <= d, KnownNat (a + c), KnownNat (b + d)) =>
(((a + c) <= (b + d)) => r) -> r
plusMonotone @b @a @d @c GTE (C (a + a)) (C (b + b))
((b + b) <= (a + a)) => GTE (C (a + a)) (C (b + b))
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE

instance Monoidal COST where
  type Unit = C 0
  type INF ** b = INF
  type a ** INF = INF
  type C a ** C b = C (a + b)
  withOb2 :: forall (a :: COST) (b :: COST) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b Ob (a ** b) => r
r = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SC @a', SC @b') -> forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a' @b' r
KnownNat (n + n) => r
Ob (a ** b) => r
r
    (SCost a
SINF, SCost b
_) -> r
Ob (a ** b) => r
r
    (SCost a
_, SCost b
SINF) -> r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: COST). Ob a => (Unit ** a) ~> a
leftUnitor @a = case forall (a :: COST). IsCost a => SCost a
sing @a of
    SCost a
SINF -> (Unit ** a) ~> a
GTE INF INF
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    SCost a
SC -> (Unit ** a) ~> a
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  leftUnitorInv :: forall (a :: COST). Ob a => a ~> (Unit ** a)
leftUnitorInv @a = case forall (a :: COST). IsCost a => SCost a
sing @a of
    SCost a
SINF -> a ~> (Unit ** a)
GTE INF INF
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    SCost a
SC -> a ~> (Unit ** a)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  rightUnitor :: forall (a :: COST). Ob a => (a ** Unit) ~> a
rightUnitor @a = case forall (a :: COST). IsCost a => SCost a
sing @a of
    SCost a
SINF -> (a ** Unit) ~> a
GTE INF INF
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    SCost a
SC -> (a ** Unit) ~> a
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  rightUnitorInv :: forall (a :: COST). Ob a => a ~> (a ** Unit)
rightUnitorInv @a = case forall (a :: COST). IsCost a => SCost a
sing @a of
    SCost a
SINF -> a ~> (a ** Unit)
GTE INF INF
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    SCost a
SC -> a ~> (a ** Unit)
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
  associator :: forall (a :: COST) (b :: COST) (c :: COST).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b, forall (a :: COST). IsCost a => SCost a
sing @c) of
    (SC @a', SC @b', SC @c') -> GTE (C ((n + n) + n)) (C ((n + n) + n))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. a -> b
unsafeCoerce (GTE (C ((n + n) + n)) (C ((n + n) + n))
 -> ((a ** b) ** c) ~> (a ** (b ** c)))
-> GTE (C ((n + n) + n)) (C ((n + n) + n))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall a b. (a -> b) -> a -> b
$ forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a' @b' ((KnownNat (n + n) => GTE (C ((n + n) + n)) (C ((n + n) + n)))
 -> GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> (KnownNat (n + n) => GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> GTE (C ((n + n) + n)) (C ((n + n) + n))
forall a b. (a -> b) -> a -> b
$ forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @(a' + b') @c' ((KnownNat ((n + n) + n) =>
  GTE (C ((n + n) + n)) (C ((n + n) + n)))
 -> GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> (KnownNat ((n + n) + n) =>
    GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> GTE (C ((n + n) + n)) (C ((n + n) + n))
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COST). (CategoryOf COST, Ob a) => Obj a
obj @(C (a' + b' + c'))
    (SCost a
SINF, SCost b
_, SCost c
_) -> ((a ** b) ** c) ~> (a ** (b ** c))
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
SINF, SCost c
_) -> ((a ** b) ** c) ~> (a ** (b ** c))
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
_, SCost c
SINF) -> ((a ** b) ** c) ~> (a ** (b ** c))
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
  associatorInv :: forall (a :: COST) (b :: COST) (c :: COST).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b, forall (a :: COST). IsCost a => SCost a
sing @c) of
    (SC @a', SC @b', SC @c') -> GTE (C ((n + n) + n)) (C ((n + n) + n))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. a -> b
unsafeCoerce (GTE (C ((n + n) + n)) (C ((n + n) + n))
 -> (a ** (b ** c)) ~> ((a ** b) ** c))
-> GTE (C ((n + n) + n)) (C ((n + n) + n))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall a b. (a -> b) -> a -> b
$ forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a' @b' ((KnownNat (n + n) => GTE (C ((n + n) + n)) (C ((n + n) + n)))
 -> GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> (KnownNat (n + n) => GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> GTE (C ((n + n) + n)) (C ((n + n) + n))
forall a b. (a -> b) -> a -> b
$ forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @(a' + b') @c' ((KnownNat ((n + n) + n) =>
  GTE (C ((n + n) + n)) (C ((n + n) + n)))
 -> GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> (KnownNat ((n + n) + n) =>
    GTE (C ((n + n) + n)) (C ((n + n) + n)))
-> GTE (C ((n + n) + n)) (C ((n + n) + n))
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COST). (CategoryOf COST, Ob a) => Obj a
obj @(C (a' + b' + c'))
    (SCost a
SINF, SCost b
_, SCost c
_) -> (a ** (b ** c)) ~> ((a ** b) ** c)
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
SINF, SCost c
_) -> (a ** (b ** c)) ~> ((a ** b) ** c)
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
_, SCost c
SINF) -> (a ** (b ** c)) ~> ((a ** b) ** c)
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf

instance SymMonoidal COST where
  swap :: forall (a :: COST) (b :: COST).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b) of
    (SCost a
SINF, SCost b
_) -> (a ** b) ~> (b ** a)
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
SINF) -> (a ** b) ~> (b ** a)
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SC @a', SC @b') -> GTE (C (n + n)) (C (n + n)) -> GTE (C (n + n)) (C (n + n))
forall a b. a -> b
unsafeCoerce (forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a' @b' (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COST). (CategoryOf COST, Ob a) => Obj a
obj @(C (a' + b'))))

instance Distributive COST where
  distL :: forall (a :: COST) (b :: COST) (c :: COST).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b, forall (a :: COST). IsCost a => SCost a
sing @c) of
    (SCost a
SINF, SCost b
_, SCost c
_) -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SCost a
_, SCost b
SINF, SCost c
_) -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @c GTE (a ** c) (a ** c)
Ob (a ** c) => GTE (a ** c) (a ** c)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    (SCost a
_, SCost b
_, SCost c
SINF) -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b GTE (a ** b) (a ** b)
Ob (a ** b) => GTE (a ** b) (a ** b)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    (SC @a', SC @b', SC @c') -> forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a' @b' ((KnownNat (n + n) => (a ** (b || c)) ~> ((a ** b) || (a ** c)))
 -> (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (KnownNat (n + n) => (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** c))
forall a b. (a -> b) -> a -> b
$
      forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a' @c' ((KnownNat (n + n) => (a ** (b || c)) ~> ((a ** b) || (a ** c)))
 -> (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (KnownNat (n + n) => (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** c))
forall a b. (a -> b) -> a -> b
$
        case (Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy c'), Proxy (n + n) -> Proxy (n + n) -> OrderingI (n + n) (n + n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy (n + n)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (a' + b')) (Proxy (n + n)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (a' + c'))) of
          (OrderingI n n
LTI, OrderingI (n + n) (n + n)
LTI) -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
GTE (C (n + n)) (C (n + n))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
          (OrderingI n n
LTI, OrderingI (n + n) (n + n)
GTI) -> [Char] -> GTE (C (n + n)) (C (n + n))
forall a. HasCallStack => [Char] -> a
error [Char]
"distL: b is less than c, but a + b is greater than a + c"
          (OrderingI n n
EQI, OrderingI (n + n) (n + n)
_) -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
GTE (C (n + n)) (C (n + n))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
          (OrderingI n n
GTI, OrderingI (n + n) (n + n)
LTI) -> [Char] -> GTE (C (n + n)) (C (n + n))
forall a. HasCallStack => [Char] -> a
error [Char]
"distL: b is greater than c, but a + b is less than a + c"
          (OrderingI n n
GTI, OrderingI (n + n) (n + n)
GTI) -> (a ** (b || c)) ~> ((a ** b) || (a ** c))
GTE (C (n + n)) (C (n + n))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
#if !(MIN_VERSION_GLASGOW_HASKELL(9,12,1,0))
          _ -> error "redundant case"
#endif
  distR :: forall (a :: COST) (b :: COST) (c :: COST).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = case (forall (a :: COST). IsCost a => SCost a
sing @a, forall (a :: COST). IsCost a => SCost a
sing @b, forall (a :: COST). IsCost a => SCost a
sing @c) of
    (SCost a
SINF, SCost b
_, SCost c
_) -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c GTE (b ** c) (b ** c)
Ob (b ** c) => GTE (b ** c) (b ** c)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    (SCost a
_, SCost b
SINF, SCost c
_) -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @c GTE (a ** c) (a ** c)
Ob (a ** c) => GTE (a ** c) (a ** c)
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
    (SCost a
_, SCost b
_, SCost c
SINF) -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
    (SC @a', SC @b', SC @c') -> forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @a' @c' ((KnownNat (n + n) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (KnownNat (n + n) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
forall a b. (a -> b) -> a -> b
$
      forall (a :: Nat) (b :: Nat) r.
(KnownNat a, KnownNat b) =>
(KnownNat (a + b) => r) -> r
withPlusIsNat @b' @c' ((KnownNat (n + n) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (KnownNat (n + n) => ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
forall a b. (a -> b) -> a -> b
$
        case (Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy a') (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy b'), Proxy (n + n) -> Proxy (n + n) -> OrderingI (n + n) (n + n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (Proxy (n + n)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (a' + c')) (Proxy (n + n)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (b' + c'))) of
          (OrderingI n n
LTI, OrderingI (n + n) (n + n)
LTI) -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
GTE (C (n + n)) (C (n + n))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
          (OrderingI n n
LTI, OrderingI (n + n) (n + n)
GTI) -> [Char] -> GTE (C (n + n)) (C (n + n))
forall a. HasCallStack => [Char] -> a
error [Char]
"distR: a is less than b, but a + c is greater than b + c"
          (OrderingI n n
EQI, OrderingI (n + n) (n + n)
_) -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
GTE (C (n + n)) (C (n + n))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
          (OrderingI n n
GTI, OrderingI (n + n) (n + n)
LTI) -> [Char] -> GTE (C (n + n)) (C (n + n))
forall a. HasCallStack => [Char] -> a
error [Char]
"distR: a is greater than b, but a + c is less than b + c"
          (OrderingI n n
GTI, OrderingI (n + n) (n + n)
GTI) -> ((a || b) ** c) ~> ((a ** c) || (b ** c))
GTE (C (n + n)) (C (n + n))
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
#if !(MIN_VERSION_GLASGOW_HASKELL(9,12,1,0))
          _ -> error "redundant case"
#endif
  absorbL :: forall (a :: COST). Ob a => (a ** InitialObject) ~> InitialObject
absorbL = (a ** InitialObject) ~> InitialObject
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
  absorbR :: forall (a :: COST). Ob a => (InitialObject ** a) ~> InitialObject
absorbR = (InitialObject ** a) ~> InitialObject
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf

-- | @COST@ is thin and totally ordered, so equalizers are trivial. @factorEqualizer incl h@ just
-- compares @e@ and @e'@ directly (their common bound @x@ does not matter), erroring when and only
-- when @e'@ is finite and strictly less than @e@, or @e@ is 'INF' while @e'@ is finite.
instance HasEqualizers COST where
  equalize :: forall (a :: COST) (b :: COST) r.
(a ~> b) -> (a ~> b) -> (forall (e :: COST). (e ~> a) -> r) -> r
equalize = (a ~> b) -> (a ~> b) -> (forall (e :: COST). (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 :: COST) (x :: COST) (e' :: COST).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer @e @_ @e' e ~> x
incl e' ~> x
h =
    ( case (forall (a :: COST). IsCost a => SCost a
sing @e', forall (a :: COST). IsCost a => SCost a
sing @e) of
        (SCost e'
SINF, SCost e
_) -> GTE e' e
GTE INF e
forall (a :: COST). Ob a => GTE INF a
Inf
        (SCost e'
SC, SCost e
SINF) -> [Char] -> GTE e' e
forall a. HasCallStack => [Char] -> a
error [Char]
"factorEqualizer: h's image must lie within incl's image"
        (SC @b, SC @a) -> case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @b) of
          OrderingI n n
LTI -> GTE e' e
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
          OrderingI n n
EQI -> GTE e' e
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
          OrderingI n n
GTI -> [Char] -> GTE e' e
forall a. HasCallStack => [Char] -> a
error [Char]
"factorEqualizer: h's image must lie within incl's image"
    )
      ((Ob e, Ob x) => GTE e' e) -> GTE e x -> GTE e' e
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COST) (b :: COST) r.
((Ob a, Ob b) => r) -> GTE a b -> r
\\ e ~> x
GTE e x
incl
      ((Ob e', Ob x) => GTE e' e) -> GTE e' x -> GTE e' e
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COST) (b :: COST) r.
((Ob a, Ob b) => r) -> GTE a b -> r
\\ e' ~> x
GTE e' x
h

-- | Dual to the 'HasEqualizers' instance above.
instance HasCoequalizers COST where
  coequalize :: forall (a :: COST) (b :: COST) r.
(a ~> b) -> (a ~> b) -> (forall (c :: COST). (b ~> c) -> r) -> r
coequalize = (a ~> b) -> (a ~> b) -> (forall (c :: COST). (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 :: COST) (x :: COST) (c' :: COST).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer @c @_ @c' x ~> c
q x ~> c'
h =
    ( case (forall (a :: COST). IsCost a => SCost a
sing @c, forall (a :: COST). IsCost a => SCost a
sing @c') of
        (SCost c
SINF, SCost c'
_) -> GTE c c'
GTE INF c'
forall (a :: COST). Ob a => GTE INF a
Inf
        (SCost c
SC, SCost c'
SINF) -> [Char] -> GTE c c'
forall a. HasCallStack => [Char] -> a
error [Char]
"factorCoequalizer: h must be constant on q's fibers"
        (SC @a, SC @b) -> case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @b) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a) of
          OrderingI n n
LTI -> GTE c c'
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
          OrderingI n n
EQI -> GTE c c'
GTE (C n) (C n)
forall (a :: Nat) (b :: Nat).
(KnownNat a, KnownNat b, b <= a) =>
GTE (C a) (C b)
GTE
          OrderingI n n
GTI -> [Char] -> GTE c c'
forall a. HasCallStack => [Char] -> a
error [Char]
"factorCoequalizer: h must be constant on q's fibers"
    )
      ((Ob x, Ob c) => GTE c c') -> GTE x c -> GTE c c'
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COST) (b :: COST) r.
((Ob a, Ob b) => r) -> GTE a b -> r
\\ x ~> c
GTE x c
q
      ((Ob x, Ob c') => GTE c c') -> GTE x c' -> GTE c c'
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: COST) (b :: COST) r.
((Ob a, Ob b) => r) -> GTE a b -> r
\\ x ~> c'
GTE x c'
h

instance HasPullbacks COST where
  pullback :: forall (o :: COST) (a :: COST) (b :: COST) r.
(a ~> o)
-> (b ~> o) -> (forall (p :: COST). (p ~> a) -> (p ~> b) -> r) -> r
pullback = (a ~> o)
-> (b ~> o) -> (forall (p :: COST). (p ~> a) -> (p ~> b) -> r) -> r
forall {k} (o :: k) (a :: k) (b :: k) r.
(Thin k, HasProducts k) =>
(a ~> o)
-> (b ~> o) -> (forall (p :: k). (p ~> a) -> (p ~> b) -> r) -> r
thinPullback
  factorPullback :: forall (a :: COST) (b :: COST) (p :: COST) (q :: COST).
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullback = (p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
forall {k} (a :: k) (b :: k) (p :: k) (q :: k).
(HasEqualizers k, HasProducts k) =>
(p ~> a) -> (p ~> b) -> (q ~> a) -> (q ~> b) -> q ~> p
factorPullbackDefault

instance HasPushouts COST where
  pushout :: forall (o :: COST) (a :: COST) (b :: COST) r.
(o ~> a)
-> (o ~> b) -> (forall (p :: COST). (a ~> p) -> (b ~> p) -> r) -> r
pushout = (o ~> a)
-> (o ~> b) -> (forall (p :: COST). (a ~> p) -> (b ~> p) -> r) -> r
forall {k} (o :: k) (a :: k) (b :: k) r.
(Thin k, HasCoproducts k) =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
thinPushout
  factorPushout :: forall (a :: COST) (b :: COST) (p :: COST) (q :: COST).
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushout = (a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
forall {k} (a :: k) (b :: k) (p :: k) (q :: k).
(HasCoequalizers k, HasCoproducts k) =>
(a ~> p) -> (b ~> p) -> (a ~> q) -> (b ~> q) -> p ~> q
factorPushoutDefault

instance HasEpiMonoFactorization COST