content: {-# LANGUAGE KindSignatures, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, ConstraintKinds, NoImplicitPrelude, TypeFamilies, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables, DataKinds #-}
  module Lame where
  
  import Data.Constraint (Constraint, (:-)(Sub), Dict(..), (\\), Class(cls), (:=>)(ins))
  import qualified Data.Constraint as Constraint
  import Data.Type.Coercion (Coercion(..))
  import qualified Data.Type.Coercion as Coercion
  import GHC.Prim (Any)
  import Prelude (($))
  
  type family Dom  (f :: i -> j)      :: i -> i -> *
  type family Cod  (f :: i -> j)      :: j -> j -> *
  type family Dom2 (f :: i -> j -> k) :: j -> j -> *
  type family Cod2 (f :: i -> j -> k) :: k -> k -> *
  
  --------------------------------------------------------------------------------
  -- * Categories
  --------------------------------------------------------------------------------
  
  class Discrete' f where
    ob :: Ob (Dom f) a :- Ob (Cod f) (f a)
  
  class Discrete' f => Functor' f where
    fmap :: Dom f a b -> Cod f (f a) (f b)
  
  class Discrete' f => Contravariant' f where
    contramap :: Dom f a b -> Cod f (f b) (f a)
  
  class (Functor' f, Contravariant' f) => Phantom' f
  instance (Functor' f, Contravariant' f) => Phantom' f
  
  class Profunctor' p where
    dimap :: Dom p a b -> Dom2 p c d -> Cod2 p (p b c) (p a d)
  
  type Iso s t a b = forall p. Profunctor p => Cod2 p (p a b) (p s t)
  
  class Bifunctor' p where
    bimap :: Dom p a b -> Dom2 p c d -> Cod2 p (p a c) (p b d)
  
  class Category' (p :: i -> i -> *) where
    type Ob p :: i -> Constraint
    id  :: Ob p a => p a a
    -- equiv  :: Coercible a b => p a b
    observe :: p a b -> Dict (Ob p a, Ob p b)
    (.) :: p b c -> p a b -> p a c
  
  --------------------------------------------------------------------------------
  -- * Circular Definition, See Definition, Circular
  --------------------------------------------------------------------------------
  
  class (Discrete' f, Category' (Dom f), Category' (Cod f)) => Discrete f
  instance (Discrete' f, Category' (Dom f), Category' (Cod f)) => Discrete f
  
  class (Contravariant' f, Category' (Dom f), Category' (Cod f)) => Contravariant f
  instance (Contravariant' f, Category' (Dom f), Category' (Cod f)) => Contravariant f
  
  class (Functor' f, Category' (Dom f), Category' (Cod f)) => Functor f
  instance (Functor' f, Category' (Dom f), Category' (Cod f)) => Functor f
  
  class (Phantom' f, Category' (Dom f), Category' (Cod f)) => Phantom f
  instance (Phantom' f, Category' (Dom f), Category' (Cod f)) => Phantom f
  
  class (Profunctor' p, Contravariant' p, Category' (Cod p), Category' (Dom p), Category' (Dom2 p), Category' (Cod2 p)) => Profunctor p -- explicitly Contravariant
  instance (Profunctor' p, Contravariant' p, Category (Cod p), Category' (Dom p), Category' (Dom2 p), Category' (Cod2 p)) => Profunctor p
  
  class (Bifunctor' p, Functor' p, Category' (Cod p), Category' (Dom p), Category' (Dom2 p), Category' (Cod2 p)) => Bifunctor p -- explicit Functor
  instance (Bifunctor' p, Functor' p, Category' (Cod p), Category' (Dom p), Category' (Dom2 p), Category' (Cod2 p)) => Bifunctor p
  
  class (Category' p, Profunctor' p, Dom p ~ p, Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->), Phantom' (Ob p)) => Category p
  instance (Category' p, Profunctor' p, Dom p ~ p, Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->), Phantom' (Ob p)) => Category p
  
  class Vacuous (c :: i -> i -> *) (a :: i)
  instance Vacuous (c :: i -> i -> *) (a :: i)
  
  type instance Dom (Vacuous c) = c
  type instance Cod (Vacuous c) = (:-)
  
  instance Discrete' (Vacuous c) where
    ob = Sub Dict
  
  instance Functor' (Vacuous c) where
    fmap _ = Sub Dict
  
  instance Contravariant' (Vacuous c) where
    contramap _ = Sub Dict
  
  --------------------------------------------------------------------------------
  -- * Constraint
  --------------------------------------------------------------------------------
  
  type instance Dom (:-)    = (:-)
  type instance Cod (:-)    = Nat (:-) (->) -- copresheaves
  type instance Dom2 (:-)   = (:-)
  type instance Dom ((:-)a) = (:-)
  type instance Cod2 (:-)   = (->)
  type instance Cod ((:-)a) = (->)
  
  instance Discrete' (:-) where ob = Sub Dict
  instance Contravariant' (:-) where contramap f = Nat (. f)
  instance Profunctor' (:-) where dimap f g h = g . h . f
  instance Discrete' ((:-) b) where ob = Sub Dict
  instance Functor' ((:-) b) where fmap = (.)
  
  instance Category' (:-) where
    type Ob (:-) = Vacuous (:-)
    id = Constraint.refl
    observe _ = Dict
    (.) = Constraint.trans
  
  constraint :: Dict (Category (:-))
  constraint = Dict
  
  --------------------------------------------------------------------------------
  -- * Hask
  --------------------------------------------------------------------------------
  
  type instance Dom (->)    = (->)
  type instance Cod (->)    = Nat (->) (->) -- copresheaves
  type instance Dom2 (->)   = (->)
  type instance Dom ((->)a) = (->)
  type instance Cod2 (->)   = (->)
  type instance Cod ((->)a) = (->)
  
  instance Discrete' (->) where ob = Sub Dict
  instance Contravariant' (->) where contramap f = Nat (. f)
  instance Discrete' ((->) b) where ob = Sub Dict
  instance Functor' ((->) b) where fmap = (.)
  instance Profunctor' (->) where dimap f g h = g . h . f
  
  instance Category' (->) where
    type Ob (->) = Vacuous (->)
    id x = x
    observe _ = Dict
    (.) f g x = f (g x)
  
  hask :: Dict (Category (->))
  hask = Dict
  
  --------------------------------------------------------------------------------
  -- * Op
  --------------------------------------------------------------------------------
  
  {-
  type family Op (p :: i -> j -> *) :: j -> i -> * where
    Op (Op1 p) = p
    Op = Op1
  -}
  
  newtype Op (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b a }
  
  -- Op :: Prof^op -> Prof
  type instance Dom (Op p)   = Op (Dom p)
  type instance Cod (Op p)   = Nat (Op (Dom p)) (->)
  type instance Dom (Op p a) = Op (Dom p)
  type instance Dom2 (Op p)  = Op (Dom p)
  type instance Cod2 (Op p)  = (->)
  type instance Cod (Op p a) = (->)
  
  instance Category p => Discrete' (Op p) where ob = Sub Dict
  instance Category p => Contravariant' (Op p) where contramap pab = Nat (. pab)
  instance Category p => Profunctor' (Op p) where dimap (Op f) (Op g) (Op h) = Op (dimap g f h)
  instance Discrete' (Op p a) where ob = Sub Dict 
  instance Category p => Functor' (Op p a) where fmap = (.)
  instance Category p => Category' (Op p) where
    type Ob (Op p) = Ob p
    id = Op id
    Op f . Op g = Op (g . f)
    observe (Op f) = case observe f of
      Dict -> Dict
  
  op :: Category p => Dict (Category (Op p))
  op = Dict
  
  
  --------------------------------------------------------------------------------
  -- * Nat
  --------------------------------------------------------------------------------
  
  data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where
    Nat :: (Functor' f, Dom f ~ p, Cod f ~ q, Functor' g, Dom g ~ p, Cod g ~ q) => { runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g
  
  type instance Dom (Nat p q)   = Nat p q
  type instance Cod (Nat p q)   = Nat (Nat p q) (->)
  type instance Dom2 (Nat p q)  = Nat p q
  type instance Cod2 (Nat p q)  = (->)
  type instance Dom (Nat p q f) = Nat p q
  type instance Cod (Nat p q f) = (->)
  
  type Copresheaves p = Nat p (->)
  type Presheaves p = Nat (Op p) (->)
  
  type instance Dom (FunctorOf p q) = Nat p q
  type instance Cod (FunctorOf p q) = (:-)
  
  class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
  instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
  
  instance Discrete' (FunctorOf p q) where
    ob = Sub Dict
    
  instance (Category' p, Category' q) => Functor' (FunctorOf p q) where
    fmap Nat{} = Sub Dict
  
  instance (Category' p, Category' q) => Contravariant' (FunctorOf p q) where
    contramap Nat{} = Sub Dict
  
  instance (Category' p, Category q) => Profunctor' (Nat p q) where
    dimap (Nat f) (Nat g) (Nat h) = Nat (dimap f g h)
  
  instance (Category' p, Category' q) => Category' (Nat p q) where
     type Ob (Nat p q) = FunctorOf p q
     id = Nat id1 where
       id1 :: forall f x. (Discrete' f, Dom f ~ p, Cod f ~ q, Ob p x) => q (f x) (f x)
       id1 = id \\ (ob :: Ob p x :- Ob q (f x))
     observe Nat{} = Dict
     Nat f . Nat g = Nat (f . g)
  
  nat :: (Category p, Category q) => Dict (Category (Nat p q))
  nat = Dict
  
  --------------------------------------------------------------------------------
  -- * Pronat
  --------------------------------------------------------------------------------
  
  -- 2-morphisms in Prof are natural in both arguments, but the former is contravariant and the latter is covariant in our 'backwards' encoding
  data Pronat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j -> *) (g :: i -> j -> *) where
    Pronat :: (Profunctor' f, Dom f ~ p, Dom2 f ~ q, Profunctor' g, Dom g ~ p, Dom2 g ~ q) => { runPronat :: forall a b. (Ob p a, Ob q b) => f a b -> g a b } -> Pronat p q f g
  
  type instance Dom  (Pronat p q) = Pronat p q
  type instance Cod  (Pronat p q) = Nat (Pronat p q) (->)
  type instance Dom2 (Pronat p q) = Pronat p q
  type instance Cod2 (Pronat p q) = (->)
  type instance Dom  (Pronat p q f) = Pronat p q
  type instance Cod  (Pronat p q f) = (->)
  
  type instance Dom (ProfunctorOf p q) = Pronat p q
  type instance Cod (ProfunctorOf p q) = (:-)
  
  class    (Functor f, Dom f ~ p, Dom2 f ~ q, Cod2 f ~ (->)) => ProfunctorOf p q f
  instance (Functor f, Dom f ~ p, Dom2 f ~ q, Cod2 f ~ (->)) => ProfunctorOf p q f
  
  data Prof (p :: j -> k -> *) (q :: i -> j -> *) (a :: i) (b :: k) where
    Prof :: p x b -> q a x -> Prof p q a b
  
  instance Discrete
  
  