{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds, FlexibleInstances, FlexibleContexts, UndecidableInstances, NoImplicitPrelude #-}
{-# LANGUAGE EmptyCase, TypeApplications, ScopedTypeVariables, TypeOperators #-}
module Data.Category.Fin where

import Data.Category
import Data.Category.Limit
import Data.Category.CartesianClosed

data Nat = Z | S Nat

data Fin n where
  FZ :: Fin ('S n)
  FS :: Fin n -> Fin ('S n)

data LTE (n :: Nat) (a :: Fin n) (b :: Fin n) where
  ZEQ :: LTE ('S m) 'FZ 'FZ
  ZLT :: LTE ('S m) 'FZ  b -> LTE ('S ('S m))  'FZ    ('FS b)
  SLT :: LTE ('S m)  a   b -> LTE ('S ('S m)) ('FS a) ('FS b)

instance Category (LTE n) where
  src :: forall (a :: Fin n) (b :: Fin n). LTE n a b -> Obj (LTE n) a
src LTE n a b
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  src (ZLT LTE ('S m) 'FZ b
_) = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  src (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src LTE ('S m) a b
a)
  tgt :: forall (a :: Fin n) (b :: Fin n). LTE n a b -> Obj (LTE n) b
tgt LTE n a b
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  tgt (ZLT LTE ('S m) 'FZ b
a) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt LTE ('S m) 'FZ b
a)
  tgt (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt LTE ('S m) a b
a)
  LTE n b c
ZEQ . :: forall (b :: Fin n) (c :: Fin n) (a :: Fin n).
LTE n b c -> LTE n a b -> LTE n a c
. LTE n a b
a = LTE n a b
a
  LTE n b c
a . LTE n a b
ZEQ = LTE n b c
a
  SLT LTE ('S m) a b
a . ZLT LTE ('S m) 'FZ b
b = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. LTE ('S m) 'FZ b
b)
  SLT LTE ('S m) a b
a . SLT LTE ('S m) a b
b = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. LTE ('S m) a b
b)

instance HasInitialObject (LTE ('S n)) where
  type InitialObject (LTE ('S n)) = 'FZ
  initialObject :: Obj (LTE ('S n)) (InitialObject (LTE ('S n)))
initialObject = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  initialize :: forall (a :: Fin ('S n)).
Obj (LTE ('S n)) a -> LTE ('S n) (InitialObject (LTE ('S n))) a
initialize LTE ('S n) a a
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  initialize (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize LTE ('S m) a b
a)

instance HasTerminalObject (LTE ('S 'Z)) where
  type TerminalObject (LTE ('S 'Z)) = 'FZ
  terminalObject :: Obj (LTE ('S 'Z)) (TerminalObject (LTE ('S 'Z)))
terminalObject = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  terminate :: forall (a :: Fin ('S 'Z)).
Obj (LTE ('S 'Z)) a -> LTE ('S 'Z) a (TerminalObject (LTE ('S 'Z)))
terminate LTE ('S 'Z) a a
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ

instance HasTerminalObject (LTE ('S n)) => HasTerminalObject (LTE ('S ('S n))) where
  type TerminalObject (LTE ('S ('S n))) = 'FS (TerminalObject (LTE ('S n)))
  terminalObject :: Obj (LTE ('S ('S n))) (TerminalObject (LTE ('S ('S n))))
terminalObject = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
  terminate :: forall (a :: Fin ('S ('S n))).
Obj (LTE ('S ('S n))) a
-> LTE ('S ('S n)) a (TerminalObject (LTE ('S ('S n))))
terminate LTE ('S ('S n)) a a
ZEQ = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ)
  terminate (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate LTE ('S m) a b
a)

instance HasBinaryCoproducts (LTE ('S 'Z)) where
  type BinaryCoproduct (LTE ('S 'Z)) 'FZ 'FZ = 'FZ
  inj1 :: forall (x :: Fin ('S 'Z)) (y :: Fin ('S 'Z)).
Obj (LTE ('S 'Z)) x
-> Obj (LTE ('S 'Z)) y
-> LTE ('S 'Z) x (BinaryCoproduct (LTE ('S 'Z)) x y)
inj1 LTE ('S 'Z) x x
ZEQ LTE ('S 'Z) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  inj2 :: forall (x :: Fin ('S 'Z)) (y :: Fin ('S 'Z)).
Obj (LTE ('S 'Z)) x
-> Obj (LTE ('S 'Z)) y
-> LTE ('S 'Z) y (BinaryCoproduct (LTE ('S 'Z)) x y)
inj2 LTE ('S 'Z) x x
ZEQ LTE ('S 'Z) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  LTE ('S 'Z) x a
ZEQ ||| :: forall (x :: Fin ('S 'Z)) (a :: Fin ('S 'Z)) (y :: Fin ('S 'Z)).
LTE ('S 'Z) x a
-> LTE ('S 'Z) y a
-> LTE ('S 'Z) (BinaryCoproduct (LTE ('S 'Z)) x y) a
||| LTE ('S 'Z) y a
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ

instance HasBinaryCoproducts (LTE ('S n)) => HasBinaryCoproducts (LTE ('S ('S n))) where
  type BinaryCoproduct (LTE ('S ('S n))) 'FZ 'FZ = 'FZ
  type BinaryCoproduct (LTE ('S ('S n))) 'FZ ('FS b) = 'FS (BinaryCoproduct (LTE ('S n)) 'FZ b)
  type BinaryCoproduct (LTE ('S ('S n))) ('FS a) 'FZ = 'FS (BinaryCoproduct (LTE ('S n)) a 'FZ)
  type BinaryCoproduct (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (BinaryCoproduct (LTE ('S n)) a b)
  inj1 :: forall (x :: Fin ('S ('S n))) (y :: Fin ('S ('S n))).
Obj (LTE ('S ('S n))) x
-> Obj (LTE ('S ('S n))) y
-> LTE ('S ('S n)) x (BinaryCoproduct (LTE ('S ('S n))) x y)
inj1 LTE ('S ('S n)) x x
ZEQ LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  inj1 LTE ('S ('S n)) x x
ZEQ (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ LTE ('S m) a b
a)
  inj1 (SLT LTE ('S m) a b
a) LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 LTE ('S m) a b
a forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ)
  inj1 (SLT LTE ('S m) a b
a) (SLT LTE ('S m) a b
b) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 LTE ('S m) a b
a LTE ('S m) a b
b)
  inj2 :: forall (x :: Fin ('S ('S n))) (y :: Fin ('S ('S n))).
Obj (LTE ('S ('S n))) x
-> Obj (LTE ('S ('S n))) y
-> LTE ('S ('S n)) y (BinaryCoproduct (LTE ('S ('S n))) x y)
inj2 LTE ('S ('S n)) x x
ZEQ LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  inj2 LTE ('S ('S n)) x x
ZEQ (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ LTE ('S m) a b
a)
  inj2 (SLT LTE ('S m) a b
a) LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 LTE ('S m) a b
a forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ)
  inj2 (SLT LTE ('S m) a b
a) (SLT LTE ('S m) a b
b) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 LTE ('S m) a b
a LTE ('S m) a b
b)
  LTE ('S ('S n)) x a
ZEQ ||| :: forall (x :: Fin ('S ('S n))) (a :: Fin ('S ('S n)))
       (y :: Fin ('S ('S n))).
LTE ('S ('S n)) x a
-> LTE ('S ('S n)) y a
-> LTE ('S ('S n)) (BinaryCoproduct (LTE ('S ('S n))) x y) a
||| LTE ('S ('S n)) y a
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  ZLT LTE ('S m) 'FZ b
a ||| ZLT LTE ('S m) 'FZ b
b = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (case LTE ('S m) 'FZ b
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| LTE ('S m) 'FZ b
b of { LTE ('S m) (BinaryCoproduct (LTE ('S n)) 'FZ 'FZ) b
LTE ('S m) (BinaryCoproduct (LTE ('S m)) 'FZ 'FZ) b
ZEQ -> forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ; ZLT LTE ('S m) 'FZ b
n -> forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT LTE ('S m) 'FZ b
n })
  ZLT LTE ('S m) 'FZ b
a ||| SLT LTE ('S m) a b
b = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) 'FZ b
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| LTE ('S m) a b
b)
  SLT LTE ('S m) a b
a ||| ZLT LTE ('S m) 'FZ b
b = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| LTE ('S m) 'FZ b
b)
  SLT LTE ('S m) a b
a ||| SLT LTE ('S m) a b
b = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| LTE ('S m) a b
b)

instance HasBinaryProducts (LTE ('S 'Z)) where
  type BinaryProduct (LTE ('S 'Z)) 'FZ 'FZ = 'FZ
  proj1 :: forall (x :: Fin ('S 'Z)) (y :: Fin ('S 'Z)).
Obj (LTE ('S 'Z)) x
-> Obj (LTE ('S 'Z)) y
-> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) x y) x
proj1 LTE ('S 'Z) x x
ZEQ LTE ('S 'Z) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  proj2 :: forall (x :: Fin ('S 'Z)) (y :: Fin ('S 'Z)).
Obj (LTE ('S 'Z)) x
-> Obj (LTE ('S 'Z)) y
-> LTE ('S 'Z) (BinaryProduct (LTE ('S 'Z)) x y) y
proj2 LTE ('S 'Z) x x
ZEQ LTE ('S 'Z) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  LTE ('S 'Z) a x
ZEQ &&& :: forall (a :: Fin ('S 'Z)) (x :: Fin ('S 'Z)) (y :: Fin ('S 'Z)).
LTE ('S 'Z) a x
-> LTE ('S 'Z) a y
-> LTE ('S 'Z) a (BinaryProduct (LTE ('S 'Z)) x y)
&&& LTE ('S 'Z) a y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ

instance HasBinaryProducts (LTE ('S n)) => HasBinaryProducts (LTE ('S ('S n))) where
  type BinaryProduct (LTE ('S ('S n))) 'FZ 'FZ = 'FZ
  type BinaryProduct (LTE ('S ('S n))) 'FZ ('FS b) = 'FZ
  type BinaryProduct (LTE ('S ('S n))) ('FS a) 'FZ = 'FZ
  type BinaryProduct (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (BinaryProduct (LTE ('S n)) a b)
  proj1 :: forall (x :: Fin ('S ('S n))) (y :: Fin ('S ('S n))).
Obj (LTE ('S ('S n))) x
-> Obj (LTE ('S ('S n))) y
-> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) x y) x
proj1 LTE ('S ('S n)) x x
ZEQ LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  proj1 LTE ('S ('S n)) x x
ZEQ (SLT LTE ('S m) a b
_) = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  proj1 (SLT LTE ('S m) a b
a) LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (case forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 LTE ('S m) a b
a forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ of { LTE ('S m) (BinaryProduct (LTE ('S n)) a 'FZ) a
LTE ('S m) (BinaryProduct (LTE ('S m)) a 'FZ) a
ZEQ -> forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ; ZLT LTE ('S m) 'FZ b
n -> forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT LTE ('S m) 'FZ b
n })
  proj1 (SLT LTE ('S m) a b
a) (SLT LTE ('S m) a b
b) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 LTE ('S m) a b
a LTE ('S m) a b
b)
  proj2 :: forall (x :: Fin ('S ('S n))) (y :: Fin ('S ('S n))).
Obj (LTE ('S ('S n))) x
-> Obj (LTE ('S ('S n))) y
-> LTE ('S ('S n)) (BinaryProduct (LTE ('S ('S n))) x y) y
proj2 LTE ('S ('S n)) x x
ZEQ LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  proj2 LTE ('S ('S n)) x x
ZEQ (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (case forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ LTE ('S m) a b
a of { LTE ('S m) (BinaryProduct (LTE ('S n)) 'FZ a) a
LTE ('S m) (BinaryProduct (LTE ('S m)) 'FZ a) a
ZEQ -> forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ; ZLT LTE ('S m) 'FZ b
n -> forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT LTE ('S m) 'FZ b
n })
  proj2 (SLT LTE ('S m) a b
_) LTE ('S ('S n)) y y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  proj2 (SLT LTE ('S m) a b
a) (SLT LTE ('S m) a b
b) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 LTE ('S m) a b
a LTE ('S m) a b
b)
  LTE ('S ('S n)) a x
ZEQ &&& :: forall (a :: Fin ('S ('S n))) (x :: Fin ('S ('S n)))
       (y :: Fin ('S ('S n))).
LTE ('S ('S n)) a x
-> LTE ('S ('S n)) a y
-> LTE ('S ('S n)) a (BinaryProduct (LTE ('S ('S n))) x y)
&&& LTE ('S ('S n)) a y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  LTE ('S ('S n)) a x
ZEQ &&& ZLT LTE ('S m) 'FZ b
_ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  ZLT LTE ('S m) 'FZ b
_ &&& LTE ('S ('S n)) a y
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  ZLT LTE ('S m) 'FZ b
a &&& ZLT LTE ('S m) 'FZ b
b = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (LTE ('S m) 'FZ b
a forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& LTE ('S m) 'FZ b
b)
  SLT LTE ('S m) a b
a &&& SLT LTE ('S m) a b
b = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& LTE ('S m) a b
b)

data Proof a n where
  Proof :: (BinaryProduct (LTE ('S n)) 'FZ a ~ 'FZ, BinaryProduct (LTE ('S n)) a 'FZ ~ 'FZ) => Proof a n
proof :: Obj (LTE ('S n)) a -> Proof a n
proof :: forall (n :: Nat) (a :: Fin ('S n)).
Obj (LTE ('S n)) a -> Proof a n
proof = forall (n :: Nat) (a :: Fin ('S n)).
Obj (LTE ('S n)) a -> Proof a n
proof -- trust me

instance CartesianClosed (LTE ('S 'Z)) where
  type Exponential (LTE ('S 'Z)) 'FZ 'FZ = 'FZ
  apply :: forall (y :: Fin ('S 'Z)) (z :: Fin ('S 'Z)).
Obj (LTE ('S 'Z)) y
-> Obj (LTE ('S 'Z)) z
-> LTE
     ('S 'Z)
     (BinaryProduct (LTE ('S 'Z)) (Exponential (LTE ('S 'Z)) y z) y)
     z
apply LTE ('S 'Z) y y
ZEQ LTE ('S 'Z) z z
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  tuple :: forall (y :: Fin ('S 'Z)) (z :: Fin ('S 'Z)).
Obj (LTE ('S 'Z)) y
-> Obj (LTE ('S 'Z)) z
-> LTE
     ('S 'Z)
     z
     (Exponential (LTE ('S 'Z)) y (BinaryProduct (LTE ('S 'Z)) z y))
tuple LTE ('S 'Z) y y
ZEQ LTE ('S 'Z) z z
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  LTE ('S 'Z) z1 z2
ZEQ ^^^ :: forall (z1 :: Fin ('S 'Z)) (z2 :: Fin ('S 'Z)) (y2 :: Fin ('S 'Z))
       (y1 :: Fin ('S 'Z)).
LTE ('S 'Z) z1 z2
-> LTE ('S 'Z) y2 y1
-> LTE
     ('S 'Z)
     (Exponential (LTE ('S 'Z)) y1 z1)
     (Exponential (LTE ('S 'Z)) y2 z2)
^^^ LTE ('S 'Z) y2 y1
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ

-- b -> c = max(a: min(a, b) <= c)
-- → 0 1 2 3
--  +-------
-- 0|3 3 3 3
-- 1|0 3 3 3
-- 2|0 1 3 3
-- 3|0 1 2 3
instance CartesianClosed (LTE ('S n)) => CartesianClosed (LTE ('S ('S n))) where
  type Exponential (LTE ('S ('S n))) 'FZ 'FZ = 'FS (Exponential (LTE ('S n)) 'FZ 'FZ)
  type Exponential (LTE ('S ('S n))) 'FZ ('FS b) = 'FS (Exponential (LTE ('S n)) 'FZ b)
  type Exponential (LTE ('S ('S n))) ('FS a) 'FZ = 'FZ
  type Exponential (LTE ('S ('S n))) ('FS a) ('FS b) = 'FS (Exponential (LTE ('S n)) a b)
  apply :: forall (y :: Fin ('S ('S n))) (z :: Fin ('S ('S n))).
Obj (LTE ('S ('S n))) y
-> Obj (LTE ('S ('S n))) z
-> LTE
     ('S ('S n))
     (BinaryProduct
        (LTE ('S ('S n))) (Exponential (LTE ('S ('S n))) y z) y)
     z
apply LTE ('S ('S n)) y y
ZEQ LTE ('S ('S n)) z z
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  apply LTE ('S ('S n)) y y
ZEQ (SLT LTE ('S m) a b
a) = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (case forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ LTE ('S m) a b
a of { LTE
  ('S m)
  (BinaryProduct (LTE ('S n)) (Exponential (LTE ('S n)) 'FZ a) 'FZ)
  a
LTE
  ('S m)
  (BinaryProduct (LTE ('S m)) (Exponential (LTE ('S m)) 'FZ a) 'FZ)
  a
ZEQ -> forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ; ZLT LTE ('S m) 'FZ b
n -> forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT LTE ('S m) 'FZ b
n })
  apply (SLT LTE ('S m) a b
_) LTE ('S ('S n)) z z
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  apply (SLT LTE ('S m) a b
a) (SLT LTE ('S m) a b
b) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply LTE ('S m) a b
a LTE ('S m) a b
b)
  tuple :: forall (y :: Fin ('S ('S n))) (z :: Fin ('S ('S n))).
Obj (LTE ('S ('S n))) y
-> Obj (LTE ('S ('S n))) z
-> LTE
     ('S ('S n))
     z
     (Exponential
        (LTE ('S ('S n))) y (BinaryProduct (LTE ('S ('S n))) z y))
tuple LTE ('S ('S n)) y y
ZEQ LTE ('S ('S n)) z z
ZEQ = case forall (n :: Nat) (a :: Fin ('S n)).
Obj (LTE ('S n)) a -> Proof a n
proof (forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ @n) of Proof 'FZ n
Proof -> forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ)
  tuple LTE ('S ('S n)) y y
ZEQ (SLT LTE ('S m) a b
a) = case forall (n :: Nat) (a :: Fin ('S n)).
Obj (LTE ('S n)) a -> Proof a n
proof (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src LTE ('S m) a b
a) of Proof a m
Proof -> forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ LTE ('S m) a b
a)
  tuple (SLT LTE ('S m) a b
_) LTE ('S ('S n)) z z
ZEQ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  tuple (SLT LTE ('S m) a b
a) (SLT LTE ('S m) a b
b) = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall {k} (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple LTE ('S m) a b
a LTE ('S m) a b
b)
  LTE ('S ('S n)) z1 z2
ZEQ ^^^ :: forall (z1 :: Fin ('S ('S n))) (z2 :: Fin ('S ('S n)))
       (y2 :: Fin ('S ('S n))) (y1 :: Fin ('S ('S n))).
LTE ('S ('S n)) z1 z2
-> LTE ('S ('S n)) y2 y1
-> LTE
     ('S ('S n))
     (Exponential (LTE ('S ('S n))) y1 z1)
     (Exponential (LTE ('S ('S n))) y2 z2)
^^^ LTE ('S ('S n)) y2 y1
ZEQ = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ)
  LTE ('S ('S n)) z1 z2
