{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Fam where

import Data.Kind (Type)
import Prelude (($), type (~))

import Proarrow.Category.Instance.Cat (FstCat, Initiate, LftCat, RgtCat, SndCat, Terminate, (:&&&:) (..), (:|||:) (..))
import Proarrow.Category.Instance.Coproduct (COPRODUCT)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Instance.Zero (VOID)
import Proarrow.Category.Opposite (OPPOSITE)
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , lmap
  , obj
  , rmap
  , tgt
  , (//)
  , (:~>)
  , type (+->)
  )
import Proarrow.Functor (FunctorForRep (..), Presheaf)
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Constant (Constant (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), trivialRep, withRepOb)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))

type data FAM (k :: Kind) = forall (x :: Kind). DEP_ (x +-> k)
type instance UN DEP_ (DEP_ dx) = dx

type family X (a :: FAM k) :: Kind where
  X (DEP_ (dx :: x +-> k)) = x
type DX :: forall (a :: FAM k) -> (X a +-> k)
type DX a = UN DEP_ a

type DEP :: forall x -> (x +-> k) -> FAM k
type DEP x dx = DEP_ dx

type Fam :: CAT (FAM k)
data Fam a b where
  Fam
    :: forall {k} {x} {y} {dx :: x +-> k} {dy :: y +-> k} (f :: x +-> y)
     . (Representable dx, Representable dy, Representable f)
    => dx :~> dy :.: f
    -> Fam (DEP x dx :: FAM k) (DEP y dy :: FAM k)

instance (CategoryOf k) => Profunctor (Fam :: CAT (FAM k)) where
  dimap :: forall (c :: FAM k) (a :: FAM k) (b :: FAM k) (d :: FAM k).
(c ~> a) -> (b ~> d) -> Fam a b -> Fam c d
dimap = (c ~> a) -> (b ~> d) -> Fam a b -> Fam c d
Fam c a -> Fam b d -> Fam a b -> Fam 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 :: FAM k) (b :: FAM k) r.
((Ob a, Ob b) => r) -> Fam a b -> r
\\ Fam{} = r
(Ob a, Ob b) => r
r

instance (CategoryOf k) => Promonad (Fam :: CAT (FAM k)) where
  id :: forall (a :: FAM k). Ob a => Fam a a
id = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: X a +-> X a).
(Representable (UN DEP_ a), Representable (UN DEP_ a),
 Representable f) =>
(UN DEP_ a :~> (UN DEP_ a :.: f))
-> Fam (DEP (X a) (UN DEP_ a)) (DEP (X a) (UN DEP_ a))
Fam @Id \UN DEP_ a a b
dx -> UN DEP_ a a b
dx UN DEP_ a a b -> Id b b -> (:.:) (UN DEP_ a) Id a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (UN DEP_ a a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt UN DEP_ a a b
dx)
  Fam @f dx :~> (dy :.: f)
l . :: forall (b :: FAM k) (c :: FAM k) (a :: FAM k).
Fam b c -> Fam a b -> Fam a c
. Fam @g dx :~> (dy :.: f)
r = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: x +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP_ dx) (DEP_ dy)
Fam @(f :.: g) \dx a b
dx -> case dx a b -> (:.:) dy f a b
dx :~> (dy :.: f)
r dx a b
dx of dy a b
dy :.: f b b
g -> case dx a b -> (:.:) dy f a b
dx :~> (dy :.: f)
l dx a b
dy a b
dy of dy a b
dz :.: f b b
f -> dy a b
dz dy a b -> (:.:) f f b b -> (:.:) dy (f :.: f) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (f b b
f f b b -> f b b -> (:.:) f f b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: f b b
g)

-- | The Fam construction a.k.a. the free coproduct completion of @k@
instance (CategoryOf k) => CategoryOf (FAM k) where
  type (~>) = Fam
  type Ob (a :: FAM k) = (a ~ DEP (X a) (DX a), Representable (DX a))

data family Embed :: k +-> FAM k
instance (CategoryOf k) => FunctorForRep (Embed :: k +-> FAM k) where
  type Embed @ a = DEP () (Constant a)
  fmap :: forall (a :: k) (b :: k). (a ~> b) -> (Embed @ a) ~> (Embed @ b)
fmap a ~> b
f = a ~> b
f (a ~> b)
-> ((Ob a, Ob b) =>
    Fam (DEP () (Constant a)) (DEP () (Constant b)))
