module Proarrow.Category.Instance.Fin where

import Proarrow.Core (CAT, CategoryOf (..), Obj, Profunctor (..), Promonad (..), dimapDefault, obj)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..))

type data NAT = Z | S NAT

type data FIN n where
  FZ :: FIN (S n)
  FS :: FIN (S n) -> FIN (S (S n))

type FIN0 = FIN Z
type FIN1 = FIN (S Z)
type FIN2 = FIN (S (S Z))
type FIN3 = FIN (S (S (S Z)))

type LTE :: forall {n :: NAT}. CAT (FIN n)
data LTE a b where
  ZEQ :: LTE FZ FZ
  ZLT :: LTE FZ b -> LTE FZ (FS b)
  SLT :: LTE a b -> LTE (FS a) (FS b)

absurdL :: (a :: FIN Z) ~> b
absurdL :: forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdL @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN Z). (CategoryOf (FIN Z), Ob a) => Obj a
obj @a of {}

absurdR :: a ~> (b :: FIN Z)
absurdR :: forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR @_ @b = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN Z). (CategoryOf (FIN Z), Ob a) => Obj a
obj @b of {}

class IsFin (a :: FIN n) where
  finId :: Obj a
instance IsFin (a :: FIN Z) where
  finId :: Obj a
finId = Obj a
forall (n :: NAT) (a :: FIN n). IsFin a => Obj a
finId
instance IsFin FZ where
  finId :: Obj FZ
finId = Obj FZ
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
instance (IsFin b) => IsFin (FS b) where
  finId :: Obj (FS b)
finId = LTE b b -> LTE (FS b) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT Obj b
LTE b b
forall (n :: NAT) (a :: FIN n). IsFin a => Obj a
finId

instance Profunctor LTE where
  dimap :: forall (c :: FIN n) (a :: FIN n) (b :: FIN n) (d :: FIN n).
(c ~> a) -> (b ~> d) -> LTE a b -> LTE c d
dimap = (c ~> a) -> (b ~> d) -> LTE a b -> LTE c d
LTE c a -> LTE b d -> LTE a b -> LTE c d
forall {k} (p :: PRO 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 :: FIN n) (b :: FIN n) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
ZEQ = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ ZLT LTE FZ b
b = r
(Ob a, Ob b) => r
(Ob FZ, Ob b) => r
r ((Ob FZ, Ob b) => r) -> LTE FZ b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE FZ b
b
  (Ob a, Ob b) => r
r \\ SLT LTE a b
ab = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> LTE a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
ab
instance Promonad LTE where
  id :: forall (a :: FIN n). Ob a => LTE a a
id = Obj a
LTE a a
forall (n :: NAT) (a :: FIN n). IsFin a => Obj a
finId
  LTE b c
ZEQ . :: forall (b :: FIN n) (c :: FIN n) (a :: FIN n).
LTE b c -> LTE a b -> LTE a c
. LTE a b
ZEQ = LTE a c
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
b . LTE a b
ZEQ = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT LTE FZ b
b
  SLT LTE a b
ab . ZLT LTE FZ b
za = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (LTE a b
ab LTE a b -> LTE FZ a -> LTE FZ b
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FIN (S n)) (c :: FIN (S n)) (a :: FIN (S n)).
LTE b c -> LTE a b -> LTE a c
. LTE FZ a
LTE FZ b
za)
  SLT LTE a b
ab . SLT LTE a b
bc = LTE a b -> LTE (FS a) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (LTE a b
ab LTE a b -> LTE a a -> LTE a b
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
forall (b :: FIN (S n)) (c :: FIN (S n)) (a :: FIN (S n)).
LTE b c -> LTE a b -> LTE a c
. LTE a a
LTE a b
bc)
instance CategoryOf (FIN n) where
  type (~>) = LTE
  type Ob a = IsFin a

class IsLTE (a :: FIN n) (b :: FIN n) where
  lte :: a ~> b
