-- | __Full subcategories__: the kind @'SUBCAT' ob@ restricts a category to the objects satisfying
-- the predicate @ob@, with 'Sub' wrapping the underlying arrows unchanged. This is how object
-- constraints beyond a kind's own 'Ob' are imposed (e.g. the category of representable profunctors
-- in "Proarrow.Category.Instance.Rep").
module Proarrow.Category.Instance.Sub where

import Data.Kind (Constraint)

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, OB, Profunctor (..), Promonad (..), UN, WrappedOb, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Prelude (type (~))

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))

type SUBCAT :: forall {k}. OB k -> Kind
type data SUBCAT (ob :: OB k) = SUB k

-- | Wraps an arrow whose endpoints satisfy the predicate @ob@: the arrows of the full
-- subcategory 'SUBCAT'.
type Sub :: CAT k -> CAT (SUBCAT (ob :: OB k))
data Sub p a b where
  Sub :: (ob a, ob b) => {forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
Sub p (SUB a) (SUB b) -> p a b
unSub :: p a b} -> Sub p (SUB a :: SUBCAT ob) (SUB b)

instance (Profunctor p) => Profunctor (Sub p) where
  dimap :: forall (c :: SUBCAT ob) (a :: SUBCAT ob) (b :: SUBCAT ob)
       (d :: SUBCAT ob).
(c ~> a) -> (b ~> d) -> Sub p a b -> Sub p c d
dimap (Sub a ~> b
l) (Sub a ~> b
r) (Sub p a b
p) = p a b -> Sub p (SUB a) (SUB b)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p 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 a ~> b
a ~> a
l a ~> b
b ~> b
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) r.
((Ob a, Ob b) => r) -> Sub p a b -> r
\\ Sub p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a b
p

instance (Promonad p) => Promonad (Sub p) where
  id :: forall (a :: SUBCAT ob). Ob a => Sub p a a