-> Fam (DEP () (Constant a)) (DEP () (Constant b))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: () +-> ()).
(Representable (Constant a), Representable (Constant b),
 Representable f) =>
(Constant a :~> (Constant b :.: f))
-> Fam (DEP () (Constant a)) (DEP () (Constant b))
Fam @(Constant '()) \(Constant a ~> a
a) -> (a ~> b) -> Constant b a '()
forall {j} {k} (b :: j) (a :: k) (c :: k).
Ob b =>
(a ~> c) -> Constant c a b
Constant (a ~> b
f (a ~> b) -> (a ~> a) -> a ~> b
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
. a ~> a
a) Constant b a '()
-> Constant '() '() b -> (:.:) (Constant b) (Constant '()) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ('() ~> '()) -> Constant '() '() b
forall {j} {k} (b :: j) (a :: k) (c :: k).
Ob b =>
(a ~> c) -> Constant c a b
Constant '() ~> '()
Unit '() '()
Unit

type AsPresheaf :: x +-> k -> Presheaf k
data AsPresheaf dx a u where
  AsPresheaf :: dx a b -> AsPresheaf dx a '()
instance (CategoryOf k, Profunctor dx) => Profunctor (AsPresheaf dx :: Presheaf k) where
  dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()).
(c ~> a) -> (b ~> d) -> AsPresheaf dx a b -> AsPresheaf dx c d
dimap c ~> a
l b ~> d
Unit b d
Unit (AsPresheaf dx a b
dx) = dx c b -> AsPresheaf dx c '()
forall {x} {k} (dx :: x +-> k) (a :: k) (b :: x).
dx a b -> AsPresheaf dx a '()
AsPresheaf ((c ~> a) -> dx a b -> dx c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l dx a b
dx)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: ()) r.
((Ob a, Ob b) => r) -> AsPresheaf dx a b -> r
\\ AsPresheaf dx a b
dx = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> dx a b -> r
forall (a :: k) (b :: x) r. ((Ob a, Ob b) => r) -> dx 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
\\ dx a b
dx
data family IsPresheafSub :: FAM k +-> Presheaf k
instance (CategoryOf k) => FunctorForRep (IsPresheafSub :: FAM k +-> Presheaf k) where
  type IsPresheafSub @ (DEP x dx) = AsPresheaf dx
  fmap :: forall (a :: FAM k) (b :: FAM k).
(a ~> b) -> (IsPresheafSub @ a) ~> (IsPresheafSub @ b)
fmap (Fam dx :~> (dy :.: f)
r) = (AsPresheaf dx :~> AsPresheaf dy)
-> Prof (AsPresheaf dx) (AsPresheaf dy)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(AsPresheaf dx a b
dx) -> dy a (f % b) -> AsPresheaf dy a '()
forall {x} {k} (dx :: x +-> k) (a :: k) (b :: x).
dx a b -> AsPresheaf dx a '()
AsPresheaf (case dx a b -> (:.:) dy f a b
dx :~> (dy :.: f)
r dx a b
dx of dy a b
dy :.: f b b
f -> (b ~> (f % b)) -> dy a b -> dy a (f % b)
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (f b b -> b ~> (f % b)
forall (a :: y) (b :: x). f a b -> a ~> (f % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index f b b
f) dy a b
dy)

instance (CategoryOf k) => HasInitialObject (FAM k) where
  type InitialObject = DEP VOID (Rep Initiate)
  initiate :: forall (a :: FAM k). Ob a => InitialObject ~> a
initiate = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: VOID +-> X a).
(Representable (Rep Initiate), Representable (UN DEP_ a),
 Representable f) =>
(Rep Initiate :~> (UN DEP_ a :.: f))
-> Fam (DEP VOID (Rep Initiate)) (DEP (X a) (UN DEP_ a))
Fam @(Rep Initiate) \(Rep @_ @_ @b a ~> (Initiate @ b)
_) -> case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: VOID). (CategoryOf VOID, Ob a) => Obj a
obj @b of {}

instance (CategoryOf k) => HasBinaryCoproducts (FAM k) where
  type a || b = DEP (COPRODUCT (X a) (X b)) (DX a :|||: DX b)
  withObCoprod :: forall (a :: FAM k) (b :: FAM k) 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 :: FAM k) (b :: FAM k). (Ob a, Ob b) => a ~> (a || b)
