{-# LANGUAGE AllowAmbiguousTypes #-}

module Pandora.Pattern.Functor.Covariant where

import Pandora.Pattern.Betwixt (Betwixt)
import Pandora.Pattern.Semigroupoid (Semigroupoid)

infixl 4 <-|-, <!>
infixl 3 <-|-|-, <!!>
infixl 2 <-|-|-|-, <!!!>

{- |
> When providing a new instance, you should ensure it satisfies:
> * Identity morphism: (identity <-|-) ≡ identity
> * Interpreted of morphisms: (f . g <-|-) ≡ (f <-|-) . (g <-|-)
-}

class (Semigroupoid source, Semigroupoid target) => Covariant source target t where
	(<-|-) :: source a b -> target (t a) (t b)

	(<-|-|-) :: (Covariant source (Betwixt source target) u, Covariant (Betwixt source target) target t)
		=> source a b -> target (t (u a)) (t (u b))
	(<-|-|-) source a b
s = (Betwixt source target (u a) (u b) -> target (t (u a)) (t (u b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) (source a b -> Betwixt source target (u a) (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) @source @(Betwixt source target) @_ source a b
s))

	(<-|-|-|-) :: (Covariant source (Betwixt source (Betwixt source target)) v, Covariant (Betwixt source (Betwixt source target)) (Betwixt (Betwixt source target) target) u, Covariant (Betwixt (Betwixt source target) target) target t)
		=> source a b -> target (t (u (v a))) (t (u (v b)))
	(<-|-|-|-) source a b
s = (Betwixt (Betwixt source target) target (u (v a)) (u (v b))
-> target (t (u (v a))) (t (u (v b)))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) @(Betwixt (Betwixt source target) target) @target (Betwixt source (Betwixt source target) (v a) (v b)
-> Betwixt (Betwixt source target) target (u (v a)) (u (v b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) @(Betwixt source (Betwixt source target)) @(Betwixt (Betwixt source target) target) @_ (source a b -> Betwixt source (Betwixt source target) (v a) (v b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-) @source @(Betwixt source (Betwixt source target)) @_ source a b
s)))

(<!>) :: Covariant source target t => source a b -> target (t a) (t b)
<!> :: source a b -> target (t a) (t b)
(<!>) = source a b -> target (t a) (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<-|-)

(<!!>) :: (Covariant source target t, Covariant source (Betwixt source target) u, Covariant (Betwixt source target) target t) => source a b -> target (t (u a)) (t (u b))
<!!> :: source a b -> target (t (u a)) (t (u b))
(<!!>) = source a b -> target (t (u a)) (t (u b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
(<-|-|-)

(<!!!>) :: (Covariant source target t, Covariant source (Betwixt source (Betwixt source target)) v, Covariant (Betwixt source (Betwixt source target)) (Betwixt (Betwixt source target) target) u, Covariant (Betwixt (Betwixt source target) target) target t)
	=> source a b -> target (t (u (v a))) (t (u (v b)))
<!!!> :: source a b -> target (t (u (v a))) (t (u (v b)))
(<!!!>) source a b
s = source a b -> target (t (u (v a))) (t (u (v b)))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (v :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source (Betwixt source target)) v,
 Covariant
   (Betwixt source (Betwixt source target))
   (Betwixt (Betwixt source target) target)
   u,
 Covariant (Betwixt (Betwixt source target) target) target t) =>
source a b -> target (t (u (v a))) (t (u (v b)))
(<-|-|-|-) source a b
s