Rewrite of equipments

Author: sjoerdvisscher

proarrow.cabal

@@ -65,10 +65,8 @@ library
         Proarrow.Category.Enriched.Dagger
         Proarrow.Category.Enriched.ThinCategory
         Proarrow.Category.Equipment
-        Proarrow.Category.Equipment.BiAsEquipment
         Proarrow.Category.Equipment.Limit
         Proarrow.Category.Equipment.Stateful
-        Proarrow.Category.Equipment.Quintet
         Proarrow.Category.Instance.Ap
         Proarrow.Category.Instance.Bool
         Proarrow.Category.Instance.Cat

src/Proarrow/Adjunction.hs

@@ -57,11 +57,11 @@ class (Profunctor p, Profunctor q) => Proadjunction (p :: j +-> k) (q :: k +-> j
   unit :: (Ob a) => (q :.: p) a a -- (~>) :~> q :.: p
   counit :: p :.: q :~> (~>)
 
-instance (Representable f) => Proadjunction f (RepCostar f) where
+instance (Representable p) => Proadjunction p (RepCostar p) where
   unit = trivialCorep :.: trivialRep
   counit (f :.: g) = coindex g . index f
 
-instance (Corepresentable f) => Proadjunction (CorepStar f) f where
+instance (Corepresentable p) => Proadjunction (CorepStar p) p where
   unit = trivialCorep :.: trivialRep
   counit (f :.: g) = coindex g . index f
 

src/Proarrow/Category/Bicategory.hs

@@ -24,13 +24,16 @@ module Proarrow.Category.Bicategory
   , Monad (..)
   , Comonad (..)
   , Adjunction (..)
-  , leftAdjunct
-  , rightAdjunct
+  , flipLeftAdjoint
+  , flipLeftAdjointInv
+  , flipRightAdjoint
+  , flipRightAdjointInv
   , Bimodule (..)
   )
 where
 
 import Data.Kind (Constraint)
+import Prelude (($))
 
 import Proarrow.Core (CAT, CategoryOf (..), Promonad (..), id)
 import Proarrow.Object (Obj, obj)
@@ -41,6 +44,7 @@ infixl 1 \\\
 
 -- | A bicategory is locally "something" if each hom-category is "something".
 class (forall j k. (Ob0 kk j, Ob0 kk k) => c (kk j k)) => Locally c kk
+
 instance (forall j k. (Ob0 kk j, Ob0 kk k) => c (kk j k)) => Locally c kk
 
 class (Ob0 kk j) => Ob0' kk j
@@ -139,12 +143,12 @@ rightUnitorInvWith c ab = ((ab `o` c) . rightUnitorInv) \\\ ab
 f == g = g . f
 
 type Monad :: forall {kk} {a}. kk a a -> Constraint
-class (Bicategory kk, Ob0 kk a, Ob t) => Monad (t :: kk a a) where
+class (Bicategory kk, Ob t) => Monad (t :: kk a a) where
   eta :: I ~> t
   mu :: t `O` t ~> t
 
 type Comonad :: forall {kk} {a}. kk a a -> Constraint
-class (Bicategory kk, Ob0 kk a, Ob t) => Comonad (t :: kk a a) where
+class (Bicategory kk, Ob t) => Comonad (t :: kk a a) where
   epsilon :: t ~> I
   delta :: t ~> t `O` t
 