lft = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: X a +-> COPRODUCT (X a) (X b)).
(Representable (UN DEP_ a),
 Representable (UN DEP_ a :|||: UN DEP_ b), Representable f) =>
(UN DEP_ a :~> ((UN DEP_ a :|||: UN DEP_ b) :.: f))
-> Fam
     (DEP (X a) (UN DEP_ a))
     (DEP (COPRODUCT (X a) (X b)) (UN DEP_ a :|||: UN DEP_ b))
Fam @(Rep LftCat) \UN DEP_ a a b
p -> UN DEP_ a a b -> (:|||:) (UN DEP_ a) (UN DEP_ b) a (L b)
forall {i} {k} {j} (p :: i +-> k) (a :: k) (b1 :: i)
       (q :: j +-> k).
p a b1 -> (:|||:) p q a (L b1)
InjLP UN DEP_ a a b
p (:|||:) (UN DEP_ a) (UN DEP_ b) a (L b)
-> Rep LftCat (L b) b
-> (:.:) (UN DEP_ a :|||: UN DEP_ b) (Rep LftCat) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Rep LftCat (L b) b
Rep LftCat (Rep LftCat % b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep ((Ob a, Ob b) =>
 (:.:) (UN DEP_ a :|||: UN DEP_ b) (Rep LftCat) a b)
-> UN DEP_ a a b
-> (:.:) (UN DEP_ a :|||: UN DEP_ b) (Rep LftCat) a b
forall (a :: k) (b :: X a) r.
((Ob a, Ob b) => r) -> UN DEP_ a 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
\\ UN DEP_ a a b
p
  rgt :: forall (a :: FAM k) (b :: FAM k). (Ob a, Ob b) => b ~> (a || b)
rgt = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: X b +-> COPRODUCT (X a) (X b)).
(Representable (UN DEP_ b),
 Representable (UN DEP_ a :|||: UN DEP_ b), Representable f) =>
(UN DEP_ b :~> ((UN DEP_ a :|||: UN DEP_ b) :.: f))
-> Fam
     (DEP (X b) (UN DEP_ b))
     (DEP (COPRODUCT (X a) (X b)) (UN DEP_ a :|||: UN DEP_ b))
Fam @(Rep RgtCat) \UN DEP_ b a b
q -> UN DEP_ b a b -> (:|||:) (UN DEP_ a) (UN DEP_ b) a (R b)
forall {j} {k} {i} (q :: j +-> k) (a :: k) (b1 :: j)
       (p :: i +-> k).
