{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Instance.Cost where

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

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, (//), obj)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts(..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts(..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Object.Initial (HasInitialObject (..))

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 :: k +-> 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 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 :: k +-> 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 :: k +-> 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
  par0 :: GTE Unit Unit
par0 = 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
  par :: forall x1 x2 y1 y2. GTE x1 x2 -> GTE y1 y2 -> GTE (x1 ** y1) (x2 ** y2)
  GTE x1 x2
l par :: forall (x1 :: COST) (x2 :: COST) (y1 :: COST) (y2 :: COST).
GTE x1 x2 -> GTE y1 y2 -> GTE (x1 ** y1) (x2 ** y2)
`par` 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
  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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> 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 :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COST). Ob a => GTE a a
id
  distL0 :: forall (a :: COST). Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf
  distR0 :: forall (a :: COST). Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
GTE INF INF
forall (a :: COST). Ob a => GTE INF a
Inf