ZEQ ^^^ ZLT LTE ('S m) 'FZ b
a = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt (forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ LTE ('S m) 'FZ b
a)))
  LTE ('S ('S n)) z1 z2
ZEQ ^^^ SLT LTE ('S m) a b
_ = forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ
  ZLT LTE ('S m) 'FZ b
a ^^^ LTE ('S ('S n)) y2 y1
ZEQ = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) 'FZ b
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ)
  ZLT LTE ('S m) 'FZ b
a ^^^ ZLT LTE ('S m) 'FZ b
b = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt (LTE ('S m) 'FZ b
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ LTE ('S m) 'FZ b
b)))
  ZLT LTE ('S m) 'FZ b
a ^^^ SLT LTE ('S m) a b
b = forall (m :: Nat) (b :: Fin ('S m)).
LTE ('S m) 'FZ b -> LTE ('S ('S m)) 'FZ ('FS b)
ZLT (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt (LTE ('S m) 'FZ b
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ LTE ('S m) a b
b)))
  SLT LTE ('S m) a b
a ^^^ LTE ('S ('S n)) y2 y1
ZEQ = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ forall (m :: Nat). LTE ('S m) 'FZ 'FZ
ZEQ)
  SLT LTE ('S m) a b
a ^^^ ZLT LTE ('S m) 'FZ b
b = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ LTE ('S m) 'FZ b
b)
  SLT LTE ('S m) a b
a ^^^ SLT LTE ('S m) a b
b = forall (m :: Nat) (b :: Fin ('S m)) (b :: Fin ('S m)).
LTE ('S m) b b -> LTE ('S ('S m)) ('FS b) ('FS b)
SLT (LTE ('S m) a b
a forall {k} (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ LTE ('S m) a b
b)