q a b1 -> (:|||:) p q a (R b1)
InjRP UN DEP_ b a b
q (:|||:) (UN DEP_ a) (UN DEP_ b) a (R b)
-> Rep RgtCat (R b) b
-> (:.:) (UN DEP_ a :|||: UN DEP_ b) (Rep RgtCat) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: Rep RgtCat (R b) b
Rep RgtCat (Rep RgtCat % b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
trivialRep ((Ob a, Ob b) =>
 (:.:) (UN DEP_ a :|||: UN DEP_ b) (Rep RgtCat) a b)
-> UN DEP_ b a b
-> (:.:) (UN DEP_ a :|||: UN DEP_ b) (Rep RgtCat) a b
forall (a :: k) (b :: X b) r.
((Ob a, Ob b) => r) -> UN DEP_ b 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
\\ UN DEP_ b a b
q
  Fam @f dx :~> (dy :.: f)
l ||| :: forall (x :: FAM k) (a :: FAM k) (y :: FAM k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Fam @g dx :~> (dy :.: f)
r = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: COPRODUCT x x +-> y).
(Representable (dx :|||: dx), Representable dy, Representable f) =>
((dx :|||: dx) :~> (dy :.: f))
-> Fam (DEP (COPRODUCT x x) (dx :|||: dx)) (DEP_ dy)
Fam @(f :|||: g) \case
    InjLP dx a b1
p -> case dx a b1 -> (:.:) dy f a b1
dx :~> (dy :.: f)
l dx a b1
p of dy a b
dx :.: f b b1
f -> dy a b
dx dy a b -> (:|||:) f f b b -> (:.:) dy (f :|||: f) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: f b b1 -> (:|||:) f f b (L b1)
forall {i} {k} {j} (p :: i +-> k) (a :: k) (b1 :: i)
       (q :: j +-> k).
p a b1 -> (:|||:) p q a (L b1)
InjLP f b b1
f
    InjRP dx a b1
q -> case dx a b1 -> (:.:) dy f a b1
dx :~> (dy :.: f)
r dx a b1
q of dy a b
dy :.: f b b1
g -> dy a b
dy a b
dy dy a b -> (:|||:) f f b b -> (:.:) dy (f :|||: f) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: f b b1 -> (:|||:) f f b (R b1)
forall {j} {k} {i} (q :: j +-> k) (a :: k) (b1 :: j)
       (p :: i +-> k).
q a b1 -> (:|||:) p q a (R b1)
InjRP f b b1
g

type Term :: () +-> k
data Term a b where Term :: Ob a => Term a '()
instance (CategoryOf k) => Profunctor (Term :: () +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: ()) (d :: ()).
(c ~> a) -> (b ~> d) -> Term a b -> Term c d
dimap c ~> a
l b ~> d
Unit b d
Unit Term a b
Term = Term c d
Term c '()
(Ob c, Ob a) => Term c d
forall {k} (a :: k). Ob a => Term a '()
Term ((Ob c, Ob a) => Term c d) -> (c ~> a) -> Term c d
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ c ~> a
l
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> Term a b -> r
\\ Term a b
Term = r
(Ob a, Ob b) => r
r
instance (HasTerminalObject k) => Representable (Term :: () +-> k) where
  type Term % '() = TerminalObject
  tabulate :: forall (b :: ()) (a :: k). Ob b => (a ~> (Term % b)) -> Term a b
tabulate a ~> (Term % b)
f = Term a b
Term a '()
(Ob a, Ob TerminalObject) => Term a b
forall {k} (a :: k). Ob a => Term a '()
Term ((Ob a, Ob TerminalObject) => Term a b)
-> (a ~> TerminalObject) -> Term a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> (Term % b)
a ~> TerminalObject
f
  index :: forall (a :: k) (b :: ()). Term a b -> a ~> (Term % b)
index Term a b
Term = a ~> (Term % b)
a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate
  repMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (Term % a) ~> (Term % b)
repMap a ~> b
Unit a b
Unit = (Term % a) ~> (Term % b)
TerminalObject ~> TerminalObject
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (CategoryOf k) => Corepresentable (Term :: () +-> k) where
  type Term %% a = '()
  cotabulate :: forall (a :: k) (b :: ()). Ob a => ((Term %% a) ~> b) -> Term a b
cotabulate (Term %% a) ~> b
Unit '() b
Unit = Term a b
Term a '()
forall {k} (a :: k). Ob a => Term a '()
Term
  coindex :: forall (a :: k) (b :: ()). Term a b -> (Term %% a) ~> b
coindex Term a b
Term = (Term %% a) ~> b
Unit '() '()
Unit
  corepMap :: forall (a :: k) (b :: k). (a ~> b) -> (Term %% a) ~> (Term %% b)
corepMap a ~> b
_ = (Term %% a) ~> (Term %% b)
Unit '() '()
Unit
instance (HasTerminalObject k) => HasTerminalObject (FAM k) where
  type TerminalObject = DEP () Term
  terminate :: forall (a :: FAM k). Ob a => a ~> TerminalObject
terminate = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: X a +-> ()).
(Representable (UN DEP_ a), Representable Term, Representable f) =>
(UN DEP_ a :~> (Term :.: f))
-> Fam (DEP (X a) (UN DEP_ a)) (DEP () Term)
Fam @(Rep Terminate) \UN DEP_ a a b
dx -> Term a '()
forall {k} (a :: k). Ob a => Term a '()
Term Term a '() -> Rep Terminate '() b -> (:.:) Term (Rep Terminate) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ('() ~> (Terminate @ b)) -> Rep Terminate '() b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep '() ~> (Terminate @ b)
Unit '() '()
Unit ((Ob a, Ob b) => (:.:) Term (Rep Terminate) a b)
-> UN DEP_ a a b -> (:.:) Term (Rep Terminate) a b
forall (a :: k) (b :: X a) r.
((Ob a, Ob b) => r) -> UN DEP_ a 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
\\ UN DEP_ a a b
dx

type (:&&:) :: x +-> k -> y +-> k -> (x, y) +-> k
data (p :&&: q) a b where
  (:&&:) :: p a b -> q a c -> (p :&&: q) a '(b, c)
instance (Profunctor l, Profunctor r, CategoryOf k) => Profunctor (l :&&: r :: (x, y) +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: (x, y)) (d :: (x, y)).
(c ~> a) -> (b ~> d) -> (:&&:) l r a b -> (:&&:) l r c d
dimap c ~> a
l (a1 ~> b1
r0 :**: a2 ~> b2
r1) (l a b
p :&&: r a c
q) = (c ~> a) -> (b ~> b1) -> l a b -> l c b1
forall (c :: k) (a :: k) (b :: x) (d :: x).
(c ~> a) -> (b ~> d) -> l a b -> l c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l a1 ~> b1
b ~> b1
r0 l a b
p l c b1 -> r c b2 -> (:&&:) l r c '(b1, b2)
forall {x} {k} {y} (p :: x +-> k) (a :: k) (b :: x) (q :: y +-> k)
       (c :: y).
p a b -> q a c -> (:&&:) p q a '(b, c)
:&&: (c ~> a) -> (c ~> b2) -> r a c -> r c b2
forall (c :: k) (a :: k) (b :: y) (d :: y).
(c ~> a) -> (b ~> d) -> r a b -> r c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l a2 ~> b2
c ~> b2
r1 r a c
q
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: (x, y)) r.
((Ob a, Ob b) => r) -> (:&&:) l r a b -> r
\\ (l a b
p :&&: r a c
q) = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> l a b -> r
forall (a :: k) (b :: x) r. ((Ob a, Ob b) => r) -> l 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
\\ l a b
p ((Ob a, Ob c) => r) -> r a c -> r
forall (a :: k) (b :: y) r. ((Ob a, Ob b) => r) -> r 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
\\ r a c
q
instance (Representable l, Representable r, HasBinaryProducts k) => Representable (l :&&: r :: (x, y) +-> k) where
  type (l :&&: r) % '(a, b) = (l % a) && (r % b)
  tabulate :: forall (b :: (x, y)) (a :: k).
