module Proarrow.Category.Instance.Collage where

import Data.Kind (Constraint)

import Proarrow.Category.Enriched.Thin
  ( CodiscreteProfunctor
  , DiscreteProfunctor (..)
  , Thin
  , ThinProfunctor (..)
  , anyArr
  )
import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))
import Proarrow.Category.Instance.Coproduct qualified as C
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Colimit.Initial (HasInitialObject (..), initiate')
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Obj
  , Profunctor (..)
  , Promonad (..)
  , dimapDefault
  , lmap
  , obj
  , rmap
  , type (+->)
  )
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..), terminate')
import Proarrow.Optic (Iso', iso)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corep (..))
import Proarrow.Profunctor.Representable (Rep (..))

type COLLAGE :: forall {j} {k}. k +-> j -> Kind
type data COLLAGE (p :: k +-> j) = L j | R k

type Collage :: CAT (COLLAGE p)
data Collage a b where
  InL :: a ~> b -> Collage (L a :: COLLAGE p) (L b :: COLLAGE p)
  InR :: a ~> b -> Collage (R a :: COLLAGE p) (R b :: COLLAGE p)
  L2R :: p a b -> Collage (L a :: COLLAGE p) (R b :: COLLAGE p)

type IsLR :: forall {p}. COLLAGE p -> Constraint
class IsLR (a :: COLLAGE p) where
  lrId :: Obj a
instance (Ob a, Promonad ((~>) :: CAT k)) => IsLR (L a :: (COLLAGE (p :: j +-> k))) where
  lrId :: Obj (L a)
lrId = (a ~> a) -> Collage (L a) (L a)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
instance (Ob a, Promonad ((~>) :: CAT j)) => IsLR (R a :: (COLLAGE (p :: j +-> k))) where
  lrId :: Obj (R a)
lrId = (a ~> a) -> Collage (R a) (R a)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (Profunctor p) => Profunctor (Collage :: CAT (COLLAGE p)) where
  dimap :: forall (c :: COLLAGE p) (a :: COLLAGE p) (b :: COLLAGE p)
       (d :: COLLAGE p).
(c ~> a) -> (b ~> d) -> Collage a b -> Collage c d
dimap = (c ~> a) -> (b ~> d) -> Collage a b -> Collage c d
Collage c a -> Collage b d -> Collage a b -> Collage 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 :: COLLAGE p) (b :: COLLAGE p) r.
((Ob a, Ob b) => r) -> Collage a b -> r
\\ InL a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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
f
  (Ob a, Ob b) => r
r \\ InR a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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 ~> b
f
  (Ob a, Ob b) => r
