module Proarrow.Category.Instance.Fin where

import Data.Kind (Constraint, Type)

import Proarrow.Core (CAT, CategoryOf (..), 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 SFin :: forall {n :: NAT}. FIN n -> Type
data SFin a where
  SZ :: SFin FZ
  SS :: (IsFin a) => SFin (FS a)

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 {}

type IsFin :: forall {n :: NAT}. FIN n -> Constraint
class IsFin (a :: FIN n) where
  singFin :: SFin a
instance IsFin (a :: FIN Z) where
  singFin :: SFin a
singFin = SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin
instance IsFin FZ where
  singFin :: SFin FZ
singFin = SFin FZ
forall (n :: NAT). SFin FZ
SZ
instance (IsFin b) => IsFin (FS b) where
  singFin :: SFin (FS b)
singFin = SFin (FS b)
forall (n :: NAT) (b :: FIN (S n)). IsFin b => SFin (FS b)
SS

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 @a = case forall (a :: FIN n). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> LTE a a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    SFin a
SS -> LTE a a -> LTE (FS a) (FS a)
forall {n :: NAT} (b :: FIN (S n)) (b :: FIN (S n)).
LTE b b -> LTE (FS b) (FS b)
SLT LTE a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FIN (S n)). Ob a => LTE a a
id
  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)). Ob a => InitialObject ~> a
initiate @a = case forall (a :: FIN (S n)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> InitialObject ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
    SS @a' -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a')

instance HasTerminalObject (FIN (S Z)) where
  type TerminalObject = FZ
  terminate :: forall (a :: FIN (S Z)). Ob a => a ~> TerminalObject
terminate @a = case forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of SFin a
SZ -> 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))). Ob a => a ~> TerminalObject
terminate @a = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> LTE FZ TerminalObject -> LTE FZ (FS TerminalObject)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT FZ ~> TerminalObject
LTE FZ TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FIN (S n)). Ob a => a ~> TerminalObject
terminate
    SS @a' -> 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 (forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate @_ @a')

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 (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> 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 (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> 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 (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> 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 (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> r
Ob (a || b) => r
r
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> r
Ob (a || b) => r
r
      SS @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

  lft :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
a ~> (a || b)
lft @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
    SFin b
SZ -> 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
    SS @b' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
      SFin a
SZ -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b')
      SS @a' -> 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')

  rgt :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> 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
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> LTE FZ a -> LTE FZ (FS a)
forall {n :: NAT} (b :: FIN (S n)). LTE FZ b -> LTE FZ (FS b)
ZLT (forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a')
      SS @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) =>
b ~> (a || b)
rgt @_ @a' @b')

  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 (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> 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 (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> (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 (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a, forall (a :: FIN (S Z)). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b) of (SFin a
SZ, SFin b
SZ) -> (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 (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> r
Ob (a && b) => r
r
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> r
Ob (a && b) => r
r
      SS @b' -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a' @b' r
Ob (a && a) => r
Ob (a && b) => r
r

  fst :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
(a && b) ~> a
fst @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
    SFin b
SZ -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @a
    SS @b' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
      SFin a
SZ -> (a && b) ~> a
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
      SS @a' -> 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')

  snd :: forall (a :: FIN (S (S n))) (b :: FIN (S (S n))).
(Ob a, Ob b) =>
(a && b) ~> b
snd @a @b = case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @a of
    SFin a
SZ -> forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate @_ @b
    SS @a' -> case forall (a :: FIN (S (S n))). IsFin a => SFin a
forall {n :: NAT} (a :: FIN n). IsFin a => SFin a
singFin @b of
      SFin b
SZ -> (a && b) ~> b
LTE FZ FZ
forall {n :: NAT}. LTE FZ FZ
ZEQ
      SS @b' -> 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')

  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)