Ob b =>
(a ~> ((l :&&: r) % b)) -> (:&&:) l r a b
tabulate @'(a, b) a ~> ((l :&&: r) % b)
f = forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: x +-> k) (a :: x) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @l @a ((Ob (l % Fst b) => (:&&:) l r a b) -> (:&&:) l r a b)
-> (Ob (l % Fst b) => (:&&:) l r a b) -> (:&&:) l r a b
forall a b. (a -> b) -> a -> b
$ forall {j} {k} (p :: j +-> k) (a :: j) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
forall (p :: y +-> k) (a :: y) r.
(Representable p, Ob a) =>
(Ob (p % a) => r) -> r
withRepOb @r @b ((Ob (r % Snd b) => (:&&:) l r a b) -> (:&&:) l r a b)
-> (Ob (r % Snd b) => (:&&:) l r a b) -> (:&&:) l r a b
forall a b. (a -> b) -> a -> b
$ (a ~> (l % Fst b)) -> l a (Fst b)
forall (b :: x) (a :: k). Ob b => (a ~> (l % b)) -> l a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @(l % a) @(r % b) (((l % Fst b) && (r % Snd b)) ~> (l % Fst b))
-> (a ~> ((l % Fst b) && (r % Snd b))) -> a ~> (l % Fst b)
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
. a ~> ((l :&&: r) % b)
a ~> ((l % Fst b) && (r % Snd b))
f) l a (Fst b) -> r a (Snd b) -> (:&&:) l r a '(Fst b, Snd b)
forall {x} {k} {y} (p :: x +-> k) (a :: k) (b :: x) (q :: y +-> k)
       (c :: y).
p a b -> q a c -> (:&&:) p q a '(b, c)
:&&: (a ~> (r % Snd b)) -> r a (Snd b)
forall (b :: y) (a :: k). Ob b => (a ~> (r % b)) -> r a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @(l % a) @(r % b) (((l % Fst b) && (r % Snd b)) ~> (r % Snd b))
-> (a ~> ((l % Fst b) && (r % Snd b))) -> a ~> (r % Snd b)
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
. a ~> ((l :&&: r) % b)
a ~> ((l % Fst b) && (r % Snd b))
f)
  index :: forall (a :: k) (b :: (x, y)).