r \\ L2R 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 :: j) (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 (Profunctor p) => Promonad (Collage :: CAT (COLLAGE p)) where
  id :: forall (a :: COLLAGE p). Ob a => Collage a a
id = Obj a
Collage a a
forall {k} {j} {p :: k +-> j} (a :: COLLAGE p). IsLR a => Obj a
lrId
  InL a ~> b
g . :: forall (b :: COLLAGE p) (c :: COLLAGE p) (a :: COLLAGE p).
Collage b c -> Collage a b -> Collage a c
. InL a ~> b
f = (a ~> b) -> Collage (L a) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL (a ~> b
g (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: j) (c :: j) (a :: j). (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 ~> b
f)
  InR a ~> b
g . L2R p a b
p = p a b -> Collage (L a) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R ((b ~> b) -> p a b -> p a b
forall (b :: k) (d :: k) (a :: j). (b ~> d) -> p a b -> p 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 a ~> b
b ~> b
g p a b
p)
  L2R p a b
p . InL a ~> b
f = p a b -> Collage (L a) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R ((a ~> a) -> p a b -> p a b
forall (c :: j) (a :: j) (b :: k). (c ~> a) -> p a b -> p 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 ~> a
a ~> b
f p a b
p)
  InR a ~> b
g . InR a ~> b
f = (a ~> b) -> Collage (R a) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR (a ~> b
g (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 ~> b
f)

-- | The collage of a profunctor.
instance (Profunctor p) => CategoryOf (COLLAGE p) where
  type (~>) = Collage
  type Ob a = IsLR a

instance (HasInitialObject j, CategoryOf k, CodiscreteProfunctor p) => HasInitialObject (COLLAGE (p :: k +-> j)) where
  type InitialObject = L InitialObject
  initiate :: forall (a :: COLLAGE p). Ob a => InitialObject ~> a
initiate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @a of
    InL a ~> b
a -> (InitialObject ~> b) -> Collage (L InitialObject) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL ((b ~> b) -> InitialObject ~> b
forall {k} (a' :: k) (a :: k).
HasInitialObject k =>
(a' ~> a) -> InitialObject ~> a
initiate' a ~> b
b ~> b
a)
    InR a ~> b
b -> p InitialObject b -> Collage (L InitialObject) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p InitialObject b
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
anyArr ((Ob b, Ob b) => Collage (L InitialObject) (R b))
-> (b ~> b) -> Collage (L InitialObject) (R 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 ~> b
b ~> b
b

instance (HasTerminalObject k, CategoryOf j, CodiscreteProfunctor p) => HasTerminalObject (COLLAGE (p :: k +-> j)) where
  type TerminalObject = R TerminalObject
  terminate :: forall (a :: COLLAGE p). Ob a => a ~> TerminalObject
terminate @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: COLLAGE p). (CategoryOf (COLLAGE p), Ob a) => Obj a
obj @a of
    InL a ~> b
a -> p b TerminalObject -> Collage (L b) (R TerminalObject)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p b TerminalObject
forall (a :: j) (b :: k). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(CodiscreteProfunctor p, Ob a, Ob b) =>
p a b
anyArr ((Ob b, Ob b) => Collage (L b) (R TerminalObject))
-> (b ~> b) -> Collage (L b) (R TerminalObject)
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
b ~> b
a
    InR a ~> b
b -> (b ~> TerminalObject) -> Collage (R b) (R TerminalObject)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR ((b ~> b) -> b ~> TerminalObject
forall {k} (a :: k) (a' :: k).
HasTerminalObject k =>
(a ~> a') -> a ~> TerminalObject
terminate' a ~> b
b ~> b
b)

class HasArrowCollage p (a :: COLLAGE p) b where arrCoprod :: a ~> b
instance (Thin j, HasArrow (~>) (a :: j) b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) (L a) (L b) where
  arrCoprod :: L a ~> L b
arrCoprod = (a ~> b) -> Collage (L a) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL a ~> b
forall (a :: j) (b :: j). (Ob a, Ob b, HasArrow (~>) a b) => a ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
instance (ThinProfunctor p, HasArrow p a b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) (L a) (R b) where
  arrCoprod :: L a ~> R b
arrCoprod = p a b -> Collage (L a) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p a b
forall (a :: j) (b :: k). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
instance (Thin k, HasArrow (~>) (a :: k) b, Ob a, Ob b) => HasArrowCollage (p :: k +-> j) (R a) (R b) where
  arrCoprod :: R a ~> R b
arrCoprod = (a ~> b) -> Collage (R a) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b, HasArrow (~>) a b) => a ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr

instance (Thin j, Thin k, ThinProfunctor p) => ThinProfunctor (Collage :: CAT (COLLAGE (p :: k +-> j))) where
  type HasArrow (Collage :: CAT (COLLAGE p)) a b = HasArrowCollage p a b
  arr :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(Ob a, Ob b, HasArrow Collage a b) =>
Collage a b
arr = a ~> b
Collage a b
forall {k} {j} (p :: k +-> j) (a :: COLLAGE p) (b :: COLLAGE p).
HasArrowCollage p a b =>
a ~> b
arrCoprod
  withArr :: forall (a :: COLLAGE p) (b :: COLLAGE p) r.
Collage a b -> ((HasArrow Collage a b, Ob a, Ob b) => r) -> r
withArr (InL a ~> b
f) (HasArrow Collage a b, Ob a, Ob b) => r
r = (a ~> b) -> ((HasArrow (Hom j) a b, Ob a, Ob b) => r) -> r
forall (a :: j) (b :: j) r.
(a ~> b) -> ((HasArrow (Hom j) a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr a ~> b
f r
(HasArrow (Hom j) a b, Ob a, Ob b) => r
(HasArrow Collage a b, Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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
f
  withArr (L2R p a b
p) (HasArrow Collage a b, Ob a, Ob b) => r
r = p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: j) (b :: k) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr p a b
p r
(HasArrow p a b, Ob a, Ob b) => r
(HasArrow Collage a b, Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (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
  withArr (InR a ~> b
f) (HasArrow Collage a b, Ob a, Ob b) => r
r = (a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
(a ~> b) -> ((HasArrow (Hom k) a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
withArr a ~> b
f r
(HasArrow (Hom k) a b, Ob a, Ob b) => r
(HasArrow Collage a b, Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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 ~> b
f

data family InjL :: forall (p :: k +-> j) -> j +-> COLLAGE p
instance (Profunctor p) => FunctorForRep (InjL p) where
  type InjL p @ a = L a
  fmap :: forall (a :: j) (b :: j). (a ~> b) -> (InjL p @ a) ~> (InjL p @ b)
fmap = (a ~> b) -> (InjL p @ a) ~> (InjL p @ b)
(a ~> b) -> Collage (L a) (L b)
forall {k} {k} (a :: k) (b :: k) (p :: k +-> k).
(a ~> b) -> Collage (L a) (L b)
InL

data family InjR :: forall (p :: k +-> j) -> k +-> COLLAGE p
instance (Profunctor p) => FunctorForRep (InjR p) where
  type InjR p @ a = R a
  fmap :: forall (a :: j) (b :: j). (a ~> b) -> (InjR p @ a) ~> (InjR p @ b)
fmap = (a ~> b) -> (InjR p @ a) ~> (InjR p @ b)
(a ~> b) -> Collage (R a) (R b)
forall {k} {j} (a :: k) (b :: k) (p :: k +-> j).
(a ~> b) -> Collage (R a) (R b)
InR

collageUniv :: forall {j} {k} (p :: k +-> j). (ThinProfunctor p) => Iso' p (Corep (InjL p) :.: Rep (InjR p))
collageUniv :: forall {j} {k} (p :: k +-> j).
ThinProfunctor p =>
Iso' p (Corep (InjL p) :.: Rep (InjR p))
collageUniv =
  (p ~> (Corep (InjL p) :.: Rep (InjR p)))
-> ((Corep (InjL p) :.: Rep (InjR p)) ~> p)
-> Iso
     p
     p
     (Corep (InjL p) :.: Rep (InjR p))
     (Corep (InjL p) :.: Rep (InjR p))
forall {j} {k} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso
    ((p :~> (Corep (InjL p) :.: Rep (InjR p)))
-> Prof p (Corep (InjL p) :.: Rep (InjR p))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \p a b
p -> ((InjL p @ a) ~> R b) -> Corep (InjL p) a (R b)
forall {j} {k} (a :: j) (f :: j +-> k) (b :: k).
Ob a =>
((f @ a) ~> b) -> Corep f a b
Corep (p a b -> Collage (L a) (R b)
forall {k} {j} (p :: k +-> j) (a :: j) (b :: k).
p a b -> Collage (L a) (R b)
L2R p a b
p) Corep (InjL p) a (R b)
-> Rep (InjR p) (R b) b
-> (:.:) (Corep (InjL p)) (Rep (InjR p)) 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
:.: (R b ~> (InjR p @ b)) -> Rep (InjR p) (R b) b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep R b ~> (InjR p @ b)
Collage (R b) (R b)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: COLLAGE p). Ob a => Collage a a
id ((Ob a, Ob b) => (:.:) (Corep (InjL p)) (Rep (InjR p)) a b)
-> p a b -> (:.:) (Corep (InjL p)) (Rep (InjR p)) a b
forall (a :: j) (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)
    ( ((Corep (InjL p) :.: Rep (InjR p)) :~> p)
-> Prof (Corep (InjL p) :.: Rep (InjR p)) p
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case
        (Corep (L2R p a b
p) :.: Rep (InR a ~> b
r)) -> (b ~> b) -> p a b -> p a b
forall (b :: k) (d :: k) (a :: j). (b ~> d) -> p a b -> p 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 b ~> b
a ~> b
r p a b
p a b
p
        (Corep (InL a ~> b
l) :.: Rep (L2R p a b
p)) -> (a ~> b) -> p b b -> p a b
forall (c :: j) (a :: j) (b :: k). (c ~> a) -> p a b -> p 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 ~> b
a ~> b
l p b b
p a b
p
    )

data family CollageAsCoprod :: COLLAGE (p :: k +-> j) +-> C.COPRODUCT j k
instance (DiscreteProfunctor p) => FunctorForRep (CollageAsCoprod :: COLLAGE (p :: k +-> j) +-> C.COPRODUCT j k) where
  type CollageAsCoprod @ L a = C.L a
  type CollageAsCoprod @ R a = C.R a
  fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(a ~> b) -> (CollageAsCoprod @ a) ~> (CollageAsCoprod @ b)
fmap (InL a ~> b
f) = (a ~> 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)
C.InjL a ~> b
f
  fmap (InR a ~> b
f) = (a ~> 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)
C.InjR a ~> b
f
  fmap (L2R p a b
p) = p a b -> (:++:) (~>) (~>) (L a) (R b)
forall (a :: j) (b :: k) r. p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DiscreteProfunctor p =>
p a b -> r
exfalso p a b
p

data family ProjTo2 :: forall (p :: k +-> j) -> COLLAGE p +-> BOOL
instance (Profunctor p) => FunctorForRep (ProjTo2 p) where
  type ProjTo2 p @ L a = FLS
  type ProjTo2 p @ R a = TRU
  fmap :: forall (a :: COLLAGE p) (b :: COLLAGE p).
(a ~> b) -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
fmap = \case
    InL a ~> b
_ -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
Booleans 'FLS 'FLS
Fls
    InR a ~> b
_ -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
Booleans 'TRU 'TRU
Tru
    L2R p a b
_ -> (ProjTo2 p @ a) ~> (ProjTo2 p @ b)
Booleans 'FLS 'TRU
F2T