Untitled

#line 1 "/tmp/ghc4538.lpp"
{-# LINE 30 "Category.lhs" #-}
#line 1 "./Macros.h"
{-# LINE 29 "Macros.lhs" #-}
{-#  OPTIONS_GHC -fglasgow-exts -fno-implicit-prelude -W -Werror  #-}

module Category where
{-# LINE 37 "Macros.lhs" #-}

{-# LINE 43 "Macros.lhs" #-}

{-# LINE 51 "Macros.lhs" #-}

{-# LINE 57 "Macros.lhs" #-}


#line 2 "/tmp/ghc4538.lpp"

{-# LINE 51 "Category.lhs" #-}
data UnivObjectEquality (eqR :: ((* -> *) -> (* -> *) -> *))
  = UnivObjectEquality
  { univObEqReflexive :: UnivObReflexive eqR
  , univObEqSymmetric :: UnivObSymmetric eqR
  , univObEqTransitive :: UnivObTransitive eqR
  }

type UnivObReflexive (eqR :: ((* -> *) -> (* -> *) -> *))
  = forall (a :: (* -> *)). eqR a a

type UnivObSymmetric (eqR :: ((* -> *) -> (* -> *) -> *))
  = forall (a :: (* -> *)) (b :: (* -> *)). eqR a b -> eqR b a

type UnivObTransitive (eqR :: ((* -> *) -> (* -> *) -> *))
  = forall (a :: (* -> *)) (b :: (* -> *)) (c :: (* -> *)). eqR a b -> eqR b c -> eqR a c
{-# LINE 71 "Category.lhs" #-}
data Equality (eqR :: (* -> * -> *)) (a :: (* -> *)) = Equality
  { eqReflexive :: Reflexive eqR a
  , eqSymmetric :: Symmetric eqR a
  , eqTransitive :: Transitive eqR a
  }

type Reflexive (eqR :: (* -> * -> *)) (a :: (* -> *))
   = forall a1. a a1 -> eqR a1 a1

type Symmetric (eqR :: (* -> * -> *)) (a :: (* -> *))
   = forall a1 a2. a a1 -> a a2 -> eqR a1 a2 -> eqR a2 a1

type Transitive (eqR :: (* -> * -> *)) (a :: (* -> *))
   = forall a1 a2 a3. a a1 -> a a2 -> a a3 -> eqR a1 a2 -> eqR a2 a3 -> eqR a1 a3

type UnivReflexive (eqR :: (* -> * -> *))
   = forall a1. eqR a1 a1

type UnivSymmetric (eqR :: (* -> * -> *))
   = forall a1 a2. eqR a1 a2 -> eqR a2 a1

type UnivTransitive (eqR :: (* -> * -> *))
   = forall a1 a2 a3. eqR a1 a2 -> eqR a2 a3 -> eqR a1 a3

newtype Identity a = Identity {runIdentity :: a}
{-# LINE 118 "Category.lhs" #-}
data LogEq (x :: *) (y :: *) = LogEq (x -> y) (y -> x)

id :: UnivReflexive (->)
id x = x

comp :: UnivTransitive (->)
comp g f x = f (g x)

(.) = (flip comp) :: (b -> c) -> (a -> b) -> a -> c

flip f x y = f y x

logEqUnivReflexive :: UnivReflexive LogEq
logEqUnivReflexive = LogEq id id

logEqUnivSymmetric :: UnivSymmetric LogEq
logEqUnivSymmetric (LogEq xy yx) = LogEq yx xy

logEqUnivTransitive :: UnivTransitive LogEq
logEqUnivTransitive (LogEq xy yx) (LogEq yz zy) = LogEq (yz . xy) (yx . zy)
{-# LINE 147 "Category.lhs" #-}
data Category (ob :: ((* -> *) -> *))
              (objectEquality :: ((* -> *) -> (* -> *) -> *))
              (hom :: ((* -> *) -> (* -> *) -> (* -> * -> *) -> *))
              (morphismEquality :: (* -> * -> *))
              (morphismComposition :: (* -> * -> *) -> (* -> * -> *) -> (* -> * -> *))
              (identityRelation :: (* -> * -> *))
  = Category
  { mtCategoryObjectEquality :: UnivObjectEquality objectEquality
  , mtCategoryMorphismEquality :: Equality morphismEquality (IsAnyRelInstance hom)
  , objectEqualityType :: forall a b. objectEquality a b -> Pair (ob a) (ob b)
  , morphismType :: forall a b pcf. hom a b pcf -> Pair (ob a) (ob b)
  , morphismEqualityType :: forall f g. morphismEquality f g -> MorphismEqualityRes hom f g
  , composeOp :: forall a b c pcf pcg. hom b c pcf -> hom a b pcg -> hom a c (morphismComposition pcf pcg)
  , identityMorphism :: forall a. ob a -> hom a a identityRelation
  , leftIdentityLaw :: forall a b pcf. ob a -> ob b -> morphismEquality
      (hom a b (morphismComposition identityRelation pcf))
      (hom a b pcf)
  , rightIdentityLaw :: forall a b pcf. ob a -> ob b -> morphismEquality
      (hom a b (morphismComposition pcf identityRelation))
      (hom a b pcf)
  }

data IsAnyRelInstance (fn :: ((* -> *) -> (* -> *) -> (* -> * -> *) -> *)) (r :: *)
   = forall a b. IsAnyRelInstance (IsRelInstance (fn a b) r)

data Pair a b = Pair { fst_ :: a, snd_ :: b }

data IsRelInstance (rc :: ((* -> * -> *) -> *)) (r :: *) = forall pcf. IsRelInstance (IdR (rc pcf) r)

data MorphismEqualityRes hom f g = forall a b. MorphismEqualityRes (IsRelInstance (hom a b) f) (IsRelInstance (hom a b) g)
{-# LINE 182 "Category.lhs" #-}
type DthUniverse = Category StdObjects StdUnivObjectEquality Fn FnEq ComposeR IdR

dthUniverse :: DthUniverse
dthUniverse = Category
  { mtCategoryObjectEquality = stdUnivObjectEquality
  , mtCategoryMorphismEquality = fnEq
  , objectEqualityType = \_ -> Pair StdObjects StdObjects
  , morphismType = \_ -> Pair StdObjects StdObjects
  , morphismEqualityType = \(FnEq _) -> MorphismEqualityRes (IsRelInstance IdR) (IsRelInstance IdR)
  , composeOp = compose
  , identityMorphism = \_ -> idFn
  , leftIdentityLaw = \_ _ -> FnEq (\_ _ -> LogEq (\(ComposeR IdR pcf) -> pcf) (ComposeR IdR))
  , rightIdentityLaw = \_ _ -> FnEq (\_ _ -> LogEq (\(ComposeR pcf IdR) -> pcf) (\pcf -> ComposeR pcf IdR))
  }
{-# LINE 210 "Category.lhs" #-}
data StdObjects (o :: (* -> *)) = StdObjects
{-# LINE 218 "Category.lhs" #-}
data StdUnivObjectEquality (a :: (* -> *)) (b :: (* -> *)) where
       StdUnivObjectEquality :: StdUnivObjectEquality a a

stdUnivObjectEquality :: UnivObjectEquality StdUnivObjectEquality
stdUnivObjectEquality = UnivObjectEquality
  { univObEqReflexive = StdUnivObjectEquality
  , univObEqSymmetric = \StdUnivObjectEquality -> StdUnivObjectEquality
  , univObEqTransitive = \StdUnivObjectEquality StdUnivObjectEquality -> StdUnivObjectEquality
  }
{-# LINE 244 "Category.lhs" #-}
type FnImpl (a :: (* -> *)) (b :: (* -> *)) (pc :: (* -> * -> *)) = PrImp a (FnRes b pc)

newtype Fn (a :: (* -> *)) (b :: (* -> *)) (pc :: (* -> * -> *)) = Fn (FnImpl a b pc)

--  FnRes is short for function result
--  FnRes b pc a1 = exists b1. pc a1 b1 && b b1
data FnRes (b :: (* -> *)) (pc :: (* -> * -> *)) (a1 :: *) = forall (b1 :: *). FnRes (pc a1 b1) (b b1)

--  Predicate implication
type PrImp p q = forall (b1 :: *). p b1 -> q b1
{-# LINE 267 "Category.lhs" #-}
data FnEq (f :: *) (g :: *) where
       FnEq :: (forall a1 b1. a a1 -> b b1 -> LogEq (pc1 a1 b1) (pc2 a1 b1))
            -> FnEq (Fn a b pc1) (Fn a b pc2)

fnEq :: Equality FnEq (IsAnyRelInstance Fn)
fnEq = Equality
  { eqReflexive = \(IsAnyRelInstance (IsRelInstance IdR)) -> FnEq (\_ _ -> logEqUnivReflexive)
  , eqSymmetric = \(IsAnyRelInstance (IsRelInstance IdR)) (IsAnyRelInstance (IsRelInstance IdR)) (FnEq eqAt)
    -> FnEq (logEqUnivSymmetric |<<| eqAt)
  , eqTransitive = \(IsAnyRelInstance (IsRelInstance IdR)) (IsAnyRelInstance (IsRelInstance IdR))
                    (IsAnyRelInstance (IsRelInstance IdR)) (FnEq eq1At) (FnEq eq2At)
    -> FnEq (\a1 b1 -> logEqUnivTransitive (eq1At a1 b1) (eq2At a1 b1))
  }

(|<<|) = (.) . (.)
{-# LINE 303 "Category.lhs" #-}
data ComposeR (pcf :: * -> * -> *) (pcg :: * -> * -> *) (a1 :: *) (c1 :: *) where
        ComposeR :: pcf b1 c1 -> pcg a1 b1 -> ComposeR pcf pcg a1 c1

compose :: Fn b c pcf -> Fn a b pcg -> Fn a c (ComposeR pcf pcg)
compose (Fn f) (Fn g) = Fn (\a -> case g a of (FnRes gab b) -> case f b of (FnRes fbc c) -> FnRes (ComposeR fbc gab) c)
{-# LINE 324 "Category.lhs" #-}
data IdR (a :: *) (b :: *) where
     IdR :: IdR a a

idFn :: Fn a a IdR
idFn = Fn (FnRes IdR)
{-# LINE 334 "Category.lhs" #-}
type Functor c d cHom dHom pcSub ret
  = forall a b. Fn (Hom cHom a b)
    (Hom dHom (ret a) (ret b))
    (FunctorPC c d cHom dHom a b pcSub ret)

data Hom hom a b h where
  Hom :: hom a b pc -> Hom hom a b (hom a b pc)

data FunctorPC c d cHom dHom a b pcSub ret g r where
{-# LINE 351 "Category.lhs" #-}
  FunctorPC ::
     Category cOb cObEq cHom cHomEq cHomComp cId
{-# LINE 357 "Category.lhs" #-}
    -> Category dOb dObEq dHom dHomEq dHomComp dId
{-# LINE 362 "Category.lhs" #-}
    -> dHomEq (dHom (ret a) (ret a) dId) (dHom (ret a) (ret a) (pcSub a a cId))
{-# LINE 367 "Category.lhs" #-}
    -> (cOb e
    -> dHomEq (dHom (ret a) (ret e) (dHomComp (pcSub a b pcg) (pcSub b e pch)))
              (dHom (ret a) (ret e) (pcSub a e (cHomComp pcg pch))))

    -> FunctorPC (Category cOb cObEq cHom cHomEq cHomComp cId) (Category dOb dObEq dHom dHomEq dHomComp dId) cHom dHom a b pcSub ret (cHom a b pcg) (dHom (ret a) (ret b) (pcSub a b pcg))
{-# LINE 379 "Category.lhs" #-}
type UnivFunctor pcSub ret
  = forall a b. Fn (Hom Fn a b)
    (Hom Fn (ret a) (ret b))
    (UnivFunctorPC a b pcSub ret)

data UnivFunctorPC a b pcSub ret g r where
  UnivFunctorPC ::
{-# LINE 390 "Category.lhs" #-}
    FnEq (Fn (ret a) (ret a) IdR) (Fn (ret a) (ret a) (pcSub a a IdR))
{-# LINE 395 "Category.lhs" #-}
    -> FnEq (Fn (ret a) (ret e) (ComposeR (pcSub a b pcg) (pcSub b e pch)))
              (dHom (ret a) (ret e) (pcSub a e (ComposeR pcg pch)))

    -> UnivFunctorPC a b pcSub ret (Fn a b pcg) (Fn (ret a) (ret b) (pcSub a b pcg))
{-# LINE 403 "Category.lhs" #-}
univFunctorToFunctor :: UnivFunctor pcSub ret -> Functor DthUniverse DthUniverse Fn Fn pcSub ret
univFunctorToFunctor uf = Fn (foo uf)

foo :: UnivFunctor pcSub ret
 -> FnImpl (Hom Fn a b)
    (Hom Fn (ret a) (ret b))
    (FunctorPC DthUniverse DthUniverse Fn Fn a b pcSub ret)
foo (Fn uf) gab = case uf gab of
      FnRes (UnivFunctorPC idLaw compLaw) r
        -> FnRes (FunctorPC dthUniverse dthUniverse idLaw compLaw) r