{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.Fam where

import Data.Kind (Type)
import GHC.Base (Any)
import Prelude (type (~))

import Proarrow.Category.Instance.Coproduct (COPRODUCT (..), Codiag, Lft, Rgt, (:++:) (..))
import Proarrow.Category.Instance.Opposite (OPPOSITE)
import Proarrow.Category.Instance.Product (Diag, Fst, Snd, (:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Instance.Zero (VOID)
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , lmap
  , obj
  , rmap
  , tgt
  , (//)
  , (:~>)
  , type (+->)
  )
import Proarrow.Functor (FunctorForRep (..), Presheaf)
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Corepresentable (Corep (..), Corepresentable (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Constant (Constant)
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), repUniv)

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

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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y 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} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y 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} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
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} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
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 () (Rep (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 () (Rep (Constant a))) (DEP () (Rep (Constant b))))
-> Fam (DEP () (Rep (Constant a))) (DEP () (Rep (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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: () +-> ()).
(Representable (Rep (Constant a)),
 Representable (Rep (Constant b)), Representable f) =>
(Rep (Constant a) :~> (Rep (Constant b) :.: f))
-> Fam (DEP () (Rep (Constant a))) (DEP () (Rep (Constant b)))
Fam @(Rep (Constant '())) \(Rep a ~> (Constant a @ b)
a) -> (a ~> (Constant b @ '())) -> Rep (Constant b) a '()
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (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 a @ b)
a) Rep (Constant b) a '()
-> Rep (Constant '()) '() b
-> (:.:) (Rep (Constant b)) (Rep (Constant '())) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ('() ~> (Constant '() @ b)) -> Rep (Constant '()) '() b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep '() ~> (Constant '() @ b)
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 (c :: k) (a :: k) (b :: x). (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 (b :: y) (d :: y) (a :: k). (b ~> d) -> dy a b -> dy a d
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)

data family Initiate :: VOID +-> k
instance (CategoryOf k) => FunctorForRep (Initiate :: VOID +-> k) where
  type Initiate @ a = Any
  fmap :: forall (a :: VOID) (b :: VOID).
(a ~> b) -> (Initiate @ a) ~> (Initiate @ b)
fmap = \case {}

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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y 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)) (Rep Codiag :.: (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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: X a +-> COPRODUCT (X a) (X b)).
(Representable (UN DEP_ a),
 Representable (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)),
 Representable f) =>
(UN DEP_ a :~> ((Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) :.: f))
-> Fam
     (DEP (X a) (UN DEP_ a))
     (DEP
        (COPRODUCT (X a) (X b))
        (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)))
Fam @(Rep Lft) \UN DEP_ a a b
p -> (Rep Codiag a (L a)
Rep Codiag (Rep Codiag % L a) (L a)
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: COPRODUCT k k). Ob a => Rep Codiag (Rep Codiag % a) a
repUniv Rep Codiag a (L a)
-> (:++:) (UN DEP_ a) (UN DEP_ b) (L a) (L b)
-> (:.:) (Rep Codiag) (UN DEP_ a :++: UN DEP_ b) a (L b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: UN DEP_ a a b -> (:++:) (UN DEP_ a) (UN DEP_ b) (L a) (L b)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL UN DEP_ a a b
p) (:.:) (Rep Codiag) (UN DEP_ a :++: UN DEP_ b) a (L b)
-> Rep Lft (L b) b
-> (:.:) (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) (Rep Lft) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Rep Lft (Rep Lft % b) b
Rep Lft (L b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: X a). Ob a => Rep Lft (Rep Lft % a) a
repUniv ((Ob a, Ob b) =>
 (:.:) (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) (Rep Lft) a b)
-> UN DEP_ a a b
-> (:.:) (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) (Rep Lft) 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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: X b +-> COPRODUCT (X a) (X b)).
(Representable (UN DEP_ b),
 Representable (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)),
 Representable f) =>
(UN DEP_ b :~> ((Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) :.: f))
-> Fam
     (DEP (X b) (UN DEP_ b))
     (DEP
        (COPRODUCT (X a) (X b))
        (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)))
Fam @(Rep Rgt) \UN DEP_ b a b
q -> (Rep Codiag a (R a)
Rep Codiag (Rep Codiag % R a) (R a)
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: COPRODUCT k k). Ob a => Rep Codiag (Rep Codiag % a) a
repUniv Rep Codiag a (R a)
-> (:++:) (UN DEP_ a) (UN DEP_ b) (R a) (R b)
-> (:.:) (Rep Codiag) (UN DEP_ a :++: UN DEP_ b) a (R b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: UN DEP_ b a b -> (:++:) (UN DEP_ a) (UN DEP_ b) (R a) (R b)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR UN DEP_ b a b
q) (:.:) (Rep Codiag) (UN DEP_ a :++: UN DEP_ b) a (R b)
-> Rep Rgt (R b) b
-> (:.:) (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) (Rep Rgt) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Rep Rgt (Rep Rgt % b) b
Rep Rgt (R b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: X b). Ob a => Rep Rgt (Rep Rgt % a) a
repUniv ((Ob a, Ob b) =>
 (:.:) (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) (Rep Rgt) a b)
-> UN DEP_ b a b
-> (:.:) (Rep Codiag :.: (UN DEP_ a :++: UN DEP_ b)) (Rep Rgt) 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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: COPRODUCT x x +-> y).
(Representable (Rep Codiag :.: (dx :++: dx)), Representable dy,
 Representable f) =>
((Rep Codiag :.: (dx :++: dx)) :~> (dy :.: f))
-> Fam
     (DEP (COPRODUCT x x) (Rep Codiag :.: (dx :++: dx))) (DEP_ dy)
Fam @(Rep Codiag :.: (f :++: g)) \case
    Rep a ~> (Codiag @ b)
d :.: InjL dx a1 b1
p -> case dx a1 b1 -> (:.:) dy f a1 b1
dx :~> (dy :.: f)
l dx a1 b1
p of dy a1 b
dx :.: f b b1
f -> (a ~> a1) -> dy a1 b -> dy a b
forall (c :: k) (a :: k) (b :: y). (c ~> a) -> dy a b -> dy 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 a ~> a1
a ~> (Codiag @ b)
d dy a1 b
dx dy a b
-> (:.:) (Rep Codiag) (f :++: f) b (L b1)
-> (:.:) dy (Rep Codiag :.: (f :++: f)) a (L b1)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (Rep Codiag b (L b)
Rep Codiag (Rep Codiag % L b) (L b)
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: COPRODUCT y y). Ob a => Rep Codiag (Rep Codiag % a) a
repUniv Rep Codiag b (L b)
-> (:++:) f f (L b) (L b1)
-> (:.:) (Rep Codiag) (f :++: f) b (L b1)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: f b b1 -> (:++:) f f (L b) (L b1)
forall {j1} {k1} {j2} {k2} (p :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (q :: j2 +-> k2).
p a1 b1 -> (:++:) p q (L a1) (L b1)
InjL f b b1
f) ((Ob b, Ob b1) => (:.:) dy (Rep Codiag :.: (f :++: f)) a (L b1))
-> f b b1 -> (:.:) dy (Rep Codiag :.: (f :++: f)) a (L b1)
forall (a :: y) (b :: x) r. ((Ob a, Ob b) => r) -> f 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
\\ f b b1
f
    Rep a ~> (Codiag @ b)
d :.: InjR dx a1 b1
q -> case dx a1 b1 -> (:.:) dy f a1 b1
dx :~> (dy :.: f)
r dx a1 b1
q of dy a1 b
dy :.: f b b1
g -> (a ~> a1) -> dy a1 b -> dy a b
forall (c :: k) (a :: k) (b :: y). (c ~> a) -> dy a b -> dy 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 a ~> a1
a ~> (Codiag @ b)
d dy a1 b
dy dy a b
-> (:.:) (Rep Codiag) (f :++: f) b (R b1)
-> (:.:) dy (Rep Codiag :.: (f :++: f)) a (R b1)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (Rep Codiag b (R b)
Rep Codiag (Rep Codiag % R b) (R b)
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: COPRODUCT y y). Ob a => Rep Codiag (Rep Codiag % a) a
repUniv Rep Codiag b (R b)
-> (:++:) f f (R b) (R b1)
-> (:.:) (Rep Codiag) (f :++: f) b (R b1)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: f b b1 -> (:++:) f f (R b) (R b1)
forall {j2} {k2} {j1} {k1} (q :: j2 +-> k2) (a1 :: k2) (b1 :: j2)
       (p :: j1 +-> k1).
q a1 b1 -> (:++:) p q (R a1) (R b1)
InjR f b b1
g) ((Ob b, Ob b1) => (:.:) dy (Rep Codiag :.: (f :++: f)) a (R b1))
-> f b b1 -> (:.:) dy (Rep Codiag :.: (f :++: f)) a (R b1)
forall (a :: y) (b :: x) r. ((Ob a, Ob b) => r) -> f 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
\\ f b b1
g

