{-# LANGUAGE ImpredicativeTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Three Parameter Functors of arbitrary varience.
module Kindly.Trifunctor
  ( Trifunctor,
    trimap,
  )
where

--------------------------------------------------------------------------------

import Control.Category
import Data.Kind (Constraint, Type)
import Kindly.Bifunctor ()
import Kindly.Class

--------------------------------------------------------------------------------

-- | A 'CategoricalFunctor' of kind @Type -> Type -> Type@ mapping from an
-- arbitrary category @cat1@ to a functor category @cat2 ~> cat3 ~> (->)@.
type Trifunctor :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> (Type -> Type -> Type) -> (Type -> Type -> Type -> Type) -> Constraint
type Trifunctor cat1 cat2 cat3 p = (MapArg3 cat3 cat2 cat1 p, forall x. MapArg2 cat2 cat1 (p x), forall x y. MapArg1 cat1 (p x y))

-- | Lift a morphism @cat1 a a'@, a morphism @cat2 b b'@, and a morphism @cat3 c c'@ into a -- function @p a b c -> p a' b' c'@.
trimap :: forall cat1 cat2 cat3 p. (Trifunctor cat1 cat2 cat3 p) => forall a b c a' b' c'. (a `cat3` a') -> (b `cat2` b') -> (c `cat1` c') -> p a b c -> p a' b' c'
trimap :: forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (cat3 :: * -> * -> *) (p :: * -> * -> * -> *) a b c a' b' c'.
Trifunctor cat1 cat2 cat3 p =>
cat3 a a' -> cat2 b b' -> cat1 c c' -> p a b c -> p a' b' c'
trimap cat3 a a'
f cat2 b b'
g cat1 c c'
h = cat3 a a' -> forall x y. p a x y -> p a' x y
forall a b. cat3 a b -> forall x y. p a x y -> p b x y
forall {from} {s} {s1} (cat1 :: Cat from) (cat2 :: Cat s)
       (cat3 :: Cat s1) (p :: from -> s -> s1 -> *) (a :: from)
       (b :: from).
