-- This file:
-- http://angg.twu.net/IDRIS/Protocats.idr.html
-- http://angg.twu.net/IDRIS/Protocats.idr
--  (find-angg        "IDRIS/Protocats.idr")

-- See:
-- http://angg.twu.net/math-b.html#idarct
-- http://angg.twu.net/LATEX/idarct-preprint.pdf
--      (find-angg ".emacs" "idarct-preprint")
-- (find-idarctpage 27 "19. The syntactical world")
-- (find-idarcttext 27 "19. The syntactical world")

-- (find-es "idris" "idris-ct")
-- (find-idrisctfile "src/Basic/Category.lidr" "Summing up")

record ProtoCategory where
  constructor MkProtoCategory
  obj           : Type
  mor           : obj -> obj -> Type
  identity      : (a : obj) -> mor a a
  compose       : (a, b, c : obj)
               -> (f : mor a b)
               -> (g : mor b c)
               -> mor a c

-- (find-idrisctfile "src/Basic/Functor.lidr" "in its entirety")
--
record ProtoFunctor (cat1 : ProtoCategory) (cat2 : ProtoCategory) where
  constructor MkProtoFunctor
  mapObj          : obj cat1 -> obj cat2
  mapMor          : (a, b : obj cat1)
                 -> mor cat1 a b
                 -> mor cat2 (mapObj a) (mapObj b)

idProtoFunctor : (cat : ProtoCategory) -> ProtoFunctor cat cat
idProtoFunctor cat = MkProtoFunctor
  id
  (\a, b => id)

protoFunctorComposition :
     (cat1, cat2, cat3 : ProtoCategory)
  -> ProtoFunctor cat1 cat2
  -> ProtoFunctor cat2 cat3
  -> ProtoFunctor cat1 cat3
protoFunctorComposition cat1 cat2 cat3 fun1 fun2 = MkProtoFunctor
  ((mapObj fun2) . (mapObj fun1))
  (\a, b => (mapMor fun2 (mapObj fun1 a) (mapObj fun1 b)) . (mapMor fun1 a b))

-- (find-idrisctfile "src/Basic/Isomorphism.lidr" "record Isomorphism")
--
record ProtoIsomorphism (cat : ProtoCategory) (a : obj cat) (b : obj cat)
                        (morphism : mor cat a b) where
  constructor MkProtoIsomorphism
  Inverse: mor cat b a
  -- lawleft: compose cat a b a morphism Inverse = identity cat a
  -- lawright: compose cat b a b Inverse morphism = identity cat b


-- (find-idrisctfile "src/Basic/NaturalTransformation.lidr")
--
record ProtoNaturalTransformation
  (cat1 : ProtoCategory)
  (cat2 : ProtoCategory)
  (fun1 : ProtoFunctor cat1 cat2)
  (fun2 : ProtoFunctor cat1 cat2)
  where
    constructor MkProtoNaturalTransformation
    component : (a : obj cat1) -> mor cat2 (mapObj fun1 a) (mapObj fun2 a)

protoNaturalTransformationComposition :
     (cat1, cat2 : ProtoCategory)
  -> (fun1, fun2, fun3 : ProtoFunctor cat1 cat2)
  -> ProtoNaturalTransformation cat1 cat2 fun1 fun2
  -> ProtoNaturalTransformation cat1 cat2 fun2 fun3
  -> ProtoNaturalTransformation cat1 cat2 fun1 fun3
protoNaturalTransformationComposition cat1 cat2 fun1 fun2 fun3 natTrans1 natTrans2 =
    MkProtoNaturalTransformation
      (\a => compose cat2 (mapObj fun1 a) (mapObj fun2 a) (mapObj fun3 a) (component natTrans1 a) (component natTrans2 a))

{-

composeFunctorNatTrans :
     (cat1, cat2, cat3 : Category)
  -> (fun1, fun2 : CFunctor cat1 cat2)
  -> NaturalTransformation cat1 cat2 fun1 fun2
  -> (fun3 : CFunctor cat2 cat3)
  -> NaturalTransformation cat1 cat3
     (functorComposition cat1 cat2 cat3 fun1 fun3)
     (functorComposition cat1 cat2 cat3 fun2 fun3)
composeFunctorNatTrans _ _ cat3 fun1 fun2 natTrans fun3 =
  MkNaturalTransformation
    (\a => mapMor fun3 (mapObj fun1 a) (mapObj fun2 a) (component natTrans a))

composeNatTransFunctor :
     (cat1, cat2, cat3 : Category)
  -> (fun1 : CFunctor cat1 cat2)
  -> (fun2, fun3 : CFunctor cat2 cat3)
  -> NaturalTransformation cat2 cat3 fun2 fun3
  -> NaturalTransformation cat1 cat3
    (functorComposition cat1 cat2 cat3 fun1 fun2)
    (functorComposition cat1 cat2 cat3 fun1 fun3)
composeNatTransFunctor _ _ _ fun1 _ _ natTrans = MkNaturalTransformation
  (\a => component natTrans (mapObj fun1 a))
  (\a, b, f => commutativity natTrans _ _ (mapMor fun1 a b f))

-- (find-idrisctfile "src/Basic/NaturalIsomorphism.lidr")

record ProtoNaturalIsomorphism
  (cat1 : ProtoCategory)
  (cat2 : ProtoCategory)
  (fun1 : ProtoFunctor cat1 cat2)
  (fun2 : ProtoFunctor cat1 cat2)
where
  constructor MkProtoNaturalIsomorphism
  natTrans : NaturalTransformation cat1 cat2 fun1 fun2
  isIso    : (a : obj cat1) -> Isomorphism cat2 (mapObj fun1 a) (mapObj fun2 a) (component natTrans a)

-}