{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

{-# OPTIONS_GHC -Wall #-}

-- | Category of linear operation sequences

module ConCat.Chain where

import Prelude hiding (id,(.),curry,uncurry)

import ConCat.Misc ((:*))
import qualified ConCat.Category as C
import ConCat.AltCat

infixr 5 :<
data Chain :: (* -> * -> *) -> (* -> * -> *) where
  Nil  :: Ok  k a => Chain k a a
  (:<) :: Ok3 k a b c => a `k` b -> Chain k b c -> Chain k a c

-- mapChain :: forall j k.
--             (forall a b.       j a b ->       k a b)
--          -> (forall a b. Chain j a b -> Chain k a b)
-- mapChain f = go
--  where
--    go :: forall a b. Chain j a b -> Chain k a b
--    go Nil         = Nil
--    go (op :< ops) = f op :< go ops

evalChain :: Category k => Chain k a b -> a `k` b
evalChain :: forall (k :: * -> * -> *) a b. Category k => Chain k a b -> k a b
evalChain Chain k a b
Nil          = k a a
k a b
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
evalChain (k a b
op :< Chain k b b
rest) = Chain k b b -> k b b
forall (k :: * -> * -> *) a b. Category k => Chain k a b -> k a b
evalChain Chain k b b
rest k b b -> k a b -> k a b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a b
op

pureChain :: Ok2 k a b => a `k` b -> Chain k a b
pureChain :: forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k a b
f = k a b
f k a b -> Chain k b b -> Chain k a b
forall (k :: * -> * -> *) a b c.
Ok3 k a b c =>
k a b -> Chain k b c -> Chain k a c
:< Chain k b b
forall (k :: * -> * -> *) a. Ok k a => Chain k a a
Nil

toList :: forall k z a b. (forall u v. (u `k` v) -> z) -> Chain k a b -> [z]
toList :: forall (k :: * -> * -> *) z a b.
(forall u v. k u v -> z) -> Chain k a b -> [z]
toList forall u v. k u v -> z
f = Chain k a b -> [z]
forall p q. Chain k p q -> [z]
go
 where
   go :: Chain k p q -> [z]
   go :: forall p q. Chain k p q -> [z]
go Chain k p q
Nil         = []
   go (k p b
op :< Chain k b q
ops) = k p b -> z
forall u v. k u v -> z
f k p b
op z -> [z] -> [z]
forall a. a -> [a] -> [a]
: Chain k b q -> [z]
forall p q. Chain k p q -> [z]
go Chain k b q
ops

instance Show2 k => Show (Chain k a b) where
  show :: Chain k a b -> String
show = [Exists2 k] -> String
forall a. Show a => a -> String
show ([Exists2 k] -> String)
-> (Chain k a b -> [Exists2 k]) -> Chain k a b -> String
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (forall u v. k u v -> Exists2 k) -> Chain k a b -> [Exists2 k]
forall (k :: * -> * -> *) z a b.
(forall u v. k u v -> z) -> Chain k a b -> [z]
toList k u v -> Exists2 k
forall u v. k u v -> Exists2 k
forall (k :: * -> * -> *) a b. k a b -> Exists2 k
Exists2

instance Category (Chain k) where
  type Ok (Chain k) = Ok k
  id :: forall a. Ok (Chain k) a => Chain k a a
id  = Chain k a a
forall (k :: * -> * -> *) a. Ok k a => Chain k a a
Nil
  . :: forall b c a.
Ok3 (Chain k) a b c =>
Chain k b c -> Chain k a b -> Chain k a c
(.) = (Chain k a b -> Chain k b c -> Chain k a c)
-> Chain k b c -> Chain k a b -> Chain k a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Chain k a b -> Chain k b c -> Chain k a c
forall (k :: * -> * -> *) a b c.
Ok3 k a b c =>
Chain k a b -> Chain k b c -> Chain k a c
(++*)

infixr 5 ++*
(++*) :: Ok3 k a b c => Chain k a b -> Chain k b c -> Chain k a c
++* :: forall (k :: * -> * -> *) a b c.
Ok3 k a b c =>
Chain k a b -> Chain k b c -> Chain k a c
(++*) Chain k a b
Nil Chain k b c
ops          = Chain k a c
Chain k b c
ops
(++*) (k a b
op :< Chain k b b
ops) Chain k b c
ops' = k a b
op k a b -> Chain k b c -> Chain k a c
forall (k :: * -> * -> *) a b c.
Ok3 k a b c =>
k a b -> Chain k b c -> Chain k a c
:< (Chain k b b
ops Chain k b b -> Chain k b c -> Chain k b c
forall (k :: * -> * -> *) a b c.
Ok3 k a b c =>
Chain k a b -> Chain k b c -> Chain k a c
++* Chain k b c
ops')

-- We could reverse in toList or show instead of in (.)

instance AssociativePCat k => AssociativePCat (Chain k) where
  lassocP :: forall a b c. Ok3 k a b c => Chain k (a :* (b :* c)) ((a :* b) :* c)
  lassocP :: forall a b c.
Ok3 k a b c =>
Chain k (a :* (b :* c)) ((a :* b) :* c)
lassocP = k (a :* (b :* c)) ((a :* b) :* c)
-> Chain k (a :* (b :* c)) ((a :* b) :* c)
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k (a :* (b :* c)) ((a :* b) :* c)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP
          (Con (Sat (Ok k) (a :* (b :* c))) =>
 Chain k (a :* (b :* c)) ((a :* b) :* c))
-> ((Sat (Ok k) a && Sat (Ok k) (b :* c))
    |- Sat (Ok k) (a :* (b :* c)))
-> Chain k (a :* (b :* c)) ((a :* b) :* c)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @(b :* c) (Con (Sat (Ok k) (b :* c)) =>
 Chain k (a :* (b :* c)) ((a :* b) :* c))
-> ((Sat (Ok k) b && Sat (Ok k) c) |- Sat (Ok k) (b :* c))
-> Chain k (a :* (b :* c)) ((a :* b) :* c)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @c
          (Con (Sat (Ok k) ((a :* b) :* c)) =>
 Chain k (a :* (b :* c)) ((a :* b) :* c))
-> ((Sat (Ok k) (a :* b) && Sat (Ok k) c)
    |- Sat (Ok k) ((a :* b) :* c))
-> Chain k (a :* (b :* c)) ((a :* b) :* c)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a :* b) @c (Con (Sat (Ok k) (a :* b)) =>
 Chain k (a :* (b :* c)) ((a :* b) :* c))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> Chain k (a :* (b :* c)) ((a :* b) :* c)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
  rassocP :: forall a b c. Ok3 k a b c => Chain k ((a :* b) :* c) (a :* (b :* c))
  rassocP :: forall a b c.
Ok3 k a b c =>
Chain k ((a :* b) :* c) (a :* (b :* c))
rassocP = k ((a :* b) :* c) (a :* (b :* c))
-> Chain k ((a :* b) :* c) (a :* (b :* c))
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k ((a :* b) :* c) (a :* (b :* c))
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP
          (Con (Sat (Ok k) (a :* (b :* c))) =>
 Chain k ((a :* b) :* c) (a :* (b :* c)))
-> ((Sat (Ok k) a && Sat (Ok k) (b :* c))
    |- Sat (Ok k) (a :* (b :* c)))
-> Chain k ((a :* b) :* c) (a :* (b :* c))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @(b :* c) (Con (Sat (Ok k) (b :* c)) =>
 Chain k ((a :* b) :* c) (a :* (b :* c)))
-> ((Sat (Ok k) b && Sat (Ok k) c) |- Sat (Ok k) (b :* c))
-> Chain k ((a :* b) :* c) (a :* (b :* c))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @c
          (Con (Sat (Ok k) ((a :* b) :* c)) =>
 Chain k ((a :* b) :* c) (a :* (b :* c)))
-> ((Sat (Ok k) (a :* b) && Sat (Ok k) c)
    |- Sat (Ok k) ((a :* b) :* c))
-> Chain k ((a :* b) :* c) (a :* (b :* c))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @(a :* b) @c (Con (Sat (Ok k) (a :* b)) =>
 Chain k ((a :* b) :* c) (a :* (b :* c)))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> Chain k ((a :* b) :* c) (a :* (b :* c))
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b

instance BraidedPCat k => BraidedPCat (Chain k) where
  swapP :: forall a b. Ok2 k a b => Chain k (a :* b) (b :* a)
  swapP :: forall a b. Ok2 k a b => Chain k (a :* b) (b :* a)
swapP = k (a :* b) (b :* a)
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP k (a :* b) (b :* a)
-> Chain k (b :* a) (b :* a) -> Chain k (a :* b) (b :* a)
forall (k :: * -> * -> *) a b c.
Ok3 k a b c =>
k a b -> Chain k b c -> Chain k a c
:< Chain k (b :* a) (b :* a)
forall (k :: * -> * -> *) a. Ok k a => Chain k a a
Nil
    (Con (Sat (Ok k) (a :* b)) => Chain k (a :* b) (b :* a))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> Chain k (a :* b) (b :* a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b (Con (Sat (Ok k) (b :* a)) => Chain k (a :* b) (b :* a))
-> ((Sat (Ok k) b && Sat (Ok k) a) |- Sat (Ok k) (b :* a))
-> Chain k (a :* b) (b :* a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @b @a

instance ProductCat k => ProductCat (Chain k) where
  exl :: forall a b. Ok2 k a b => Chain k (a :* b) a
  exr :: forall a b. Ok2 k a b => Chain k (a :* b) b
  dup :: forall a  . Ok  k a   => Chain k a (a :* a)
  exl :: forall a b. Ok2 k a b => Chain k (a :* b) a
exl = k (a :* b) a -> Chain k (a :* b) a
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k (a :* b) a
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl (Con (Sat (Ok k) (a :* b)) => Chain k (a :* b) a)
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> Chain k (a :* b) a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
  exr :: forall a b. Ok2 k a b => Chain k (a :* b) b
exr = k (a :* b) b -> Chain k (a :* b) b
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k (a :* b) b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr (Con (Sat (Ok k) (a :* b)) => Chain k (a :* b) b)
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> Chain k (a :* b) b
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
  dup :: forall a. Ok k a => Chain k a (a :* a)
dup = k a (a :* a) -> Chain k a (a :* a)
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k a (a :* a)
forall (k :: * -> * -> *) a.
(ProductCat k, Ok k a) =>
k a (Prod k a a)
dup (Con (Sat (Ok k) (a :* a)) => Chain k a (a :* a))
-> ((Sat (Ok k) a && Sat (Ok k) a) |- Sat (Ok k) (a :* a))
-> Chain k a (a :* a)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @a

instance (MonoidalPCat k, BraidedPCat k) => MonoidalPCat (Chain k) where
  first :: forall a b c. Ok3 k a b c => Chain k a c -> Chain k (a :* b) (c :* b)
  first :: forall a b c.
Ok3 k a b c =>
Chain k a c -> Chain k (a :* b) (c :* b)
first Chain k a c
Nil = Chain k (a :* b) (a :* b)
Chain k (a :* b) (c, b)
Con (Sat (Ok k) (a :* b)) => Chain k (a :* b) (c, b)
forall (k :: * -> * -> *) a. Ok k a => Chain k a a
Nil (Con (Sat (Ok k) (a :* b)) => Chain k (a :* b) (c, b))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> Chain k (a :* b) (c, b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b
  first (k a b
op :< Chain k b c
ops) = k a b -> Chain k b c -> Chain k (a :* b) (c, b)
forall x. Ok k x => k a x -> Chain k x c -> Chain k (a :* b) (c, b)
firstCons k a b
op Chain k b c
ops
   where
     firstCons :: forall x. Ok k x => (a `k` x) -> Chain k x c -> Chain k (a :* b) (c :* b)
     firstCons :: forall x. Ok k x => k a x -> Chain k x c -> Chain k (a :* b) (c, b)
firstCons k a x
f Chain k x c
fs = k a x -> k (a :* b) (x :* b)
forall (k :: * -> * -> *) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first k a x
f k (a :* b) (x :* b)
-> Chain k (x :* b) (c, b) -> Chain k (a :* b) (c, b)
forall (k :: * -> * -> *) a b c.
Ok3 k a b c =>
k a b -> Chain k b c -> Chain k a c
:< Chain k x c -> Chain k (x :* b) (c, b)
forall (k :: * -> * -> *) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first Chain k x c
fs
       (Con (Sat (Ok k) (a :* b)) => Chain k (a :* b) (c, b))
-> ((Sat (Ok k) a && Sat (Ok k) b) |- Sat (Ok k) (a :* b))
-> Chain k (a :* b) (c, b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @b (Con (Sat (Ok k) (c, b)) => Chain k (a :* b) (c, b))
-> ((Sat (Ok k) c && Sat (Ok k) b) |- Sat (Ok k) (c, b))
-> Chain k (a :* b) (c, b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @c @b (Con (Sat (Ok k) (x :* b)) => Chain k (a :* b) (c, b))
-> ((Sat (Ok k) x && Sat (Ok k) b) |- Sat (Ok k) (x :* b))
-> Chain k (a :* b) (c, b)
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @x @b
  second :: forall a b b'.
Ok3 (Chain k) a b b' =>
Chain k b b' -> Chain k (Prod (Chain k) a b) (Prod (Chain k) a b')
second = Chain k b b' -> Chain k (a :* b) (a :* b')
forall (k :: * -> * -> *) a b d.
(MonoidalPCat k, BraidedPCat k, Ok3 k a b d) =>
k b d -> k (a :* b) (a :* d)
secondFirst
  *** :: forall a b c d.
Ok4 (Chain k) a b c d =>
Chain k a c
-> Chain k b d -> Chain k (Prod (Chain k) a b) (Prod (Chain k) c d)
(***) = Chain k a c -> Chain k b d -> Chain k (a :* b) (c :* d)
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (a :* b) (c :* d)
crossSecondFirst

instance TerminalCat k => TerminalCat (Chain k) where
  it :: forall a. Ok (Chain k) a => Chain k a (Unit (Chain k))
it = k a (Unit (Chain k)) -> Chain k a (Unit (Chain k))
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k a (Unit (Chain k))
forall (k :: * -> * -> *) a.
(TerminalCat k, Ok k a) =>
k a (Unit (Chain k))
it

instance (BraidedPCat k, MProductCat k, TerminalCat k) => UnitCat (Chain k)
  
instance (OkProd k, NumCat k a) => NumCat (Chain k) a where
  negateC :: Chain k a a
negateC = k a a -> Chain k a a
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k a a
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC
  addC :: Chain k (Prod (Chain k) a a) a
addC  = k (Prod (Chain k) a a) a -> Chain k (Prod (Chain k) a a) a
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k (Prod (Chain k) a a) a
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
addC  (Con (Sat (Ok k) (Prod (Chain k) a a)) =>
 Chain k (Prod (Chain k) a a) a)
-> ((Sat (Ok k) a && Sat (Ok k) a)
    |- Sat (Ok k) (Prod (Chain k) a a))
-> Chain k (Prod (Chain k) a a) a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @a
  subC :: Chain k (Prod (Chain k) a a) a
subC  = k (Prod (Chain k) a a) a -> Chain k (Prod (Chain k) a a) a
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k (Prod (Chain k) a a) a
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
subC  (Con (Sat (Ok k) (Prod (Chain k) a a)) =>
 Chain k (Prod (Chain k) a a) a)
-> ((Sat (Ok k) a && Sat (Ok k) a)
    |- Sat (Ok k) (Prod (Chain k) a a))
-> Chain k (Prod (Chain k) a a) a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @a
  mulC :: Chain k (Prod (Chain k) a a) a
mulC  = k (Prod (Chain k) a a) a -> Chain k (Prod (Chain k) a a) a
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k (Prod (Chain k) a a) a
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
mulC  (Con (Sat (Ok k) (Prod (Chain k) a a)) =>
 Chain k (Prod (Chain k) a a) a)
-> ((Sat (Ok k) a && Sat (Ok k) a)
    |- Sat (Ok k) (Prod (Chain k) a a))
-> Chain k (Prod (Chain k) a a) a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @a
  powIC :: Ok (Chain k) Int => Chain k (Prod (Chain k) a Int) a
powIC = k (Prod (Chain k) a Int) a -> Chain k (Prod (Chain k) a Int) a
forall (k :: * -> * -> *) a b. Ok2 k a b => k a b -> Chain k a b
pureChain k (Prod (Chain k) a Int) a
forall (k :: * -> * -> *) a.
(NumCat k a, Ok k Int) =>
k (Prod k a Int) a
powIC (Con (Sat (Ok k) (Prod (Chain k) a Int)) =>
 Chain k (Prod (Chain k) a Int) a)
-> ((Sat (Ok k) a && Sat (Ok k) Int)
    |- Sat (Ok k) (Prod (Chain k) a Int))
-> Chain k (Prod (Chain k) a Int) a
forall a b r. Con a => (Con b => r) -> (a |- b) -> r
<+ forall (k :: * -> * -> *) a b.
OkProd k =>
(Ok' k a && Ok' k b) |- Ok' k (Prod k a b)
okProd @k @a @Int

-- TODO: Many more instances

{--------------------------------------------------------------------
    Miscellany
--------------------------------------------------------------------}

data Exists2 k = forall a b. Exists2 (a `k` b)

instance Show2 k => Show (Exists2 k) where show :: Exists2 k -> String
show (Exists2 k a b
f) = k a b -> String
forall a b. k a b -> String
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (b :: k1).
Show2 k2 =>
k2 a b -> String
show2 k a b
f