content: {-# LANGUAGE KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds, AllowAmbiguousTypes, LambdaCase, DefaultSignatures, EmptyCase #-}
  module Hask.Tensor.Day where
  
  import Hask.Category
  import Hask.Iso
  import Hask.Tensor
  import Prelude ()
  
  --------------------------------------------------------------------------------
  -- * Day Convolution
  --------------------------------------------------------------------------------
  
  class FunctorOf c (->) f => CopresheafOf c f
  instance FunctorOf c (->) f => CopresheafOf c f
  
  data Day (t :: i -> i -> i) (f :: i -> *) (g :: i -> *) (a :: i) where
    Day :: (Dom t ~ c, CopresheafOf c f, CopresheafOf c g, Ob c x, Ob c y)
        => c (t x y) a -> f x -> g y -> Day t f g a
  
  --Day convolution of copresheaves is a copresheaf
  
  instance (Dom t ~ c, CopresheafOf c f, CopresheafOf c g) => Functor (Day t f g) where
    type Dom (Day t f g) = Dom t
    type Cod (Day t f g) = (->)
    fmap c' (Day c fx gy) = Day (c' . c) fx gy
  
  --Day convolution is a bifunctor of copresheaves
  
  instance (Dom t ~ c, CopresheafOf c f) => Functor (Day t f) where
    type Dom (Day t f) = Copresheaves (Dom t)
    type Cod (Day t f) = Copresheaves (Dom t)
    fmap = fmap' where
      fmap' :: Copresheaves c g g' -> Copresheaves c (Day t f g) (Day t f g')
      fmap' (Nat natg) = Nat $ \(Day c fx gy) -> Day c fx (natg gy)
  
  instance (Dom t ~ c, Category c) => Functor (Day t) where
    type Dom (Day t) = Copresheaves (Dom t)
    type Cod (Day t) = Nat (Copresheaves (Dom t)) (Copresheaves (Dom t))
    fmap = fmap' where
      fmap' :: Copresheaves c f f' -> Nat (Copresheaves c) (Copresheaves c) (Day t f) (Day t f')
      fmap' (Nat natf) = Nat $ Nat $ \(Day c fx gy) -> Day c (natf fx) gy
  
  --Day convolution on a monoidal category is associative
  
  instance (Semitensor t, Dom t ~ c, Category c) => Semitensor (Day t) where
    associate = dimap (Nat hither) (Nat yon) where
      hither :: Day t (Day t f g) h a -> Day t f (Day t g h) a
      hither (Day (c' :: c (t b z) a) (Day (c :: c (t x y) b) fx gy) hz) =
        case semitensorClosed :: Dict (Ob c (t y z)) of
          Dict -> case semitensorClosed :: Dict (Ob c (t x (t y z))) of
            Dict -> Day (c' . runNat (fmap c) . beget associate) fx (Day id gy hz)
      yon :: Day t f (Day t g h) a -> Day t (Day t f g) h a
      yon (Day (c' :: c (t x b) a) fx (Day (c :: c (t y z) b) gy hz)) =
        case semitensorClosed :: Dict (Ob c (t x y)) of
          Dict -> case semitensorClosed :: Dict (Ob c (t y z)) of
            Dict -> case semitensorClosed :: Dict (Ob c (t x (t y z))) of
              Dict -> Day (c' . fmap1 c . get associate) (Day id fx gy) hz
  
  --Day convolution on a monoidal category is left & right unital
  
  --type instance (Dom t ~ c, Category c) => I (Day t) = c (I t)
  