{-# LANGUAGE AllowAmbiguousTypes #-}

-- | The free bicartesian closed category on a generating profunctor @p@.
--
-- Unlike "Proarrow.Category.Instance.Free" (which is generic over an arbitrary /list/ of
-- structures), this is hardcoded to exactly the BiCCC signature, to simplify the implementation.
module Proarrow.Category.Instance.FreeBiCCC
  ( FBC (..)
  , Term (..)
  , Lower
  , interp
  , KnownFBCOb (fbcCase)
  , fbcOb
  ) where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (BiCCC, Closed (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, type (+->))
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Limit.Terminal (HasTerminalObject (..))

-- | Object expressions of the free BiCCC on generators @p@: base objects (@OBJ@, carrying an
-- actual object of @k@ — the category @p@'s generating morphisms are themselves between),
-- plus terminal\/initial objects and products, coproducts and exponentials of
-- sub-expressions.
type data FBC (p :: k +-> k)
  = OBJ k
  | UNIT
  | PROD (FBC p) (FBC p)
  | ZERO
  | SUM (FBC p) (FBC p)
  | EXPO (FBC p) (FBC p)

-- | Interpret an object expression as the object of @k@ it denotes.
type family Lower (a :: FBC p) :: k where
  Lower (OBJ x) = x
  Lower UNIT = TerminalObject
  Lower (PROD a b) = Lower a && Lower b
  Lower ZERO = InitialObject
  Lower (SUM a b) = Lower a || Lower b
  Lower (EXPO a b) = Lower a ~~> Lower b

-- | A term of the free BiCCC: one constructor per operation, including composition itself.
-- No smart constructors, no normal forms — e.g. @Compose Id f@ and @f@ are different 'Term's
-- that happen to interpret to the same morphism. @p@ (and the base category @k@ it's a
-- profunctor on) is carried purely by the kind of @a@/@b@ (@FBC p@), the same way
-- "Proarrow.Category.Instance.Free"'s @Free@ carries its generating profunctor, so it doesn't
-- need to be an explicit parameter of 'Term' itself.
type Term :: CAT (FBC p)
data Term a b where
  Id :: (Ob a) => Term a a
  Compose :: Term b c -> Term a b -> Term a c
  Emb :: (Ob x, Ob y) => p x y -> Term (OBJ x :: FBC p) (OBJ y)
  Terminate :: (Ob a) => Term a UNIT
  Absurd :: (Ob a) => Term ZERO a
  Fst :: (Ob a, Ob b) => Term (PROD a b) a
  Snd :: (Ob a, Ob b) => Term (PROD a b) b
  Pair :: Term c a -> Term c b -> Term c (PROD a b)
  Inl :: (Ob a, Ob b) => Term a (SUM a b)
  Inr :: (Ob a, Ob b) => Term b (SUM a b)
  Case :: Term a c -> Term b c -> Term (SUM a b) c
  Curry :: (Ob a, Ob b) => Term (PROD a b) c -> Term a (EXPO b c)
  Apply :: (Ob a, Ob b) => Term (PROD (EXPO a b) a) b

instance forall k (p :: k +-> k). (BiCCC k) => Profunctor (Term :: CAT (FBC p)) where
  dimap :: forall (c :: FBC p) (a :: FBC p) (b :: FBC p) (d :: FBC p).
(c ~> a) -> (b ~> d) -> Term a b -> Term c d
dimap = (c ~> a) -> (b ~> d) -> Term a b -> Term c d
Term c a -> Term b d -> Term a b -> Term 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 :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term a b
Id = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Compose Term b b
g Term a b
f = r
(Ob a, Ob b) => r
(Ob b, Ob b) => r
r ((Ob b, Ob b) => r) -> Term b b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term b b
g ((Ob a, Ob b) => r) -> Term a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term a b
f
  (Ob a, Ob b) => r
r \\ Emb p x y
_ = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Term a b
Terminate = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ Term a b
Absurd = r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ (Fst @a @b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(Lower a) @(Lower b) r
Ob (Lower b && Lower b) => r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ (Snd @a @b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(Lower a) @(Lower b) r
Ob (Lower a && Lower b) => r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ (Pair @_ @a @b Term a a
f Term a b
g) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(Lower a) @(Lower b) r
Ob (Lower a && Lower b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob a) => r) -> Term a a -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term a a
f ((Ob a, Ob b) => r) -> Term a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term a b
g
  (Ob a, Ob b) => r
r \\ (Inl @a @b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(Lower a) @(Lower b) r
Ob (Lower a || Lower b) => r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ (Inr @a @b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(Lower a) @(Lower b) r
Ob (Lower a || Lower a) => r
(Ob a, Ob b) => r
r
  (Ob a, Ob b) => r
r \\ (Case @a @_ @b Term a b
f Term b b
g) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(Lower a) @(Lower b) r
Ob (Lower a || Lower b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> Term a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term a b
f ((Ob b, Ob b) => r) -> Term b b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term b b
g
  (Ob a, Ob b) => r
r \\ (Curry @_ @b @c Term (PROD a b) c
f) = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(Lower b) @(Lower c) r
Ob (Lower b ~~> Lower c) => r
(Ob a, Ob b) => r
r ((Ob (PROD a b), Ob c) => r) -> Term (PROD a b) c -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ Term (PROD a b) c
f
  (Ob a, Ob b) => r
r \\ (Apply @a @b) = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(Lower a) @(Lower b) (forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(Lower a ~~> Lower b) @(Lower a) r
Ob ((Lower a ~~> Lower b) && Lower a) => r
(Ob a, Ob b) => r
r)

instance forall k (p :: k +-> k). (BiCCC k) => Promonad (Term :: CAT (FBC p)) where
  id :: forall (a :: FBC p). Ob a => Term a a
id = Term a a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Id
  . :: forall (b :: FBC p) (c :: FBC p) (a :: FBC p).
Term b c -> Term a b -> Term a c
(.) = Term b c -> Term a b -> Term a c
forall {k} {p :: k +-> k} (a :: FBC p) (c :: FBC p) (a :: FBC p).
Term a c -> Term a a -> Term a c
Compose
instance forall k (p :: k +-> k). (BiCCC k) => CategoryOf (FBC p) where
  type (~>) = Term
  type Ob (a :: FBC (p :: k +-> k)) = (Ob (Lower a :: k), KnownFBCOb a)

-- | Witnesses that an object expression is well-formed by case analysis on its shape.
type KnownFBCOb :: forall {k} {p :: k +-> k}. FBC p -> Constraint
class KnownFBCOb (a :: FBC (p :: k +-> k)) where
  fbcCase
    :: (forall x. (a ~ OBJ x, Ob (x :: k)) => r)
    -> ((a ~ UNIT) => r)
    -> (forall x y. (a ~ PROD x y, Ob x, Ob y) => r)
    -> ((a ~ ZERO) => r)
    -> (forall x y. (a ~ SUM x y, Ob x, Ob y) => r)
    -> (forall x y. (a ~ EXPO x y, Ob x, Ob y) => r)
    -> r

instance (Ob x) => KnownFBCOb (OBJ x :: FBC p) where
  fbcCase :: forall r.
(forall (x :: k). (OBJ x ~ OBJ x, Ob x) => r)
-> ((OBJ x ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (OBJ x ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((OBJ x ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (OBJ x ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (OBJ x ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase forall (x :: k). (OBJ x ~ OBJ x, Ob x) => r
o (OBJ x ~ UNIT) => r
_ forall (x :: FBC p) (y :: FBC p).
(OBJ x ~ PROD x y, Ob x, Ob y) =>
r
_ (OBJ x ~ ZERO) => r
_ forall (x :: FBC p) (y :: FBC p).
(OBJ x ~ SUM x y, Ob x, Ob y) =>
r
_ forall (x :: FBC p) (y :: FBC p).
(OBJ x ~ EXPO x y, Ob x, Ob y) =>
r
_ = r
forall (x :: k). (OBJ x ~ OBJ x, Ob x) => r
o

instance forall k (p :: k +-> k). (BiCCC k) => KnownFBCOb (UNIT :: FBC p) where
  fbcCase :: forall r.
(forall (x :: k). (UNIT ~ OBJ x, Ob x) => r)
-> ((UNIT ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (UNIT ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((UNIT ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (UNIT ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (UNIT ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase forall (x :: k). (UNIT ~ OBJ x, Ob x) => r
_ (UNIT ~ UNIT) => r
u forall (x :: FBC p) (y :: FBC p).
(UNIT ~ PROD x y, Ob x, Ob y) =>
r
_ (UNIT ~ ZERO) => r
_ forall (x :: FBC p) (y :: FBC p). (UNIT ~ SUM x y, Ob x, Ob y) => r
_ forall (x :: FBC p) (y :: FBC p).
(UNIT ~ EXPO x y, Ob x, Ob y) =>
r
_ = r
(UNIT ~ UNIT) => r
u

instance forall k (p :: k +-> k). (BiCCC k) => KnownFBCOb (ZERO :: FBC p) where
  fbcCase :: forall r.
(forall (x :: k). (ZERO ~ OBJ x, Ob x) => r)
-> ((ZERO ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (ZERO ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((ZERO ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (ZERO ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (ZERO ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase forall (x :: k). (ZERO ~ OBJ x, Ob x) => r
_ (ZERO ~ UNIT) => r
_ forall (x :: FBC p) (y :: FBC p).
(ZERO ~ PROD x y, Ob x, Ob y) =>
r
_ (ZERO ~ ZERO) => r
z forall (x :: FBC p) (y :: FBC p). (ZERO ~ SUM x y, Ob x, Ob y) => r
_ forall (x :: FBC p) (y :: FBC p).
(ZERO ~ EXPO x y, Ob x, Ob y) =>
r
_ = r
(ZERO ~ ZERO) => r
z

instance forall k (p :: k +-> k) a b. (BiCCC k, KnownFBCOb (a :: FBC p), KnownFBCOb b) => KnownFBCOb (PROD a b) where
  fbcCase :: forall r.
(forall (x :: k). (PROD a b ~ OBJ x, Ob x) => r)
-> ((PROD a b ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (PROD a b ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((PROD a b ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (PROD a b ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (PROD a b ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase forall (x :: k). (PROD a b ~ OBJ x, Ob x) => r
_ (PROD a b ~ UNIT) => r
_ forall (x :: FBC p) (y :: FBC p).
(PROD a b ~ PROD x y, Ob x, Ob y) =>
r
prod (PROD a b ~ ZERO) => r
_ forall (x :: FBC p) (y :: FBC p).
(PROD a b ~ SUM x y, Ob x, Ob y) =>
r
_ forall (x :: FBC p) (y :: FBC p).
(PROD a b ~ EXPO x y, Ob x, Ob y) =>
r
_ = forall {k} {p :: k +-> k} (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
forall (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
withLowerOb @a (forall {k} {p :: k +-> k} (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
forall (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
withLowerOb @b r
Ob (Lower b) => r
forall (x :: FBC p) (y :: FBC p).
(PROD a b ~ PROD x y, Ob x, Ob y) =>
r
prod)

instance forall k (p :: k +-> k) a b. (BiCCC k, KnownFBCOb (a :: FBC p), KnownFBCOb b) => KnownFBCOb (SUM a b) where
  fbcCase :: forall r.
(forall (x :: k). (SUM a b ~ OBJ x, Ob x) => r)
-> ((SUM a b ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (SUM a b ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((SUM a b ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (SUM a b ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (SUM a b ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase forall (x :: k). (SUM a b ~ OBJ x, Ob x) => r
_ (SUM a b ~ UNIT) => r
_ forall (x :: FBC p) (y :: FBC p).
(SUM a b ~ PROD x y, Ob x, Ob y) =>
r
_ (SUM a b ~ ZERO) => r
_ forall (x :: FBC p) (y :: FBC p).
(SUM a b ~ SUM x y, Ob x, Ob y) =>
r
sm forall (x :: FBC p) (y :: FBC p).
(SUM a b ~ EXPO x y, Ob x, Ob y) =>
r
_ = forall {k} {p :: k +-> k} (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
forall (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
withLowerOb @a (forall {k} {p :: k +-> k} (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
forall (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
withLowerOb @b r
Ob (Lower b) => r
forall (x :: FBC p) (y :: FBC p).
(SUM a b ~ SUM x y, Ob x, Ob y) =>
r
sm)

instance forall k (p :: k +-> k) a b. (BiCCC k, KnownFBCOb (a :: FBC p), KnownFBCOb b) => KnownFBCOb (EXPO a b) where
  fbcCase :: forall r.
(forall (x :: k). (EXPO a b ~ OBJ x, Ob x) => r)
-> ((EXPO a b ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (EXPO a b ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((EXPO a b ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (EXPO a b ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (EXPO a b ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase forall (x :: k). (EXPO a b ~ OBJ x, Ob x) => r
_ (EXPO a b ~ UNIT) => r
_ forall (x :: FBC p) (y :: FBC p).
(EXPO a b ~ PROD x y, Ob x, Ob y) =>
r
_ (EXPO a b ~ ZERO) => r
_ forall (x :: FBC p) (y :: FBC p).
(EXPO a b ~ SUM x y, Ob x, Ob y) =>
r
_ forall (x :: FBC p) (y :: FBC p).
(EXPO a b ~ EXPO x y, Ob x, Ob y) =>
r
ex = forall {k} {p :: k +-> k} (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
forall (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
withLowerOb @a (forall {k} {p :: k +-> k} (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
forall (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
withLowerOb @b r
Ob (Lower b) => r
forall (x :: FBC p) (y :: FBC p).
(EXPO a b ~ EXPO x y, Ob x, Ob y) =>
r
ex)

-- | Recover 'Ob' of the /interpreted/ shape (needed to call @k@'s own 'withObProd'\/
-- 'withObCoprod'\/'withObExp') from only the /leaves'/ 'Ob', by case analysis via 'fbcCase' —
-- deliberately weaker than requiring the already-bundled, full 'Ob' of the sub-shapes, since
-- that would make it impossible to ever construct in the first place (needing 'Ob' of a
-- compound shape to construct 'Ob' of a bigger compound shape containing it).
withLowerOb :: forall {k} {p :: k +-> k} a r. (BiCCC k, KnownFBCOb (a :: FBC p)) => ((Ob (Lower a :: k)) => r) -> r
withLowerOb :: forall {k} {p :: k +-> k} (a :: FBC p) r.
(BiCCC k, KnownFBCOb a) =>
(Ob (Lower a) => r) -> r
withLowerOb Ob (Lower a) => r
r =
  forall {k} {p :: k +-> k} (a :: FBC p) r.
KnownFBCOb a =>
(forall (x :: k). (a ~ OBJ x, Ob x) => r)
-> ((a ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((a ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
forall (a :: FBC p) r.
KnownFBCOb a =>
(forall (x :: k). (a ~ OBJ x, Ob x) => r)
-> ((a ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((a ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase @a
    r
Ob (Lower a) => r
forall (x :: k). (a ~ OBJ x, Ob x) => r
r
    r
(a ~ UNIT) => r
Ob (Lower a) => r
r
    (\ @x @y -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @(Lower x) @(Lower y) r
Ob (Lower x && Lower y) => r
Ob (Lower a) => r
r)
    r
(a ~ ZERO) => r
Ob (Lower a) => r
r
    (\ @x @y -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @(Lower x) @(Lower y) r
Ob (Lower x || Lower y) => r
Ob (Lower a) => r
r)
    (\ @x @y -> forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(Lower x) @(Lower y) r
Ob (Lower x ~~> Lower y) => r
Ob (Lower a) => r
r)

-- | The identity morphism on @a@, recovered by case analysis via 'fbcCase' — the only place
-- 'KnownFBCOb' is needed once it's bundled into 'Ob' (see 'CategoryOf' above): everywhere else,
-- an 'Ob' proof in hand is already enough, and 'Proarrow.Object.obj' gives the identity directly.
fbcOb :: forall {k} {p :: k +-> k} a. (BiCCC k, KnownFBCOb (a :: FBC p)) => Term a a
fbcOb :: forall {k} {p :: k +-> k} (a :: FBC p).
(BiCCC k, KnownFBCOb a) =>
Term a a
fbcOb =
  forall {k} {p :: k +-> k} (a :: FBC p) r.
KnownFBCOb a =>
(forall (x :: k). (a ~ OBJ x, Ob x) => r)
-> ((a ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((a ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
forall (a :: FBC p) r.
KnownFBCOb a =>
(forall (x :: k). (a ~ OBJ x, Ob x) => r)
-> ((a ~ UNIT) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ PROD x y, Ob x, Ob y) =>
    r)
-> ((a ~ ZERO) => r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ SUM x y, Ob x, Ob y) =>
    r)
-> (forall (x :: FBC p) (y :: FBC p).
    (a ~ EXPO x y, Ob x, Ob y) =>
    r)
-> r
fbcCase @a
    Term a a
forall (x :: k). (a ~ OBJ x, Ob x) => Term a a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Id
    Term a a
(a ~ UNIT) => Term a a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Id
    (\ @x @y -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(FBC p) @x @y Term a a
Ob (x && y) => Term a a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Id)
    Term a a
(a ~ ZERO) => Term a a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Id
    (\ @x @y -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(FBC p) @x @y Term a a
Ob (x || y) => Term a a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Id)
    (\ @x @y -> forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @(FBC p) @x @y Term a a
Ob (x ~~> y) => Term a a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a a
Id)

instance forall k (p :: k +-> k). (BiCCC k) => HasTerminalObject (FBC p) where
  type TerminalObject = UNIT
  terminate :: forall (a :: FBC p). Ob a => a ~> TerminalObject
terminate = a ~> TerminalObject
Term a UNIT
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term a UNIT
Terminate
instance forall k (p :: k +-> k). (BiCCC k) => HasInitialObject (FBC p) where
  type InitialObject = ZERO
  initiate :: forall (a :: FBC p). Ob a => InitialObject ~> a
initiate = InitialObject ~> a
Term ZERO a
forall {k} {p :: k +-> k} (a :: FBC p). Ob a => Term ZERO a
Absurd

instance forall k (p :: k +-> k). (BiCCC k) => HasBinaryProducts (FBC p) where
  type a && b = PROD a b
  withObProd :: forall (a :: FBC p) (b :: FBC p) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @a @b Ob (a && b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @(Lower a) @(Lower b) r
Ob (Lower a && Lower b) => r
Ob (a && b) => r
r
  fst :: forall (a :: FBC p) (b :: FBC p). (Ob a, Ob b) => (a && b) ~> a
fst = (a && b) ~> a
Term (PROD a b) a
forall {k} {p :: k +-> k} (a :: FBC p) (a :: FBC p).
(Ob a, Ob a) =>
Term (PROD a a) a
Fst
  snd :: forall (a :: FBC p) (b :: FBC p). (Ob a, Ob b) => (a && b) ~> b
snd = (a && b) ~> b
Term (PROD a b) b
forall {k} {p :: k +-> k} (a :: FBC p) (b :: FBC p).
(Ob a, Ob b) =>
Term (PROD a b) b
Snd
  a ~> x
f &&& :: forall (a :: FBC p) (x :: FBC p) (y :: FBC p).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a ~> y
g = Term a x -> Term a y -> Term a (PROD x y)
forall {k} {p :: k +-> k} (c :: FBC p) (a :: FBC p) (c :: FBC p).
Term c a -> Term c c -> Term c (PROD a c)
Pair a ~> x
Term a x
f a ~> y
Term a y
g ((Ob a, Ob x) => Term a (PROD x y))
-> Term a x -> Term a (PROD x y)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ a ~> x
Term a x
f

instance forall k (p :: k +-> k). (BiCCC k) => HasBinaryCoproducts (FBC p) where
  type a || b = SUM a b
  withObCoprod :: forall (a :: FBC p) (b :: FBC p) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @a @b Ob (a || b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @(Lower a) @(Lower b) r
Ob (Lower a || Lower b) => r
Ob (a || b) => r
r
  lft :: forall (a :: FBC p) (b :: FBC p). (Ob a, Ob b) => a ~> (a || b)
lft = a ~> (a || b)
Term a (SUM a b)
forall {k} {p :: k +-> k} (a :: FBC p) (a :: FBC p).
(Ob a, Ob a) =>
Term a (SUM a a)
Inl
  rgt :: forall (a :: FBC p) (b :: FBC p). (Ob a, Ob b) => b ~> (a || b)
rgt = b ~> (a || b)
Term b (SUM a b)
forall {k} {p :: k +-> k} (a :: FBC p) (b :: FBC p).
(Ob a, Ob b) =>
Term b (SUM a b)
Inr
  x ~> a
f ||| :: forall (x :: FBC p) (a :: FBC p) (y :: FBC p).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
g = Term x a -> Term y a -> Term (SUM x y) a
forall {k} {p :: k +-> k} (a :: FBC p) (c :: FBC p) (c :: FBC p).
Term a c -> Term c c -> Term (SUM a c) c
Case x ~> a
Term x a
f y ~> a
Term y a
g ((Ob x, Ob a) => Term (SUM x y) a) -> Term x a -> Term (SUM x y) a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FBC p) (b :: FBC p) r.
((Ob a, Ob b) => r) -> Term a b -> r
\\ x ~> a
Term x a
f

instance forall k (p :: k +-> k). (BiCCC k) => MonoidalProfunctor (Term :: CAT (FBC p)) where
  one :: Term Unit Unit
one = Term Unit Unit
Term UNIT UNIT
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FBC p). Ob a => Term a a
id
  ** :: forall (x1 :: FBC p) (x2 :: FBC p) (y1 :: FBC p) (y2 :: FBC p).
Term x1 x2 -> Term y1 y2 -> Term (x1 ** y1) (x2 ** y2)
(**) = (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
Term x1 x2 -> Term y1 y2 -> Term (x1 ** y1) (x2 ** y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: FBC p) (b :: FBC p) (x :: FBC p) (y :: FBC p).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
(***)
instance forall k (p :: k +-> k). (BiCCC k) => Monoidal (FBC p) where
  type a ** b = a && b
  type Unit = TerminalObject
  withOb2 :: forall (a :: FBC p) (b :: FBC p) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a @b
  leftUnitor :: forall (a :: FBC p). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && a) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: FBC p). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
a ~> (TerminalObject && a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: FBC p). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(a && TerminalObject) ~> a
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: FBC p). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
a ~> (a && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: FBC p) (b :: FBC p) (c :: FBC p).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall (a :: FBC p) (b :: FBC p) (c :: FBC p).
(HasProducts (FBC p), Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c
  associatorInv :: forall (a :: FBC p) (b :: FBC p) (c :: FBC p).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall (a :: FBC p) (b :: FBC p) (c :: FBC p).
(HasProducts (FBC p), Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c
instance forall k (p :: k +-> k). (BiCCC k) => SymMonoidal (FBC p) where
  swap :: forall (a :: FBC p) (b :: FBC p).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b = forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall (a :: FBC p) (b :: FBC p).
(HasBinaryProducts (FBC p), Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @b

instance forall k (p :: k +-> k). (BiCCC k) => Closed (FBC p) where
  type a ~~> b = EXPO a b
  withObExp :: forall (a :: FBC p) (b :: FBC p) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @a @b Ob (a ~~> b) => r
r = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @(Lower a) @(Lower b) r
Ob (Lower a ~~> Lower b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: FBC p) (b :: FBC p) (c :: FBC p).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry = ((a ** b) ~> c) -> a ~> (b ~~> c)
Term (PROD a b) c -> Term a (EXPO b c)
forall {k} {p :: k +-> k} (a :: FBC p) (a :: FBC p) (c :: FBC p).
(Ob a, Ob a) =>
Term (PROD a a) c -> Term a (EXPO a c)
Curry
  apply :: forall (a :: FBC p) (b :: FBC p).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = ((a ~~> b) ** a) ~> b
Term (PROD (EXPO a b) a) b
forall {k} {p :: k +-> k} (a :: FBC p) (b :: FBC p).
(Ob a, Ob b) =>
Term (PROD (EXPO a b) a) b
Apply

-- | Interpret a 'Term' as the morphism of @k@ it denotes, given an interpretation of the
-- generators, provided @k@ is itself a BiCCC. This is the one place a 'Term''s meaning is
-- pinned down; everything else (including equality) is defined in terms of it.
interp
  :: forall {k} (p :: k +-> k) src tgt
   . (BiCCC k)
  => (forall x y. p x y -> x ~> y)
  -> Term (src :: FBC p) tgt
  -> Lower src ~> Lower tgt
interp :: forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ Term src tgt
Id = Lower src ~> Lower src
Lower src ~> Lower tgt
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
interp forall (x :: k) (y :: k). p x y -> x ~> y
gn (Compose Term b tgt
g Term src b
f) = (forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term b tgt -> Lower b ~> Lower tgt
forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn Term b tgt
g (Lower b ~> Lower tgt)
-> (Lower src ~> Lower b) -> Lower src ~> Lower tgt
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src b -> Lower src ~> Lower b
forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn Term src b
f
interp forall (x :: k) (y :: k). p x y -> x ~> y
gn (Emb p x y
g) = p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn p x y
g
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ Term src tgt
Terminate = Lower src ~> TerminalObject
Lower src ~> Lower tgt
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ Term src tgt
Absurd = InitialObject ~> Lower tgt
Lower src ~> Lower tgt
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ (Fst @a @b) = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @(Lower a) @(Lower b)
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ (Snd @a @b) = forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(Lower a) @(Lower b)
interp forall (x :: k) (y :: k). p x y -> x ~> y
gn (Pair Term src a
f Term src b
g) = (forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src a -> Lower src ~> Lower a
forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn Term src a
f (Lower src ~> Lower a)
-> (Lower src ~> Lower b) -> Lower src ~> (Lower a && Lower b)
forall (a :: k) (x :: k) (y :: k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& (forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src b -> Lower src ~> Lower b
forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn Term src b
g
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ (Inl @a @b) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @(Lower a) @(Lower b)
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ (Inr @a @b) = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @(Lower a) @(Lower b)
interp forall (x :: k) (y :: k). p x y -> x ~> y
gn (Case Term a tgt
f Term b tgt
g) = (forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term a tgt -> Lower a ~> Lower tgt
forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn Term a tgt
f (Lower a ~> Lower tgt)
-> (Lower b ~> Lower tgt) -> (Lower a || Lower b) ~> Lower tgt
forall (x :: k) (a :: k) (y :: k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| (forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term b tgt -> Lower b ~> Lower tgt
forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn Term b tgt
g
interp forall (x :: k) (y :: k). p x y -> x ~> y
gn (Curry @a @b @c Term (PROD src b) c
f) = forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @(Lower a) @(Lower b) @(Lower c) ((forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term (PROD src b) c -> Lower (PROD src b) ~> Lower c
forall {k} (p :: k +-> k) (src :: FBC p) (tgt :: FBC p).
BiCCC k =>
(forall (x :: k) (y :: k). p x y -> x ~> y)
-> Term src tgt -> Lower src ~> Lower tgt
interp p x y -> x ~> y
forall (x :: k) (y :: k). p x y -> x ~> y
gn Term (PROD src b) c
f)
interp forall (x :: k) (y :: k). p x y -> x ~> y
_ (Apply @a @b) = forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @_ @(Lower a) @(Lower b)