instance IsLTE FZ FZ where
  lte :: FZ ~> FZ
lte = FZ ~> FZ
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
instance (IsLTE FZ b) => IsLTE FZ (FS b) where
  lte :: FZ ~> FS b
lte = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT FZ ~> b
LTE FZ b
forall (n :: NAT) (a :: FIN n) (b :: FIN n). IsLTE a b => a ~> b
lte
instance (IsLTE a b) => IsLTE (FS a) (FS b) where
  lte :: FS a ~> FS b
lte = LTE a b -> LTE (FS a) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT a ~> b
LTE a b
forall (n :: NAT) (a :: FIN n) (b :: FIN n). IsLTE a b => a ~> b
lte
instance ThinProfunctor LTE where
  type HasArrow LTE a b = IsLTE a b
  arr :: forall (a :: FIN n) (b :: FIN n).
(Ob a, Ob b, HasArrow LTE a b) =>
LTE a b
arr = a ~> b
LTE a b
forall (n :: NAT) (a :: FIN n) (b :: FIN n). IsLTE a b => a ~> b
lte
  withArr :: forall (a :: FIN n) (b :: FIN n) r.
LTE a b -> (HasArrow LTE a b => r) -> r
withArr LTE a b
ZEQ HasArrow LTE a b => r
r = r
HasArrow LTE a b => r
r
  withArr (ZLT LTE FZ b
b) HasArrow LTE a b => r
r = LTE FZ b -> (HasArrow LTE FZ b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
LTE a b -> (HasArrow LTE a b => r) -> r
withArr LTE FZ b
b r
HasArrow LTE a b => r
HasArrow LTE FZ b => r
r
  withArr (SLT LTE a b
ab) HasArrow LTE a b => r
r = LTE a b -> (HasArrow LTE a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
LTE a b -> (HasArrow LTE a b => r) -> r
withArr LTE a b
ab r
HasArrow LTE a b => r
HasArrow LTE a b => r
r

instance HasInitialObject (FIN (S n)) where
  type InitialObject = FZ
  initiate' :: forall (a' :: FIN (S n)) (a :: FIN (S n)).
(a' ~> a) -> InitialObject ~> a
initiate' a' ~> a
LTE a' a
ZEQ = InitialObject ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  initiate' (ZLT LTE FZ b
b) = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT LTE FZ b
b
  initiate' (SLT LTE a b
ab) = LTE FZ b -> LTE FZ (FS b)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT ((a ~> b) -> InitialObject ~> b
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: FIN (S n)) (a :: FIN (S n)).
(a' ~> a) -> InitialObject ~> a
initiate' a ~> b
LTE a b
ab)

instance HasTerminalObject (FIN (S Z)) where
  type TerminalObject = FZ
  terminate' :: forall (a :: FIN (S Z)) (a' :: FIN (S Z)).
(a ~> a') -> a ~> TerminalObject
terminate' a ~> a'
LTE a a'
ZEQ = a ~> TerminalObject
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ

instance (HasTerminalObject (FIN (S n))) => HasTerminalObject (FIN (S (S n))) where
  type TerminalObject = FS TerminalObject
  terminate' :: forall (a :: FIN (S (S n))) (a' :: FIN (S (S n))).