id = p (UN SUB a) (UN SUB a) -> Sub p (SUB (UN SUB a)) (SUB (UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub p (UN SUB a) (UN SUB a)
forall (a :: k). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Sub p a b
f . :: forall (b :: SUBCAT ob) (c :: SUBCAT ob) (a :: SUBCAT ob).
Sub p b c -> Sub p a b -> Sub p a c
. Sub p a b
g = p a b -> Sub p (SUB a) (SUB b)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (p a b
f p a b -> p a a -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a a
p a b
g)

-- | The subcategory with objects with instances of the given constraint `ob`.
instance (CategoryOf k) => CategoryOf (SUBCAT (ob :: OB k)) where
  type (~>) = Sub (~>)
  type Ob (a :: SUBCAT ob) = (WrappedOb SUB a, ob (UN SUB a))

type On :: (k -> Constraint) -> forall (ob :: OB k) -> SUBCAT ob -> Constraint
class (c (UN SUB a)) => (c `On` ob) a
instance (c (UN SUB a)) => (c `On` ob) a

class (ob (a ** b)) => IsObMult (ob :: OB k) a b
instance (ob (a ** b)) => IsObMult (ob :: OB k) a b

-- | The same for the /product/: that the subcategory contains the products of its objects, as a
-- class with a single instance so that it can be the head of a quantified constraint.
class (ob (a && b)) => IsObProd (ob :: OB k) a b

instance (ob (a && b)) => IsObProd (ob :: OB k) a b

-- | A full subcategory has the ambient finite products as soon as it contains them, as the
-- quantified constraint says. The projections and pairing are the ambient ones under 'Sub'.
--
-- There is no exponential at an arbitrary kind: neither @'withObExp'@ nor @curry@ discharges
-- through @'Proarrow.Limit.BinaryProduct.PROD' k@\'s round trip
-- @'Proarrow.Core.UN' PR (PR a '~~>' PR b)@.
-- For subcategories of profunctors see
-- @'Proarrow.Category.Monoidal.Closed.Closed' ('Proarrow.Limit.BinaryProduct.PROD' ('SUBCAT' ob))@
-- in "Proarrow.Profunctor.Instance.Exponential".
instance (HasTerminalObject k, ob (TerminalObject :: k)) => HasTerminalObject (SUBCAT (ob :: OB k)) where
  type TerminalObject @(SUBCAT (ob :: OB k)) = SUB (TerminalObject :: k)
  terminate :: forall (a :: SUBCAT ob). Ob a => a ~> TerminalObject
terminate = (UN SUB a ~> TerminalObject)
-> Sub (~>) (SUB (UN SUB a)) (SUB TerminalObject)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub UN SUB a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
terminate

instance
  (HasBinaryProducts k, forall a b. (ob a, ob b) => IsObProd ob a b)
  => HasBinaryProducts (SUBCAT (ob :: OB k))
  where
  type (&&) @(SUBCAT (ob :: OB k)) a b = SUB (UN SUB a && UN SUB b)
  withObProd :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(SUB a) @(SUB 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 @a @b r
Ob (UN SUB a && UN SUB b) => r
Ob (a && b) => r
r
  fst :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(SUB a) @(SUB b) = ((UN SUB a && UN SUB b) ~> UN SUB a)
-> Sub (~>) (SUB (UN SUB a && UN SUB b)) (SUB (UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @k @a @b)
  snd :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(SUB a) @(SUB b) = ((UN SUB a && UN SUB b) ~> UN SUB b)
-> Sub (~>) (SUB (UN SUB a && UN SUB b)) (SUB (UN SUB b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @k @a @b)
  Sub a ~> b
l &&& :: forall (a :: SUBCAT ob) (x :: SUBCAT ob) (y :: SUBCAT ob).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Sub a ~> b
r = (a ~> (b && b)) -> Sub (~>) (SUB a) (SUB (b && b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (a ~> b
l (a ~> b) -> (a ~> b) -> a ~> (b && 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)
&&& a ~> b
a ~> b
r)

instance (MonoidalProfunctor p, SubMonoidal ob) => MonoidalProfunctor (Sub p :: CAT (SUBCAT (ob :: OB k))) where
  one :: Sub p Unit Unit
one = p Unit Unit -> Sub p (SUB Unit) (SUB Unit)
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  Sub p a b
f ** :: forall (x1 :: SUBCAT ob) (x2 :: SUBCAT ob) (y1 :: SUBCAT ob)
       (y2 :: SUBCAT ob).
Sub p x1 x2 -> Sub p y1 y2 -> Sub p (x1 ** y1) (x2 ** y2)
** Sub p a b
g = p (a ** a) (b ** b) -> Sub p (SUB (a ** a)) (SUB (b ** b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (p a b
f p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** p a b
g)

class (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: OB k)
instance (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: OB k)

instance (SubMonoidal ob) => Monoidal (SUBCAT (ob :: OB k)) where
  type Unit = SUB Unit
  type a ** b = SUB (UN SUB a ** UN SUB b)
  withOb2 :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(SUB a) @(SUB b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b r
Ob (UN SUB a ** UN SUB b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: SUBCAT ob). Ob a => (Unit ** a) ~> a
leftUnitor = ((Unit ** UN SUB a) ~> UN SUB a)
-> Sub (~>) (SUB (Unit ** UN SUB a)) (SUB (UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (Unit ** UN SUB a) ~> UN SUB a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  leftUnitorInv :: forall (a :: SUBCAT ob). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN SUB a ~> (Unit ** UN SUB a))
-> Sub (~>) (SUB (UN SUB a)) (SUB (Unit ** UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub UN SUB a ~> (Unit ** UN SUB a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  rightUnitor :: forall (a :: SUBCAT ob). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN SUB a ** Unit) ~> UN SUB a)
-> Sub (~>) (SUB (UN SUB a ** Unit)) (SUB (UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (UN SUB a ** Unit) ~> UN SUB a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  rightUnitorInv :: forall (a :: SUBCAT ob). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN SUB a ~> (UN SUB a ** Unit))
-> Sub (~>) (SUB (UN SUB a)) (SUB (UN SUB a ** Unit))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub UN SUB a ~> (UN SUB a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  associator :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(SUB a) @(SUB b) @(SUB c) = (((UN SUB a ** UN SUB b) ** UN SUB c)
 ~> (UN SUB a ** (UN SUB b ** UN SUB c)))
-> Sub
     (~>)
     (SUB ((UN SUB a ** UN SUB b) ** UN SUB c))
     (SUB (UN SUB a ** (UN SUB b ** UN SUB c)))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @b @c)
  associatorInv :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (c :: SUBCAT ob).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(SUB a) @(SUB b) @(SUB c) = ((UN SUB a ** (UN SUB b ** UN SUB c))
 ~> ((UN SUB a ** UN SUB b) ** UN SUB c))
-> Sub
     (~>)
     (SUB (UN SUB a ** (UN SUB b ** UN SUB c)))
     (SUB ((UN SUB a ** UN SUB b) ** UN SUB c))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @a @b @c)

instance (SymMonoidal k, SubMonoidal ob) => SymMonoidal (SUBCAT (ob :: OB k)) where
  swap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(SUB a) @(SUB b) = ((UN SUB a ** UN SUB b) ~> (UN SUB b ** UN SUB a))
-> Sub
     (~>) (SUB (UN SUB a ** UN SUB b)) (SUB (UN SUB b ** UN SUB a))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b)

data family Forget :: forall (ob :: OB k) -> SUBCAT ob +-> k
instance (CategoryOf k) => FunctorForRep (Forget (ob :: OB k)) where
  type Forget ob @ a = UN SUB a
  fmap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Forget ob @ a) ~> (Forget ob @ b)
fmap (Sub a ~> b
f) = a ~> b
(Forget ob @ a) ~> (Forget ob @ b)
f

instance (Representable p, forall a. (ob a) => ob (p % a)) => Representable (Sub p :: CAT (SUBCAT (ob :: OB k))) where
  type Sub p % a = SUB (p % UN SUB a)
  index :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
Sub p a b -> a ~> (Sub p % b)
index (Sub p a b
p) = (a ~> (p % b)) -> Sub (~>) (SUB a) (SUB (p % b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (p a b -> a ~> (p % b)
forall (a :: k) (b :: k). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p a b
p)
  tabulate :: forall (b :: SUBCAT ob) (a :: SUBCAT ob).
Ob b =>
(a ~> (Sub p % b)) -> Sub p a b
tabulate (Sub a ~> b
f) = p a (UN SUB b) -> Sub p (SUB a) (SUB (UN SUB b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub ((a ~> (p % UN SUB b)) -> p a (UN SUB b)
forall (b :: k) (a :: k). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a ~> b
a ~> (p % UN SUB b)
f)
  repMap :: forall (a :: SUBCAT ob) (b :: SUBCAT ob).
(a ~> b) -> (Sub p % a) ~> (Sub p % b)
repMap (Sub a ~> b
f) = ((p % a) ~> (p % b)) -> Sub (~>) (SUB (p % a)) (SUB (p % b))
forall {k} (ob :: k -> Constraint) (a :: k) (b :: k) (p :: CAT k).
(ob a, ob b) =>
p a b -> Sub p (SUB a) (SUB b)
Sub (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a ~> b
f)

type FUN j k = SUBCAT (Representable :: OB (j +-> k))

(!) :: forall {j} {k} f g a b. f ~> (g :: FUN j k) -> a ~> b -> UN SUB f % a ~> UN SUB g % b
Sub (Prof a :~> b
n) ! :: forall {j} {k} (f :: FUN j k) (g :: FUN j k) (a :: j) (b :: j).
(f ~> g) -> (a ~> b) -> (UN SUB f % a) ~> (UN SUB g % b)
! a ~> b
ab = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: k -> j -> Type) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @(UN SUB g) @_ @b (a (a % a) b -> b (a % a) b
a :~> b
n (((a % a) ~> (a % b)) -> a (a % a) b
forall (b :: j) (a :: k). Ob b => (a ~> (a % b)) -> a a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: k -> j -> Type) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @(UN SUB f) a ~> b
ab))) ((Ob a, Ob b) => (a % a) ~> (b % b))
-> (a ~> b) -> (a % a) ~> (b % b)
forall (a :: j) (b :: j) 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 ~> b
ab

-- | The arrow category of @k@ as functor category from @2@ to @k@.
type ARROW k = FUN BOOL k

commSquare
  :: forall {k} f g a b c d
   . (a ~ f % FLS, b ~ f % TRU, c ~ g % FLS, d ~ g % TRU) => SUB f ~> (SUB g :: ARROW k) -> (a ~> b, b ~> d, a ~> c, c ~> d)
commSquare :: forall {k} (f :: BOOL +-> k) (g :: BOOL +-> k) (a :: k) (b :: k)
       (c :: k) (d :: k).
(a ~ (f % 'FLS), b ~ (f % 'TRU), c ~ (g % 'FLS), d ~ (g % 'TRU)) =>
(SUB f ~> SUB g) -> (a ~> b, b ~> d, a ~> c, c ~> d)
commSquare SUB f ~> SUB g
n = (forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: BOOL +-> k) (a :: BOOL) (b :: BOOL).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @f 'FLS ~> 'TRU
Booleans 'FLS 'TRU
F2T, SUB f ~> SUB g
n (SUB f ~> SUB g)
-> ('TRU ~> 'TRU)
-> (UN SUB (SUB f) % 'TRU) ~> (UN SUB (SUB g) % 'TRU)
forall {j} {k} (f :: FUN j k) (g :: FUN j k) (a :: j) (b :: j).
(f ~> g) -> (a ~> b) -> (UN SUB f % a) ~> (UN SUB g % b)
! 'TRU ~> 'TRU
Booleans 'TRU 'TRU
Tru, SUB f ~> SUB g
n (SUB f ~> SUB g)
-> ('FLS ~> 'FLS)
-> (UN SUB (SUB f) % 'FLS) ~> (UN SUB (SUB g) % 'FLS)
forall {j} {k} (f :: FUN j k) (g :: FUN j k) (a :: j) (b :: j).
(f ~> g) -> (a ~> b) -> (UN SUB f % a) ~> (UN SUB g % b)
! 'FLS ~> 'FLS
Booleans 'FLS 'FLS
Fls, forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: BOOL +-> k) (a :: BOOL) (b :: BOOL).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @g 'FLS ~> 'TRU
Booleans 'FLS 'TRU
F2T) ((Ob (SUB f), Ob (SUB g)) => (a ~> b, b ~> d, a ~> c, c ~> d))
-> Sub Prof (SUB f) (SUB g) -> (a ~> b, b ~> d, a ~> c, c ~> d)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: SUBCAT Representable) (b :: SUBCAT Representable) r.
((Ob a, Ob b) => r) -> Sub Prof a b -> r
\\ SUB f ~> SUB g
Sub Prof (SUB f) (SUB g)
n