MapArg3 cat1 cat2 cat3 p =>
cat1 a b -> forall (x :: s) (y :: s1). p a x y -> p b x y
map3 cat3 a a'
f (p a b' c' -> p a' b' c')
-> (p a b c -> p a b' c') -> p a b c -> p a' b' c'
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {from} {s} (cat1 :: Cat from) (cat2 :: Cat s)
       (p :: from -> s -> *) (a :: from) (b :: from).
MapArg2 cat1 cat2 p =>
cat1 a b -> forall (x :: s). p a x -> p b x
forall (cat1 :: * -> * -> *) (cat2 :: * -> * -> *)
       (p :: * -> * -> *) a b.
MapArg2 cat1 cat2 p =>
cat1 a b -> forall x. p a x -> p b x
map2 @_ @cat1 cat2 b b'
g (p a b c' -> p a b' c')
-> (p a b c -> p a b c') -> p a b c -> p a b' c'
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. cat1 c c' -> p a b c -> p a b c'
forall a b. cat1 a b -> p a b a -> p a b b
forall {from} (cat1 :: Cat from) (p :: from -> *) (a :: from)
       (b :: from).
MapArg1 cat1 p =>
cat1 a b -> p a -> p b
map1 cat1 c c'
h

--------------------------------------------------------------------------------

instance CategoricalFunctor (,,) where
  type Dom (,,) = (->)
  type Cod (,,) = (->) ~> (->) ~> (->)

  map :: (a -> b) -> ((->) ~> (->) ~> (->)) ((,,) a) ((,,) b)
  map :: forall a b. (a -> b) -> (~>) (->) ((->) ~> (->)) ((,,) a) ((,,) b)
map a -> b
f = (forall x. (~>) (->) (->) ((,,) a x) ((,,) b x))
-> Nat (->) ((->) ~> (->)) ((,,) a) ((,,) b)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat ((forall x. (a, x, x) -> (b, x, x))
-> Nat (->) (->) ((,,) a x) ((,,) b x)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat (\(a
x, x
y, x
z) -> (a -> b
f a
x, x
y, x
z)))

instance CategoricalFunctor ((,,,) x) where
  type Dom ((,,,) x) = (->)
  type Cod ((,,,) x) = (->) ~> (->) ~> (->)

  map :: (a -> b) -> ((->) ~> (->) ~> (->)) ((,,,) x a) ((,,,) x b)
  map :: forall a b.
(a -> b) -> (~>) (->) ((->) ~> (->)) ((,,,) x a) ((,,,) x b)
map a -> b
f = (forall x. (~>) (->) (->) ((,,,) x a x) ((,,,) x b x))
-> Nat (->) ((->) ~> (->)) ((,,,) x a) ((,,,) x b)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat ((forall x. (x, a, x, x) -> (x, b, x, x))
-> Nat (->) (->) ((,,,) x a x) ((,,,) x b x)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat (\(x
a, a
b, x
c, x
d) -> (x
a, a -> b
f a
b, x
c, x
d)))

instance CategoricalFunctor ((,,,,) x x') where
  type Dom ((,,,,) x x') = (->)
  type Cod ((,,,,) x x') = (->) ~> (->) ~> (->)

  map :: (a -> b) -> ((->) ~> (->) ~> (->)) ((,,,,) x x' a) ((,,,,) x x' b)
  map :: forall a b.
(a -> b)
-> (~>) (->) ((->) ~> (->)) ((,,,,) x x' a) ((,,,,) x x' b)
map a -> b
f = (forall x. (~>) (->) (->) ((,,,,) x x' a x) ((,,,,) x x' b x))
-> Nat (->) ((->) ~> (->)) ((,,,,) x x' a) ((,,,,) x x' b)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat ((forall x. (x, x', a, x, x) -> (x, x', b, x, x))
-> Nat (->) (->) ((,,,,) x x' a x) ((,,,,) x x' b x)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat (\(x
a, x'
b, a
c, x
d, x
e) -> (x
a, x'
b, a -> b
f a
c, x
d, x
e)))

instance CategoricalFunctor ((,,,,,) x x' x'') where
  type Dom ((,,,,,) x x' x'') = (->)
  type Cod ((,,,,,) x x' x'') = (->) ~> (->) ~> (->)

  map :: (a -> b) -> ((->) ~> (->) ~> (->)) ((,,,,,) x x' x'' a) ((,,,,,) x x' x'' b)
  map :: forall a b.
(a -> b)
-> (~>)
     (->) ((->) ~> (->)) ((,,,,,) x x' x'' a) ((,,,,,) x x' x'' b)
map a -> b
f' = (forall x.
 (~>) (->) (->) ((,,,,,) x x' x'' a x) ((,,,,,) x x' x'' b x))
-> Nat
     (->) ((->) ~> (->)) ((,,,,,) x x' x'' a) ((,,,,,) x x' x'' b)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat ((forall x. (x, x', x'', a, x, x) -> (x, x', x'', b, x, x))
-> Nat (->) (->) ((,,,,,) x x' x'' a x) ((,,,,,) x x' x'' b x)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat (\(x
a, x'
b, x''
c, a
d, x
e, x
f) -> (x
a, x'
b, x''
c, a -> b
f' a
d, x
e, x
f)))

instance CategoricalFunctor ((,,,,,,) x x' x'' x''') where
  type Dom ((,,,,,,) x x' x'' x''') = (->)
  type Cod ((,,,,,,) x x' x'' x''') = (->) ~> (->) ~> (->)

  map :: (a -> b) -> ((->) ~> (->) ~> (->)) ((,,,,,,) x x' x'' x''' a) ((,,,,,,) x x' x'' x''' b)
  map :: forall a b.
(a -> b)
-> (~>)
     (->)
     ((->) ~> (->))
     ((,,,,,,) x x' x'' x''' a)
     ((,,,,,,) x x' x'' x''' b)
map a -> b
f' = (forall x.
 (~>)
   (->)
   (->)
   ((,,,,,,) x x' x'' x''' a x)
   ((,,,,,,) x x' x'' x''' b x))
-> Nat
     (->)
     ((->) ~> (->))
     ((,,,,,,) x x' x'' x''' a)
     ((,,,,,,) x x' x'' x''' b)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat ((forall x.
 (x, x', x'', x''', a, x, x) -> (x, x', x'', x''', b, x, x))
-> Nat
     (->) (->) ((,,,,,,) x x' x'' x''' a x) ((,,,,,,) x x' x'' x''' b x)
forall {t} {s} (target :: Cat t) (f :: s -> t) (g :: s -> t)
       (source :: Cat s).
(forall (x :: s). target (f x) (g x)) -> Nat source target f g
Nat (\(x
a, x'
b, x''
c, x'''
d, a
e, x
f, x
g) -> (x
a, x'
b, x''
c, x'''
d, a -> b
f' a
e, x
f, x
g)))

--------------------------------------------------------------------------------

instance MapArg3 (->) (->) (->) (,,)

instance MapArg3 (->) (->) (->) ((,,,) x)

instance MapArg3 (->) (->) (->) ((,,,,) x x')

instance MapArg3 (->) (->) (->) ((,,,,,) x x' x'')

instance MapArg3 (->) (->) (->) ((,,,,,,) x x' x'' x''')