(:&&:) l r a b -> a ~> ((l :&&: r) % b)
index (l a b
p :&&: r a c
q) = l a b -> a ~> (l % b)
forall (a :: k) (b :: x). l a b -> a ~> (l % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index l a b
p (a ~> (l % b)) -> (a ~> (r % c)) -> a ~> ((l % b) && (r % c))
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)
&&& r a c -> a ~> (r % c)
forall (a :: k) (b :: y). r a b -> a ~> (r % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index r a c
q
  repMap :: forall (a :: (x, y)) (b :: (x, y)).
(a ~> b) -> ((l :&&: r) % a) ~> ((l :&&: r) % b)
repMap (a1 ~> b1
f :**: a2 ~> b2
g) = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: x +-> k) (a :: x) (b :: x).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @l a1 ~> b1
f ((l % a1) ~> (l % b1))
-> ((r % a2) ~> (r % b2))
-> ((l % a1) && (r % a2)) ~> ((l % b1) && (r % b2))
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: y +-> k) (a :: y) (b :: y).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @r a2 ~> b2
g
instance (Corepresentable l, Corepresentable r, CategoryOf k) => Corepresentable (l :&&: r :: (x, y) +-> k) where
  type (l :&&: r) %% a = '(l %% a, r %% a)
  cotabulate :: forall (a :: k) (b :: (x, y)).
Ob a =>
(((l :&&: r) %% a) ~> b) -> (:&&:) l r a b
cotabulate (a1 ~> b1
f :**: a2 ~> b2
g) = ((l %% a) ~> b1) -> l a b1
forall (a :: k) (b :: x). Ob a => ((l %% a) ~> b) -> l a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate a1 ~> b1
(l %% a) ~> b1
f l a b1 -> r a b2 -> (:&&:) l r a '(b1, b2)
forall {x} {k} {y} (p :: x +-> k) (a :: k) (b :: x) (q :: y +-> k)
       (c :: y).
p a b -> q a c -> (:&&:) p q a '(b, c)
:&&: ((r %% a) ~> b2) -> r a b2
forall (a :: k) (b :: y). Ob a => ((r %% a) ~> b) -> r a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Corepresentable p, Ob a) =>
((p %% a) ~> b) -> p a b
cotabulate a2 ~> b2
(r %% a) ~> b2
g
  coindex :: forall (a :: k) (b :: (x, y)).
(:&&:) l r a b -> ((l :&&: r) %% a) ~> b
coindex (l a b
p :&&: r a c
q) = l a b -> (l %% a) ~> b
forall (a :: k) (b :: x). l a b -> (l %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex l a b
p ((l %% a) ~> b)
-> ((r %% a) ~> c) -> (:**:) (~>) (~>) '(l %% a, r %% a) '(b, c)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: r a c -> (r %% a) ~> c
forall (a :: k) (b :: y). r a b -> (r %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex r a c
q
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> ((l :&&: r) %% a) ~> ((l :&&: r) %% b)
corepMap a ~> b
f = forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: x +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @l a ~> b
f ((l %% a) ~> (l %% b))
-> ((r %% a) ~> (r %% b))
-> (:**:) (~>) (~>) '(l %% a, r %% a) '(l %% b, r %% b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall {j} {k} (p :: j +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
forall (p :: y +-> k) (a :: k) (b :: k).
Corepresentable p =>
(a ~> b) -> (p %% a) ~> (p %% b)
corepMap @r a ~> b
f
instance (HasBinaryProducts k) => HasBinaryProducts (FAM k) where
  type a && b = DEP (X a, X b) (DX a :&&: DX b)
  withObProd :: forall (a :: FAM k) (b :: FAM k) 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 :: FAM k) (b :: FAM k). (Ob a, Ob b) => (a && b) ~> a
fst = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: (X a, X b) +-> X a).
(Representable (UN DEP_ a :&&: UN DEP_ b),
 Representable (UN DEP_ a), Representable f) =>
((UN DEP_ a :&&: UN DEP_ b) :~> (UN DEP_ a :.: f))
-> Fam
     (DEP (X a, X b) (UN DEP_ a :&&: UN DEP_ b)) (DEP (X a) (UN DEP_ a))
Fam @(Rep FstCat) \(UN DEP_ a a b
l :&&: UN DEP_ b a c
r) -> UN DEP_ a a b
l UN DEP_ a a b
-> Rep FstCat b b -> (:.:) (UN DEP_ a) (Rep FstCat) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> (FstCat @ b)) -> Rep FstCat b b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep b ~> b
b ~> (FstCat @ b)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: X a). Ob a => a ~> a
id ((Ob a, Ob b) => (:.:) (UN DEP_ a) (Rep FstCat) a b)
-> UN DEP_ a a b -> (:.:) (UN DEP_ a) (Rep FstCat) a b
forall (a :: k) (b :: X a) r.
((Ob a, Ob b) => r) -> UN DEP_ a 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
\\ UN DEP_ a a b
l ((Ob a, Ob c) => (:.:) (UN DEP_ a) (Rep FstCat) a b)
-> UN DEP_ b a c -> (:.:) (UN DEP_ a) (Rep FstCat) a b
forall (a :: k) (b :: X b) r.
((Ob a, Ob b) => r) -> UN DEP_ b 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
\\ UN DEP_ b a c
r
  snd :: forall (a :: FAM k) (b :: FAM k). (Ob a, Ob b) => (a && b) ~> b
