{-# LANGUAGE AllowAmbiguousTypes #-}
module Proarrow.Category.Double where
import Data.Kind (Type)
import Proarrow.Core (CategoryOf(..), CAT, UN)
import Proarrow.Category.Bicategory (Path(..), type (+++), Bicategory(..), Fold, Strictified (..), appendObj, IsPath (..))
import Proarrow.Object (Obj)
import Proarrow.Category.Bicategory.Op (OPK(OP), Op (..))
import Proarrow.Category.Bicategory.Co (COK(CO), Co (..), splitFoldCo, concatFoldCo)
import Prelude (($))
infixl 6 |||
infixl 5 ===
type SQ1 (hk :: CAT c) (vk :: CAT c) = forall {h} {i} {j} {k}. hk h j -> hk i k -> vk h i -> vk j k -> Type
type SQ (hk :: CAT c) (vk :: CAT c) = SQ1 (Path hk) (Path vk)
class (Bicategory hk, Bicategory vk) => Double hk vk where
data Sq hk vk :: SQ hk vk
data Sq1 hk vk :: SQ1 hk vk
singleton :: (DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k, Ob (p :: hk h j), Ob (q :: hk i k), Ob (f :: vk h i), Ob (g :: vk j k)) =>
Sq1 hk vk p q f g -> Sq hk vk (p ::: Nil) (q ::: Nil) (f ::: Nil) (g ::: Nil)
folded :: (DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k, Ob (ps :: Path hk h j), Ob (qs :: Path hk i k), Ob (fs :: Path vk h i), Ob (gs :: Path vk j k)) =>
Sq hk vk ps qs fs gs -> Sq1 hk vk (Fold ps) (Fold qs) (Fold fs) (Fold gs)
object :: DOb hk vk k => Sq hk vk (Nil :: Path hk k k) Nil Nil Nil
hArr :: (DOb hk vk j, DOb hk vk k) => (ps :: Path hk j k) ~> qs -> Sq hk vk ps qs Nil Nil
hArr1 :: (DOb hk vk j, DOb hk vk k) => (p :: hk j k) ~> q -> Sq1 hk vk p q I I
(|||) :: Sq hk vk ps qs fs gs -> Sq hk vk qs rs hs is -> Sq hk vk ps rs (fs +++ hs) (gs +++ is)
vArr :: (DOb hk vk j, DOb hk vk k) => (fs :: Path vk j k) ~> gs -> Sq hk vk Nil Nil fs gs
vArr1 :: (DOb hk vk j, DOb hk vk k) => (f :: vk j k) ~> g -> Sq1 hk vk I I f g
(===) :: Sq hk vk ps qs fs gs -> Sq hk vk rs ss gs hs -> Sq hk vk (ps +++ rs) (qs +++ ss) fs hs
(\\\\) :: ((DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k, Ob ps, Ob qs, Ob fs, Ob gs) => r) -> Sq hk vk (ps :: Path hk h j) (qs :: Path hk i k) fs gs -> r
type DOb hk vk k = (Ob0 hk k, Ob0 vk k)
class Double hk vk => Equipment hk vk where
type Companion hk vk (f :: vk j k) :: hk j k
type Conjoint hk vk (f :: vk j k) :: hk k j
fromRight :: (DOb hk vk j, DOb hk vk k, Ob (f :: vk j k)) => Sq hk vk Nil (Companion hk vk f ::: Nil) Nil (f ::: Nil)
toLeft :: (DOb hk vk j, DOb hk vk k, Ob (f :: vk j k)) => Sq hk vk (Companion hk vk f ::: Nil) Nil (f ::: Nil) Nil
toRight :: (DOb hk vk j, DOb hk vk k, Ob (f :: vk j k)) => Sq hk vk Nil (Conjoint hk vk f ::: Nil) (f ::: Nil) Nil
fromLeft :: (DOb hk vk j, DOb hk vk k, Ob (f :: vk j k)) => Sq hk vk (Conjoint hk vk f ::: Nil) Nil Nil (f ::: Nil)
withComOb :: (DOb hk vk j, DOb hk vk k, Ob (f :: vk j k)) => Obj f -> (Ob (Companion hk vk f) => r) -> r
withConOb :: (DOb hk vk j, DOb hk vk k, Ob (f :: vk j k)) => Obj f -> (Ob (Conjoint hk vk f) => r) -> r
type UnOp ps = UN OP (Fold ps)
type UnCo fs = UN CO (Fold fs)
type CoSq (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k) = Sq (OPK hk) (COK vk) ps qs fs gs
instance Double hk vk => Double (OPK hk) (COK vk) where
data Sq (OPK hk) (COK vk) ps qs fs gs where
CoSq :: forall {hk} {vk} {h} {i} {j} {k} ps qs fs gs. (Ob ps, Ob qs, Ob fs, Ob gs) => Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k)
data Sq1 (OPK hk) (COK vk) p q f g where
CoSq1 :: Sq1 hk vk (UN OP p) (UN OP q) (UN CO g) (UN CO f) -> Sq1 (OPK hk) (COK vk) p q f g
singleton :: forall (h :: k) (i :: k) (j :: k) (k :: k) (p :: OPK hk h j)
(q :: OPK hk i k) (f :: COK vk h i) (g :: COK vk j k).
(DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i,
DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k, Ob p, Ob q, Ob f,
Ob g) =>
Sq1 (OPK hk) (COK vk) p q f g
-> Sq
(OPK hk) (COK vk) (p ::: Nil) (q ::: Nil) (f ::: Nil) (g ::: Nil)
singleton = Sq1 (OPK hk) (COK vk) p q f g
-> Sq
(OPK hk) (COK vk) (p ::: Nil) (q ::: Nil) (f ::: Nil) (g ::: Nil)
Sq1
(OPK hk)
(COK vk)
(Fold (p ::: Nil))
(Fold (q ::: Nil))
(Fold (f ::: Nil))
(Fold (g ::: Nil))
-> Sq
(OPK hk) (COK vk) (p ::: Nil) (q ::: Nil) (f ::: Nil) (g ::: Nil)
forall {k} {hk :: CAT k} {vk :: CAT k} {h :: k} {i :: k} {j :: k}
{k :: k} (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k)
(fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k).
(Ob ps, Ob qs, Ob fs, Ob gs) =>
Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) ps qs fs gs
CoSq
folded :: forall (h :: k) (i :: k) (j :: k) (k :: k)
(ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k)
(fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k).
(DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i,
DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k, Ob ps, Ob qs,
Ob fs, Ob gs) =>
Sq (OPK hk) (COK vk) ps qs fs gs
-> Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
folded (CoSq Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
sq) = Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
sq
object :: forall (k :: k).
DOb (OPK hk) (COK vk) k =>
Sq (OPK hk) (COK vk) Nil Nil Nil Nil
object = Sq1 (OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
-> Sq (OPK hk) (COK vk) Nil Nil Nil Nil
forall {k} {hk :: CAT k} {vk :: CAT k} {h :: k} {i :: k} {j :: k}
{k :: k} (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k)
(fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k).
(Ob ps, Ob qs, Ob fs, Ob gs) =>
Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) ps qs fs gs
CoSq (Sq1 (OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
-> Sq (OPK hk) (COK vk) Nil Nil Nil Nil)
-> Sq1
(OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
-> Sq (OPK hk) (COK vk) Nil Nil Nil Nil
forall a b. (a -> b) -> a -> b
$ Sq1
hk
vk
(UN 'OP (Fold Nil))
(UN 'OP (Fold Nil))
(UN 'CO (Fold Nil))
(UN 'CO (Fold Nil))
-> Sq1
(OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
forall {k} {j :: k} {j :: k} {k1 :: k} {k1 :: k} (hk :: CAT k)
(vk :: CAT k) (p :: OPK hk j j) (q :: OPK hk k1 k1)
(g :: COK vk j k1) (f :: COK vk j k1).
Sq1 hk vk (UN 'OP p) (UN 'OP q) (UN 'CO g) (UN 'CO f)
-> Sq1 (OPK hk) (COK vk) p q f g
CoSq1 (Sq1
hk
vk
(UN 'OP (Fold Nil))
(UN 'OP (Fold Nil))
(UN 'CO (Fold Nil))
(UN 'CO (Fold Nil))
-> Sq1
(OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil))
-> Sq1
hk
vk
(UN 'OP (Fold Nil))
(UN 'OP (Fold Nil))
(UN 'CO (Fold Nil))
(UN 'CO (Fold Nil))
-> Sq1
(OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
forall a b. (a -> b) -> a -> b
$ Sq hk vk Nil Nil Nil Nil
-> Sq1 hk vk (Fold Nil) (Fold Nil) (Fold Nil) (Fold Nil)
forall (h :: k) (i :: k) (j :: k) (k :: k) (ps :: Path hk h j)
(qs :: Path hk i k) (fs :: Path vk h i) (gs :: Path vk j k).
(DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k, Ob ps, Ob qs,
Ob fs, Ob gs) =>
Sq hk vk ps qs fs gs
-> Sq1 hk vk (Fold ps) (Fold qs) (Fold fs) (Fold gs)
forall {k} (hk :: CAT k) (vk :: CAT k) (h :: k) (i :: k) (j :: k)
(k :: k) (ps :: Path hk h j) (qs :: Path hk i k)
(fs :: Path vk h i) (gs :: Path vk j k).
(Double hk vk, DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k,
Ob ps, Ob qs, Ob fs, Ob gs) =>
Sq hk vk ps qs fs gs
-> Sq1 hk vk (Fold ps) (Fold qs) (Fold fs) (Fold gs)
folded Sq hk vk Nil Nil Nil Nil
forall (k :: k). DOb hk vk k => Sq hk vk Nil Nil Nil Nil
forall {k} (hk :: CAT k) (vk :: CAT k) (k :: k).
(Double hk vk, DOb hk vk k) =>
Sq hk vk Nil Nil Nil Nil
object
hArr :: forall (j :: k) (k :: k) (ps :: Path (OPK hk) j k)
(qs :: Path (OPK hk) j k).
(DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k) =>
(ps ~> qs) -> Sq (OPK hk) (COK vk) ps qs Nil Nil
hArr (Str Fold ps ~> Fold qs
fs) = Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold Nil) (Fold Nil)
-> Sq (OPK hk) (COK vk) ps qs Nil Nil
forall {k} {hk :: CAT k} {vk :: CAT k} {h :: k} {i :: k} {j :: k}
{k :: k} (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k)
(fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k).
(Ob ps, Ob qs, Ob fs, Ob gs) =>
Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) ps qs fs gs
CoSq (Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold Nil) (Fold Nil)
-> Sq (OPK hk) (COK vk) ps qs Nil Nil)
-> Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold Nil) (Fold Nil)
-> Sq (OPK hk) (COK vk) ps qs Nil Nil
forall a b. (a -> b) -> a -> b
$ ('OP (UN 'OP (Fold ps)) ~> 'OP (UN 'OP (Fold qs)))
-> Sq1
(OPK hk)
(COK vk)
('OP (UN 'OP (Fold ps)))
('OP (UN 'OP (Fold qs)))
I
I
forall (j :: k) (k :: k) (p :: OPK hk j k) (q :: OPK hk j k).
(DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k) =>
(p ~> q) -> Sq1 (OPK hk) (COK vk) p q I I
forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k :: k)
(p :: hk j k) (q :: hk j k).
(Double hk vk, DOb hk vk j, DOb hk vk k) =>
(p ~> q) -> Sq1 hk vk p q I I
hArr1 Fold ps ~> Fold qs
'OP (UN 'OP (Fold ps)) ~> 'OP (UN 'OP (Fold qs))
fs
hArr1 :: forall (j :: k) (k :: k) (p :: OPK hk j k) (q :: OPK hk j k).
(DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k) =>
(p ~> q) -> Sq1 (OPK hk) (COK vk) p q I I
hArr1 (Op a1 ~> b1
f) = Sq1 hk vk (UN 'OP p) (UN 'OP q) (UN 'CO I) (UN 'CO I)
-> Sq1 (OPK hk) (COK vk) p q I I
forall {k} {j :: k} {j :: k} {k1 :: k} {k1 :: k} (hk :: CAT k)
(vk :: CAT k) (p :: OPK hk j j) (q :: OPK hk k1 k1)
(g :: COK vk j k1) (f :: COK vk j k1).
Sq1 hk vk (UN 'OP p) (UN 'OP q) (UN 'CO g) (UN 'CO f)
-> Sq1 (OPK hk) (COK vk) p q f g
CoSq1 (Sq1 hk vk (UN 'OP p) (UN 'OP q) (UN 'CO I) (UN 'CO I)
-> Sq1 (OPK hk) (COK vk) p q I I)
-> Sq1 hk vk (UN 'OP p) (UN 'OP q) (UN 'CO I) (UN 'CO I)
-> Sq1 (OPK hk) (COK vk) p q I I
forall a b. (a -> b) -> a -> b
$ (a1 ~> b1) -> Sq1 hk vk a1 b1 I I
forall (j :: k) (k :: k) (p :: hk j k) (q :: hk j k).
(DOb hk vk j, DOb hk vk k) =>
(p ~> q) -> Sq1 hk vk p q I I
forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k :: k)
(p :: hk j k) (q :: hk j k).
(Double hk vk, DOb hk vk j, DOb hk vk k) =>
(p ~> q) -> Sq1 hk vk p q I I
hArr1 a1 ~> b1
f
vArr :: forall (j :: k) (k :: k) (fs :: Path (COK vk) j k)
(gs :: Path (COK vk) j k).
(DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k) =>
(fs ~> gs) -> Sq (OPK hk) (COK vk) Nil Nil fs gs
vArr (Str Fold fs ~> Fold gs
fs) = Sq1 (OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) Nil Nil fs gs
forall {k} {hk :: CAT k} {vk :: CAT k} {h :: k} {i :: k} {j :: k}
{k :: k} (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k)
(fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k).
(Ob ps, Ob qs, Ob fs, Ob gs) =>
Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) ps qs fs gs
CoSq (Sq1 (OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) Nil Nil fs gs)
-> Sq1 (OPK hk) (COK vk) (Fold Nil) (Fold Nil) (Fold fs) (Fold gs)
-> Sq (OPK hk) (COK vk) Nil Nil fs gs
forall a b. (a -> b) -> a -> b
$ ('CO (UN 'CO (Fold fs)) ~> 'CO (UN 'CO (Fold gs)))
-> Sq1
(OPK hk)
(COK vk)
I
I
('CO (UN 'CO (Fold fs)))
('CO (UN 'CO (Fold gs)))
forall (j :: k) (k :: k) (f :: COK vk j k) (g :: COK vk j k).
(DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k) =>
(f ~> g) -> Sq1 (OPK hk) (COK vk) I I f g
forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k :: k)
(f :: vk j k) (g :: vk j k).
(Double hk vk, DOb hk vk j, DOb hk vk k) =>
(f ~> g) -> Sq1 hk vk I I f g
vArr1 Fold fs ~> Fold gs
'CO (UN 'CO (Fold fs)) ~> 'CO (UN 'CO (Fold gs))
fs
vArr1 :: forall (j :: k) (k :: k) (f :: COK vk j k) (g :: COK vk j k).
(DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k) =>
(f ~> g) -> Sq1 (OPK hk) (COK vk) I I f g
vArr1 (Co b1 ~> a1
f) = Sq1 hk vk (UN 'OP I) (UN 'OP I) (UN 'CO g) (UN 'CO f)
-> Sq1 (OPK hk) (COK vk) I I f g
forall {k} {j :: k} {j :: k} {k1 :: k} {k1 :: k} (hk :: CAT k)
(vk :: CAT k) (p :: OPK hk j j) (q :: OPK hk k1 k1)
(g :: COK vk j k1) (f :: COK vk j k1).
Sq1 hk vk (UN 'OP p) (UN 'OP q) (UN 'CO g) (UN 'CO f)
-> Sq1 (OPK hk) (COK vk) p q f g
CoSq1 (Sq1 hk vk (UN 'OP I) (UN 'OP I) (UN 'CO g) (UN 'CO f)
-> Sq1 (OPK hk) (COK vk) I I f g)
-> Sq1 hk vk (UN 'OP I) (UN 'OP I) (UN 'CO g) (UN 'CO f)
-> Sq1 (OPK hk) (COK vk) I I f g
forall a b. (a -> b) -> a -> b
$ (b1 ~> a1) -> Sq1 hk vk I I b1 a1
forall (j :: k) (k :: k) (f :: vk j k) (g :: vk j k).
(DOb hk vk j, DOb hk vk k) =>
(f ~> g) -> Sq1 hk vk I I f g
forall {k} (hk :: CAT k) (vk :: CAT k) (j :: k) (k :: k)
(f :: vk j k) (g :: vk j k).
(Double hk vk, DOb hk vk j, DOb hk vk k) =>
(f ~> g) -> Sq1 hk vk I I f g
vArr1 b1 ~> a1
f