(a ~> a') -> a ~> TerminalObject
terminate' a ~> a'
LTE a a'
ZEQ = LTE FZ TerminalObject -> LTE FZ (FS TerminalObject)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT ((FZ ~> FZ) -> FZ ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
forall (a :: FIN (S n)) (a' :: FIN (S n)).
(a ~> a') -> a ~> TerminalObject
terminate' FZ ~> FZ
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ)
  terminate' (ZLT LTE FZ b
b) = LTE FZ TerminalObject -> LTE FZ (FS TerminalObject)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT ((FZ ~> b) -> FZ ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
forall (a :: FIN (S n)) (a' :: FIN (S n)).
(a ~> a') -> a ~> TerminalObject
terminate' FZ ~> b
LTE FZ b
b)
  terminate' (SLT LTE a b
ab) = LTE a TerminalObject -> LTE (FS a) (FS TerminalObject)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT ((a ~> b) -> a ~> TerminalObject
forall k (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
forall (a :: FIN (S n)) (a' :: FIN (S n)).
(a ~> a') -> a ~> TerminalObject
terminate' a ~> b
LTE a b
ab)

instance HasBinaryCoproducts (FIN Z) where
  type a || b = a
  withObCoprod :: forall (a :: FIN Z) (b :: FIN Z) 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 :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => a ~> (a || b)
lft = a ~> a
a ~> (a || b)
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  rgt :: forall (a :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => b ~> (a || b)
rgt = b ~> a
b ~> (a || b)
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  ||| :: forall (x :: FIN Z) (a :: FIN Z) (y :: FIN Z).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
(|||) = \case {}

instance HasBinaryCoproducts (FIN (S Z)) where
  type FZ || FZ = FZ
  withObCoprod :: forall (a :: FIN (S Z)) (b :: FIN (S Z)) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @b) of (LTE a a
ZEQ, LTE b b
ZEQ) -> r
Ob (a || b) => r
r
  lft :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @b) of (LTE a a
ZEQ, LTE b b
ZEQ) -> a ~> (a || b)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  rgt :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @b) of (LTE a a
ZEQ, LTE b b
ZEQ) -> b ~> (a || b)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  x ~> a
LTE x a
ZEQ ||| :: forall (x :: FIN (S Z)) (a :: FIN (S Z)) (y :: FIN (S Z)).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
LTE y FZ
ZEQ = (x || y) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ

-- | Maximum
instance (HasBinaryCoproducts (FIN (S n))) => HasBinaryCoproducts (FIN (S (S n))) where
  type FZ || b = b
  type a || FZ = a
  type FS a || FS b = FS (a || b)
  withObCoprod :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @a of
    Obj a
LTE a a
ZEQ -> r
Ob (a || b) => r
r
    SLT @a' LTE a b
a -> case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @b of
      Obj b
LTE b b
ZEQ -> r
Ob (a || b) => r
r
      SLT @b' LTE a b
b -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(FIN (S n)) @a' @b' r
Ob (a || a) => r
Ob (a || b) => r
r ((Ob a, Ob b) => r) -> LTE a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
a ((Ob a, Ob b) => r) -> LTE a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
b

  lft :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @b) of
    (LTE a a
ZEQ, LTE b b
ZEQ) -> a ~> (a || b)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    (LTE a a
ZEQ, SLT LTE a b
b) -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT ((a ~> a) -> InitialObject ~> a
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: FIN (S n)) (a :: FIN (S n)).
(a' ~> a) -> InitialObject ~> a
initiate' a ~> a
LTE a b
b)
    (LTE a a
a, LTE b b
ZEQ) -> a ~> (a || b)
LTE a a
a
    (SLT @a' LTE a b
ab, SLT @b' LTE a b
b) -> LTE a (a || a) -> LTE (FS a) (FS (a || a))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a' @b' ((Ob a, Ob b) => LTE a (a || a)) -> LTE a b -> LTE a (a || a)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
ab ((Ob a, Ob b) => LTE a (a || a)) -> LTE a b -> LTE a (a || a)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
b)

  rgt :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @b) of
    (LTE a a
ZEQ, LTE b b
ZEQ) -> b ~> (a || b)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    (SLT LTE a b
a, LTE b b
ZEQ) -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT ((a ~> a) -> InitialObject ~> a
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: FIN (S n)) (a :: FIN (S n)).
(a' ~> a) -> InitialObject ~> a
initiate' a ~> a
LTE a b
a)
    (LTE a a
ZEQ, LTE b b
b) -> b ~> (a || b)
LTE b b
b
    (SLT @a' LTE a b
a, SLT @b' LTE a b
ab) -> LTE a (a || a) -> LTE (FS a) (FS (a || a))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a' @b' ((Ob a, Ob b) => LTE a (a || a)) -> LTE a b -> LTE a (a || a)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
a ((Ob a, Ob b) => LTE a (a || a)) -> LTE a b -> LTE a (a || a)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
ab)

  x ~> a