@@ -158,28 +162,61 @@ instance {-# OVERLAPPABLE #-} (Monad s) => Bimodule s s s where
   rightAction = mu
 
 type Adjunction :: forall {kk} {c} {d}. kk c d -> kk d c -> Constraint
-class (Bicategory kk, Ob0 kk c, Ob0 kk d) => Adjunction (l :: kk c d) (r :: kk d c) where
+class (Bicategory kk, Ob l, Ob r) => Adjunction (l :: kk c d) (r :: kk d c) where
   unit :: I ~> r `O` l
   counit :: l `O` r ~> I
 
-leftAdjunct
+flipLeftAdjoint
   :: forall {kk} {c} {d} {i} (l :: kk c d) (r :: kk d c) (a :: kk i c) b
-   . (Adjunction l r, Ob a, Ob r, Ob l, Ob0 kk i)
+   . (Adjunction l r, Ob a)
   => l `O` a ~> b
   -> a ~> r `O` b
-leftAdjunct f =
-  leftUnitorInv
-    == unit @l @r || obj @a
-    == associator @_ @r @l @a
-    == obj @r || f
-
-rightAdjunct
+flipLeftAdjoint f =
+  withOb0s @kk @l $
+    withOb0s @kk @a $
+      ( leftUnitorInv
+          == unit @l @r || obj @a
+          == associator @_ @r @l @a
+          == obj @r || f
+      )
+
+flipLeftAdjointInv
   :: forall {kk} {c} {d} {i} (l :: kk c d) (r :: kk d c) (a :: kk i c) b
-   . (Adjunction l r, Ob b, Ob r, Ob l, Ob0 kk i)
+   . (Adjunction l r, Ob b)
   => a ~> r `O` b
   -> l `O` a ~> b
-rightAdjunct f =
-  obj @l || f
-    == associatorInv @_ @l @r @b
-    == counit @l @r || obj @b
-    == leftUnitor
+flipLeftAdjointInv f =
+  withOb0s @kk @r $
+    withOb0s @kk @b $
+      ( obj @l || f
+          == associatorInv @_ @l @r @b
+          == counit @l @r || obj @b
+          == leftUnitor
+      )
+
+flipRightAdjoint
+  :: forall {kk} {c} {d} {i} (l :: kk c d) (r :: kk d c) (a :: kk c i) b
+   . (Adjunction l r, Ob a)
+  => a `O` r ~> b
+  -> a ~> b `O` l
+flipRightAdjoint f =
+  withOb0s @kk @l $
+    withOb0s @kk @a $
+      rightUnitorInv
+        == obj @a || unit @l @r
+        == associatorInv @_ @a @r @l
+        == f || obj @l
+
+flipRightAdjointInv
+  :: forall {kk} {c} {d} {i} (l :: kk c d) (r :: kk d c) a (b :: kk d i)
+   . (Adjunction l r, Ob b)
+  => a ~> b `O` l
+  -> a `O` r ~> b
+flipRightAdjointInv f =
+  withOb0s @kk @r $
+    withOb0s @kk @b $
+      ( f || obj @r
+          == associator @_ @b @l @r
+          == obj @b || counit @l @r
+          == rightUnitor
+      )

src/Proarrow/Category/Bicategory/Co.hs

@@ -1,16 +1,18 @@
 module Proarrow.Category.Bicategory.Co where
 
 import Proarrow.Category.Bicategory
-  ( Bicategory (..)
+  ( Adjunction (..)
+  , Bicategory (..)
   , Comonad (..)
-  , Monad (..), Adjunction (..)
+  , Monad (..)
   )
 import Proarrow.Category.Bicategory.Kan
   ( LeftKanExtension (..)
   , LeftKanLift (..)
   , RightKanExtension (..)
   , RightKanLift (..)
   )
+import Proarrow.Category.Equipment (Cotight, CotightAdjoint, Equipment (..), IsOb, Tight, TightAdjoint, WithObO2 (..))
 import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
 
 type COK :: CAT k -> CAT k
@@ -45,9 +47,21 @@ instance (Bicategory kk) => Bicategory (COK kk) where
   rightUnitor = Co rightUnitorInv
   rightUnitorInv = Co rightUnitor
   associator @(CO p) @(CO q) @(CO r) = Co (associatorInv @kk @p @q @r)
-  associatorInv  @(CO p) @(CO q) @(CO r) = Co (associator @kk @p @q @r)
+  associatorInv @(CO p) @(CO q) @(CO r) = Co (associator @kk @p @q @r)
 
-instance Adjunction f g => Adjunction (CO g) (CO f) where
+type instance IsOb Tight p = IsOb Cotight (UN CO p)
+type instance IsOb Cotight p = IsOb Tight (UN CO p)
+type instance TightAdjoint p = CO (CotightAdjoint (UN CO p))
+type instance CotightAdjoint p = CO (TightAdjoint (UN CO p))
+instance (WithObO2 Cotight kk) => WithObO2 Tight (COK kk) where
+  withObO2 @p @q r = withObO2 @Cotight @kk @(UN CO p) @(UN CO q) r
+instance (WithObO2 Tight kk) => WithObO2 Cotight (COK kk) where
+  withObO2 @p @q r = withObO2 @Tight @kk @(UN CO p) @(UN CO q) r
+instance (Equipment kk) => Equipment (COK kk) where
+  withTightAdjoint @(CO f) r = withCotightAdjoint @kk @f r
+  withCotightAdjoint @(CO f) r = withTightAdjoint @kk @f r
+
+instance (Adjunction f g) => Adjunction (CO g) (CO f) where
   unit = Co (counit @f @g)
   counit = Co (unit @f @g)
 

src/Proarrow/Category/Bicategory/Kan.hs

@@ -4,16 +4,18 @@ module Proarrow.Category.Bicategory.Kan where
 
 import Data.Kind (Constraint)
 
-import Proarrow.Category.Bicategory (Bicategory (..), (==), (||), Monad (..), rightUnitorInvWith, Comonad (..), rightUnitorWith, obj1)
-import Proarrow.Category.Equipment
-  ( Equipment (..)
-  , HasCompanions (..)
-  , flipCompanion
-  , flipCompanionInv
-  , flipConjoint
-  , flipConjointInv
+import Proarrow.Category.Bicategory
+  ( Adjunction (..)
+  , Bicategory (..)
+  , Comonad (..)
+  , Monad (..)
+  , rightUnitorInvWith
+  , rightUnitorWith
+  , (==)
+  , (||), flipRightAdjointInv, flipRightAdjoint, flipLeftAdjointInv, flipLeftAdjoint
   )
-import Proarrow.Core (CAT, CategoryOf (..), Ob, Obj, Profunctor (..), Promonad (..), obj, (\\))
+
+import Proarrow.Core (CAT, CategoryOf (..), Ob, Profunctor (..), Promonad (..), obj, (\\))
 
 type LeftKanExtension :: forall {k} {kk :: CAT k} {c} {d} {e}. kk c d -> kk c e -> Constraint
 class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lan j f)) => LeftKanExtension (j :: kk c d) (f :: kk c e) where
@@ -39,7 +41,7 @@ lanComonadDelta :: forall {kk} {c} {d} (p :: kk c d). (LeftKanExtension p p) =>
 lanComonadDelta =
   let lpp = obj @(Lan p p)
   in lanUniv @p @p (associatorInv @_ @(Lan p p) @(Lan p p) @p . (lpp `o` lan @p @p) . lan @p @p)
-      \\ (lpp `o` lpp)
+       \\ (lpp `o` lpp)
 
 -- | Density is the "mother of all comonads"
 coinj :: forall p. (Comonad p, LeftKanExtension p p) => p ~> Density p
@@ -51,22 +53,19 @@ corun = lanUniv @p @p delta
 idLan :: forall f. (LeftKanExtension I f, Ob f) => f ~> Lan I f
 idLan = rightUnitor . lan @I @f
 
-lanAlongCompanion
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (LeftKanExtension (Companion hk j) f, Equipment hk vk, Ob j)
-  => Lan (Companion hk j) f ~> f `O` Conjoint hk j
-lanAlongCompanion =
-  let j = obj1 @j; f = obj @f; conJ = mapConjoint @hk j
-  in lanUniv @(Companion hk j) @f
-      (rightUnitorInv == f || comConUnit j == associatorInv @_ @f @(Conjoint hk j) @(Companion hk j))
-      \\ (f `o` conJ)
-      \\ conJ
-
-lanAlongCompanionInv
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (LeftKanExtension (Companion hk j) f, Equipment hk vk, Ob j)
-  => f `O` Conjoint hk j ~> Lan (Companion hk j) f
-lanAlongCompanionInv = flipConjointInv @j @f @(Lan (Companion hk j) f) (lan @(Companion hk j))
+lanAlongLeftAdjoint
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (LeftKanExtension j f, Adjunction j j', Ob j, Ob j')
+  => Lan j f ~> f `O` j'
+lanAlongLeftAdjoint =
+  withOb2 @kk @f @j'
+    (lanUniv @j @f (rightUnitorInv == obj @f || unit @j @j' == associatorInv @_ @f @j' @j))
+
+lanAlongLeftAdjointInv
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (LeftKanExtension j f, Adjunction j j', Ob j, Ob j')
+  => f `O` j' ~> Lan j f
+lanAlongLeftAdjointInv = flipRightAdjointInv @j @j' (lan @j @f)
 
 type j |> p = Ran j p
 type RightKanExtension :: forall {k} {kk :: CAT k} {c} {d} {e}. kk c d -> kk c e -> Constraint
@@ -113,21 +112,19 @@ composeRan =
 idRan :: forall f. (RightKanExtension I f, Ob f) => f ~> Ran I f
 idRan = ranUniv @I @f rightUnitor
 
-ranAlongConjoint
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (RightKanExtension (Conjoint hk j) f, Equipment hk vk, Ob j)
-  => Ran (Conjoint hk j) f ~> f `O` Companion hk j
-ranAlongConjoint = flipConjoint @j @(Ran (Conjoint hk j) f) @f (ran @(Conjoint hk j))
-
-ranAlongConjointInv
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (RightKanExtension (Conjoint hk j) f, Equipment hk vk, Ob j)
-  => f `O` Companion hk j ~> Ran (Conjoint hk j) f
-ranAlongConjointInv =
-  let j = obj1 @j; f = obj @f; comJ = mapCompanion @hk j
-  in ranUniv @(Conjoint hk j) @f (rightUnitor . (f `o` comConCounit j) . associator @_ @f @(Companion hk j) @(Conjoint hk j))
-      \\ (f `o` comJ)
-      \\ comJ
+ranAlongRightAdjoint
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (RightKanExtension j' f, Adjunction j j', Ob j, Ob j')
+  => Ran j' f ~> f `O` j
+ranAlongRightAdjoint = flipRightAdjoint @j @j' (ran @j' @f)
+
+ranAlongRightAdjointInv
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (RightKanExtension j' f, Adjunction j j', Ob j, Ob j')
+  => f `O` j ~> Ran j' f
+ranAlongRightAdjointInv =
+  withOb2 @kk @f @j
+    (ranUniv @j' @f (associator @_ @f @j @j' == obj @f || counit @j @j' == rightUnitor))
 
 type LeftKanLift :: forall {k} {kk :: CAT k} {c} {d} {e}. kk d c -> kk e c -> Constraint
 class (Bicategory kk, Ob0 kk c, Ob0 kk d, Ob0 kk e, Ob f, Ob j, Ob (Lift j f)) => LeftKanLift (j :: kk d c) (f :: kk e c) where
@@ -151,27 +148,24 @@ liftComonadDelta :: forall {kk} {c} {d} (p :: kk d c). (LeftKanLift p p) => Lift
 liftComonadDelta =
   let lpp = obj @(Lift p p)
   in liftUniv @p @p (associator @_ @p @(Lift p p) @(Lift p p) . (lift @p @p `o` lpp) . lift @p @p)
-      \\ (lpp `o` lpp)
+       \\ (lpp `o` lpp)
 
 idLift :: forall f. (LeftKanLift I f, Ob f) => f ~> Lift I f
 idLift = leftUnitor . lift @I @f
 
-liftAlongConjoint
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (Ob j, LeftKanLift (Conjoint hk j) f, Equipment hk vk)
-  => Lift (Conjoint hk j) f ~> Companion hk j `O` f
-liftAlongConjoint =
-  let j = obj1 @j; f = obj @f; comJ = mapCompanion @hk j
-  in liftUniv @(Conjoint hk j) @f
-      (associator @_ @(Conjoint hk j) @(Companion hk j) @f . (comConUnit j `o` f) . leftUnitorInv)
-      \\ (comJ `o` f)
-      \\ comJ
-
-liftAlongConjointInv
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (Ob j, LeftKanLift (Conjoint hk j) f, Equipment hk vk)
-  => Companion hk j `O` f ~> Lift (Conjoint hk j) f
-liftAlongConjointInv = flipCompanionInv @j @f @(Lift (Conjoint hk j) f) (lift @(Conjoint hk j))
+liftAlongRightAdjoint
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (Ob j, Ob j', LeftKanLift j' f, Adjunction j j')
+  => Lift j' f ~> j `O` f
+liftAlongRightAdjoint =
+  withOb2 @kk @j @f
+    (liftUniv @j' @f (leftUnitorInv == unit @j @j' || obj @f == associator @_ @j' @j @f))
+
+liftAlongRightAdjointInv
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (Ob j, Ob j', LeftKanLift j' f, Adjunction j j')
+  => j `O` f ~> Lift j' f
+liftAlongRightAdjointInv = flipLeftAdjointInv @j @j' (lift @j' @f)
 
 type f <| j = Rift j f
 type RightKanLift :: forall {k} {kk :: CAT k} {c} {d} {e}. kk d c -> kk e c -> Constraint
@@ -196,7 +190,7 @@ riftMonadMu :: forall {kk} {c} {d} (p :: kk d c). (RightKanLift p p) => Rift p p
 riftMonadMu =
   let rpp = obj @(Rift p p)
   in riftUniv @p @p (rift @p @p . (rift @p @p `o` rpp) . associatorInv @_ @p @(Rift p p) @(Rift p p))
-      \\ (rpp `o` rpp)
+       \\ (rpp `o` rpp)
 
 composeRift
   :: forall i j f
@@ -209,20 +203,16 @@ composeRift =
 idRift :: forall f. (RightKanLift I f, Ob f) => f ~> Rift I f
 idRift = riftUniv @I @f leftUnitor
 
-riftAlongCompanion
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (Ob j, RightKanLift (Companion hk j) f, Equipment hk vk)
-  => Rift (Companion hk j) f ~> Conjoint hk j `O` f
-riftAlongCompanion = flipCompanion @j @(Rift (Companion hk j) f) @f (rift @(Companion hk j))
-
-riftAlongCompanionInv
-  :: forall {i} {k} hk vk (j :: vk i k) f
-   . (RightKanLift (Companion hk j) f, Equipment hk vk)
-  => Obj j
-  -> Conjoint hk j `O` f ~> Rift (Companion hk j) f
-riftAlongCompanionInv j =
-  let f = obj @f; conJ = mapConjoint @hk j
-  in riftUniv @(Companion hk j) @f
-      (leftUnitor . (comConCounit j `o` f) . associatorInv @_ @(Companion hk j) @(Conjoint hk j) @f)
-      \\ (conJ `o` f)
-      \\ conJ
+riftAlongLeftAdjoint
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (RightKanLift j f, Adjunction j j', Ob j, Ob j')
+  => Rift j f ~> j' `O` f
+riftAlongLeftAdjoint = flipLeftAdjoint @j @j' (rift @j @f)
+
+riftAlongLeftAdjointInv
+  :: forall {i} {k} kk (j :: kk i k) j' f
+   . (RightKanLift j f, Adjunction j j', Ob j, Ob j')
+  => j' `O` f ~> Rift j f
+riftAlongLeftAdjointInv =
+  withOb2 @kk @j' @f
+    (riftUniv @j @f (associatorInv @_ @j @j' @f == counit @j @j' || obj @f == leftUnitor))