instance (HasTerminalObject k) => HasTerminalObject (FAM k) where
  type TerminalObject = DEP () TerminalProfunctor
  terminate :: forall (a :: FAM k). Ob a => a ~> TerminalObject
terminate = forall {k} {b} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: X a +-> ()).
(Representable (UN DEP_ a), Representable TerminalProfunctor,
 Representable f) =>
(UN DEP_ a :~> (TerminalProfunctor :.: f))
-> Fam (DEP (X a) (UN DEP_ a)) (DEP () TerminalProfunctor)
Fam @(Rep (Constant '())) \UN DEP_ a a b
dx -> TerminalProfunctor a '()
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor TerminalProfunctor a '()
-> Rep (Constant '()) '() b
-> (:.:) TerminalProfunctor (Rep (Constant '())) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: ('() ~> (Constant '() @ b)) -> Rep (Constant '()) '() b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep '() ~> (Constant '() @ b)
Unit '() '()
Unit ((Ob a, Ob b) => (:.:) TerminalProfunctor (Rep (Constant '())) a b)
-> UN DEP_ a a b
-> (:.:) TerminalProfunctor (Rep (Constant '())) 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

instance (HasBinaryProducts k) => HasBinaryProducts (FAM k) where
  type a && b = DEP (X a, X b) (Corep Diag :.: (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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: (X a, X b) +-> X a).
(Representable (Corep Diag :.: (UN DEP_ a :**: UN DEP_ b)),
 Representable (UN DEP_ a), Representable f) =>
((Corep Diag :.: (UN DEP_ a :**: UN DEP_ b)) :~> (UN DEP_ a :.: f))
-> Fam
     (DEP (X a, X b) (Corep Diag :.: (UN DEP_ a :**: UN DEP_ b)))
     (DEP (X a) (UN DEP_ a))
Fam @(Rep Fst) \(Corep (a1 ~> b1
d :**: a2 ~> b2
_) :.: (UN DEP_ a a1 b1
l :**: UN DEP_ b a2 b2
r)) -> (a ~> b1) -> UN DEP_ a b1 b1 -> UN DEP_ a a b1
forall (c :: k) (a :: k) (b :: X a).
(c ~> a) -> UN DEP_ a a b -> UN DEP_ a 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 a ~> b1
a1 ~> b1
d UN DEP_ a b1 b1
UN DEP_ a a1 b1
l UN DEP_ a a b1 -> Rep Fst b1 b -> (:.:) (UN DEP_ a) (Rep Fst) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Rep Fst b1 b
Rep Fst (Rep Fst % b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: (X a, X b)). Ob a => Rep Fst (Rep Fst % a) a
repUniv ((Ob a1, Ob b1) => (:.:) (UN DEP_ a) (Rep Fst) a b)
-> UN DEP_ a a1 b1 -> (:.:) (UN DEP_ a) (Rep Fst) 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 a1 b1
l ((Ob a2, Ob b2) => (:.:) (UN DEP_ a) (Rep Fst) a b)
-> UN DEP_ b a2 b2 -> (:.:) (UN DEP_ a) (Rep Fst) 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 a2 b2
r
  snd :: forall (a :: FAM k) (b :: FAM k). (Ob a, Ob b) => (a && b) ~> b
snd = forall {k} {b} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: (X a, X b) +-> X b).
(Representable (Corep Diag :.: (UN DEP_ a :**: UN DEP_ b)),
 Representable (UN DEP_ b), Representable f) =>
((Corep Diag :.: (UN DEP_ a :**: UN DEP_ b)) :~> (UN DEP_ b :.: f))
-> Fam
     (DEP (X a, X b) (Corep Diag :.: (UN DEP_ a :**: UN DEP_ b)))
     (DEP (X b) (UN DEP_ b))
Fam @(Rep Snd) \(Corep (a1 ~> b1
_ :**: a2 ~> b2
d) :.: (UN DEP_ a a1 b1
l :**: UN DEP_ b a2 b2
r)) -> (a ~> b2) -> UN DEP_ b b2 b2 -> UN DEP_ b a b2
forall (c :: k) (a :: k) (b :: X b).
(c ~> a) -> UN DEP_ b a b -> UN DEP_ b 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 a ~> b2
a2 ~> b2
d UN DEP_ b b2 b2
UN DEP_ b a2 b2
r UN DEP_ b a b2 -> Rep Snd b2 b -> (:.:) (UN DEP_ b) (Rep Snd) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Rep Snd b2 b
Rep Snd (Rep Snd % b) b
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (a :: (X a, X b)). Ob a => Rep Snd (Rep Snd % a) a
repUniv ((Ob a1, Ob b1) => (:.:) (UN DEP_ b) (Rep Snd) a b)
-> UN DEP_ a a1 b1 -> (:.:) (UN DEP_ b) (Rep Snd) 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 a1 b1
l ((Ob a2, Ob b2) => (:.:) (UN DEP_ b) (Rep Snd) a b)
-> UN DEP_ b a2 b2 -> (:.:) (UN DEP_ b) (Rep Snd) 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 a2 b2
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} {y} {dx :: b +-> k} {dy :: y +-> k} (f :: b +-> y).
(Representable dx, Representable dy, Representable f) =>
(dx :~> (dy :.: f)) -> Fam (DEP b dx) (DEP y dy)
forall (f :: x +-> (y, y)).
(Representable dx, Representable (Corep Diag :.: (dy :**: dy)),
 Representable f) =>
(dx :~> ((Corep Diag :.: (dy :**: dy)) :.: f))
-> Fam (DEP_ dx) (DEP (y, y) (Corep Diag :.: (dy :**: dy)))
Fam @((f :**: g) :.: Rep Diag) \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) -> (Corep Diag a '(a, a)
Corep Diag a (Corep Diag %% a)
forall (a :: k). Ob a => Corep Diag a (Corep Diag %% a)
forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv Corep Diag a '(a, a)
-> (:**:) dy dy '(a, a) '(b, b)
-> (:.:) (Corep Diag) (dy :**: dy) a '(b, b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (dy a b
dy1 dy a b -> dy a b -> (:**:) dy dy '(a, a) '(b, 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)
:**: dy a b
dy2)) (:.:) (Corep Diag) (dy :**: dy) a '(b, b)
-> (:.:) (f :**: f) (Rep Diag) '(b, b) b
-> (:.:)
     (Corep Diag :.: (dy :**: dy)) ((f :**: f) :.: Rep Diag) a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
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, 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)
:**: f b b
g) (:**:) f f '(b, b) '(b, b)
-> Rep Diag '(b, b) b -> (:.:) (f :**: f) (Rep Diag) '(b, b) b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Rep Diag '(b, b) b
Rep Diag (Rep Diag % b) b
forall (a :: x). Ob a => Rep Diag (Rep Diag % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv) ((Ob b, Ob b) =>
 (:.:) (Corep Diag :.: (dy :**: dy)) ((f :**: f) :.: Rep Diag) a b)
-> f b b
-> (:.:)
     (Corep Diag :.: (dy :**: dy)) ((f :**: f) :.: Rep Diag) a b
forall (a :: y) (b :: x) r. ((Ob a, Ob b) => r) -> f 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
\\ f b b
f ((Ob a, Ob b) =>
 (:.:) (Corep Diag :.: (dy :**: dy)) ((f :**: f) :.: Rep Diag) a b)
-> dy a b
-> (:.:)
     (Corep Diag :.: (dy :**: dy)) ((f :**: f) :.: Rep Diag) a b
forall (a :: k) (b :: y) r. ((Ob a, Ob b) => r) -> dy 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
\\ dy a b
dy2

type Poly = FAM (OPPOSITE Type)