LTE x a
ZEQ ||| :: forall (x :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
LTE y FZ
ZEQ = (x || y) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
ZEQ ||| y ~> a
a = y ~> a
(x || y) ~> a
a
  x ~> a
a ||| ZLT LTE FZ b
ZEQ = x ~> a
(x || y) ~> a
a
  ZLT a :: LTE FZ b
a@ZLT{} ||| ZLT b :: LTE FZ b
b@ZLT{} = LTE FZ (FS b) -> LTE FZ (FS (FS b))
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (FZ ~> FS b
LTE FZ b
a (FZ ~> FS b) -> (FZ ~> FS b) -> (FZ || FZ) ~> FS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FZ ~> FS b
LTE FZ b
b)
  ZLT a :: LTE FZ b
a@ZLT{} ||| SLT LTE a b
bc = LTE (FZ || a) (FS b) -> LTE (FS (FZ || a)) (FS (FS b))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (FZ ~> FS b
LTE FZ b
a (FZ ~> FS b) -> (a ~> FS b) -> (FZ || a) ~> FS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> FS b
LTE a b
bc)
  SLT LTE a b
ab ||| ZLT c :: LTE FZ b
c@ZLT{} = LTE (a || FZ) (FS b) -> LTE (FS (a || FZ)) (FS (FS b))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (a ~> FS b
LTE a b
ab (a ~> FS b) -> (FZ ~> FS b) -> (a || FZ) ~> FS b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: FIN (S (S n))) (a :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FZ ~> FS b
LTE FZ b
c)
  SLT LTE a b
a ||| SLT LTE a b
b = LTE (a || a) b -> LTE (FS (a || a)) (FS b)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (a ~> b
LTE a b
a (a ~> b) -> (a ~> b) -> (a || a) ~> b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: FIN (S n)) (a :: FIN (S n)) (y :: FIN (S n)).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> b
LTE a b
b)

instance HasBinaryProducts (FIN Z) where
  type a && b = a
  withObProd :: forall (a :: FIN Z) (b :: FIN Z) 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 :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => (a && b) ~> a
fst = a ~> a
(a && b) ~> a
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  snd :: forall (a :: FIN Z) (b :: FIN Z). (Ob a, Ob b) => (a && b) ~> b
snd = a ~> b
(a && b) ~> b
forall (a :: FIN Z) (b :: FIN Z). a ~> b
absurdR
  &&& :: forall (a :: FIN Z) (x :: FIN Z) (y :: FIN Z).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
(&&&) = \case {}