snd = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: (X a, X b) +-> X b).
(Representable (UN DEP_ a :&&: UN DEP_ b),
 Representable (UN DEP_ b), Representable f) =>
((UN DEP_ a :&&: UN DEP_ b) :~> (UN DEP_ b :.: f))
-> Fam
     (DEP (X a, X b) (UN DEP_ a :&&: UN DEP_ b)) (DEP (X b) (UN DEP_ b))
Fam @(Rep SndCat) \(UN DEP_ a a b
l :&&: UN DEP_ b a c
r) -> UN DEP_ b a c
r UN DEP_ b a c
-> Rep SndCat c b -> (:.:) (UN DEP_ b) (Rep SndCat) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (c ~> (SndCat @ b)) -> Rep SndCat c b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep c ~> c
c ~> (SndCat @ b)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: X b). Ob a => a ~> a
id ((Ob a, Ob b) => (:.:) (UN DEP_ b) (Rep SndCat) a b)
-> UN DEP_ a a b -> (:.:) (UN DEP_ b) (Rep SndCat) a b
forall (a :: k) (b :: X a) r.
((Ob a, Ob b) => r) -> UN DEP_ a 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
\\ UN DEP_ a a b
l ((Ob a, Ob c) => (:.:) (UN DEP_ b) (Rep SndCat) a b)
-> UN DEP_ b a c -> (:.:) (UN DEP_ b) (Rep SndCat) a b
forall (a :: k) (b :: X b) r.
((Ob a, Ob b) => r) -> UN DEP_ b 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
\\ UN DEP_ b a c
r
  Fam @f dx :~> (dy :.: f)
l &&& :: forall (a :: FAM k) (x :: FAM k) (y :: FAM k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Fam @g dx :~> (dy :.: f)
r = forall {k} {b} {c} {dx :: b +-> k} {dy :: c +-> k} (f :: b +-> c).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP c dy)
forall (f :: x +-> (y, y)).
(Representable dx, Representable (dy :&&: dy), Representable f) =>
(dx :~> ((dy :&&: dy) :.: f))
-> Fam (DEP_ dx) (DEP (y, y) (dy :&&: dy))
Fam @(f :&&&: g) \dx a b
dx -> case (dx a b -> (:.:) dy f a b
dx :~> (dy :.: f)
l dx a b
dx, dx a b -> (:.:) dy f a b
dx :~> (dy :.: f)
r dx a b
dx a b
dx) of (dy a b
dy1 :.: f b b
f, dy a b
dy2 :.: f b b
g) -> (dy a b
dy1 dy a b -> dy a b -> (:&&:) dy dy a '(b, b)
forall {x} {k} {y} (p :: x +-> k) (a :: k) (b :: x) (q :: y +-> k)
       (c :: y).
p a b -> q a c -> (:&&:) p q a '(b, c)
:&&: dy a b
dy2) (:&&:) dy dy a '(b, b)
-> (:&&&:) f f '(b, b) b -> (:.:) (dy :&&: dy) (f :&&&: f) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (f b b
f f b b -> f b b -> (:&&&:) f f '(b, b) b
forall {k} {i} {j} (p :: k +-> i) (a1 :: i) (b :: k) (q :: k +-> j)
       (b1 :: j).
p a1 b -> q b1 b -> (:&&&:) p q '(a1, b1) b
:&&&: f b b
g)

type Poly = FAM (OPPOSITE Type)