instance HasBinaryProducts (FIN (S Z)) where
  type FZ && FZ = FZ
  withObProd :: forall (a :: FIN (S Z)) (b :: FIN (S Z)) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @b) of (LTE a a
ZEQ, LTE b b
ZEQ) -> r
Ob (a && b) => r
r
  fst :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @b) of (LTE a a
ZEQ, LTE b b
ZEQ) -> (a && b) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  snd :: forall (a :: FIN (S Z)) (b :: FIN (S Z)).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S Z)). (CategoryOf (FIN (S Z)), Ob a) => Obj a
obj @b) of (LTE a a
ZEQ, LTE b b
ZEQ) -> (a && b) ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  a ~> x
LTE a x
ZEQ &&& :: forall (a :: FIN (S Z)) (x :: FIN (S Z)) (y :: FIN (S Z)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
LTE FZ y
ZEQ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ

-- | Minimum
instance (HasBinaryProducts (FIN (S n))) => HasBinaryProducts (FIN (S (S n))) where
  type FZ && b = FZ
  type a && FZ = FZ
  type FS a && FS b = FS (a && b)
  withObProd :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @a of
    Obj a
LTE a a
ZEQ -> r
Ob (a && b) => r
r
    SLT @a' LTE a b
a -> case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @b of
      Obj b
LTE b b
ZEQ -> r
Ob (a && b) => r
r
      SLT @b' LTE a b
b -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(FIN (S n)) @a' @b' r
Ob (a && a) => r
Ob (a && b) => r
r ((Ob a, Ob b) => r) -> LTE a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
a ((Ob a, Ob b) => r) -> LTE a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
b

  fst :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @b) of
    (LTE a a
ZEQ, LTE b b
ZEQ) -> (a && b) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    (LTE a a
ZEQ, SLT LTE a b
_) -> (a && b) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    (LTE a a
a , LTE b b
ZEQ) -> Obj a -> InitialObject ~> a
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: FIN (S (S n))) (a :: FIN (S (S n))).
(a' ~> a) -> InitialObject ~> a
initiate' Obj a
LTE a a
a
    (SLT @a' LTE a b
l, SLT @b' LTE a b
r) -> LTE (a && a) a -> LTE (FS (a && a)) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a' @b' ((Ob a, Ob b) => LTE (a && a) a) -> LTE a b -> LTE (a && a) a
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
l ((Ob a, Ob b) => LTE (a && a) a) -> LTE a b -> LTE (a && a) a
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
r)

  snd :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: FIN (S (S n))).
(CategoryOf (FIN (S (S n))), Ob a) =>
Obj a
obj @b) of
    (LTE a a
ZEQ, LTE b b
ZEQ) -> (a && b) ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    (SLT LTE a b
_, LTE b b
ZEQ) -> (a && b) ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    (LTE a a
ZEQ, LTE b b
b) -> Obj b -> InitialObject ~> b
forall k (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
forall (a' :: FIN (S (S n))) (a :: FIN (S (S n))).
(a' ~> a) -> InitialObject ~> a
initiate' Obj b
LTE b b
b
    (SLT @a' LTE a b
l, SLT @b' LTE a b
r) -> LTE (a && a) a -> LTE (FS (a && a)) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a' @b' ((Ob a, Ob b) => LTE (a && a) a) -> LTE a b -> LTE (a && a) a
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
l ((Ob a, Ob b) => LTE (a && a) a) -> LTE a b -> LTE (a && a) a
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FIN (S n)) (b :: FIN (S n)) r.
((Ob a, Ob b) => r) -> LTE a b -> r
\\ LTE a b
r)

  a ~> x
LTE a x
ZEQ &&& :: forall (a :: FIN (S (S n))) (x :: FIN (S (S n)))
       (y :: FIN (S (S n))).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
LTE FZ y
ZEQ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
_ &&& a ~> y
LTE FZ y
ZEQ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  a ~> x
LTE a x
ZEQ &&& ZLT LTE FZ b
_ = a ~> (x && y)
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
  ZLT LTE FZ b
a &&& ZLT LTE FZ b
b = LTE FZ (b && b) -> LTE FZ (FS (b && b))
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (FZ ~> b
LTE FZ b
a (FZ ~> b) -> (FZ ~> b) -> FZ ~> (b && b)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: FIN (S n)) (x :: FIN (S n)) (y :: FIN (S n)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& FZ ~> b
LTE FZ b
b)
  SLT LTE a b
a &&& SLT LTE a b
b = LTE a (b && b) -> LTE (FS a) (FS (b && b))
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT (a ~> b
LTE a b
a (a ~> b) -> (a ~> b) -> a ~> (b && b)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: FIN (S n)) (x :: FIN (S n)) (y :: FIN (S n)).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> b
LTE a b
b)