Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.LaxFunctor

Synopsis

type family Sort (kk :: CAT s) where ...
type (:->) (kk :: CAT s) (ll :: CAT t) = Proxy kk -> Proxy ll -> Type
type family Map0 (f :: kk :-> ll) (i :: s) :: t
type family Map1 (f :: kk :-> ll) (a :: kk i j) :: ll (Map0 f i) (Map0 f j)
class (Bicategory kk, Bicategory ll) => LaxFunctor (f :: kk :-> ll) where
- map2 :: forall {i :: sk} {j :: sk} (a :: kk i j) (b :: kk i j). (Ob0 kk i, Ob0 kk j, Ob a, Ob b) => (a ~> b) -> Map1 f a ~> Map1 f b
- laxId :: forall (i :: Sort kk). Ob0 kk i => (I :: ll (Map0 f i) (Map0 f i)) ~> Map1 f (I :: kk i i)
- laxComp :: forall {i :: sk} {j :: sk} {k :: sk} (a :: kk j k) (b :: kk i j). (Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b) => O (Map1 f a) (Map1 f b) ~> Map1 f (O a b)
- withMap0Ob0 :: forall (i :: Sort kk) r. Ob0 kk i => (Ob0 ll (Map0 f i) => r) -> r
- withMap1Ob :: forall {i :: sk} {j :: sk} (a :: kk i j) r. (Ob0 kk i, Ob0 kk j, Ob a) => ((Ob (Map1 f a), Ob0 ll (Map0 f i), Ob0 ll (Map0 f j)) => r) -> r
class (I :: ll (Map0 f i) (Map0 f i)) ~ Map1 f (I :: kk i i) => IsNormal (f :: kk :-> ll) (i :: Sort kk)
class (LaxFunctor f, forall (i :: sk). Ob0 kk i => IsNormal f i) => NormalLaxFunctor (f :: kk :-> ll)

Documentation

type family Sort (kk :: CAT s) where ... Source Github #

Equations

Sort (kk :: CAT s) = s

type (:->) (kk :: CAT s) (ll :: CAT t) = Proxy kk -> Proxy ll -> Type Source Github #

The kind of a tag for a lax functor. Just a way to store kk and ll.

type family Map0 (f :: kk :-> ll) (i :: s) :: t Source Github #

Mapping of 0-cells.

Instances

Instances details

type Map0 (MonFunctor p :: MonK j :-> MonK k) '() Source Github #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Map0 (MonFunctor p :: MonK j :-> MonK k) '() = '()
type Map0 (ThinFunctor p :: THINK j :-> THINK k) (a :: j) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi type Map0 (ThinFunctor p :: THINK j :-> THINK k) (a :: j) = p % a

type family Map1 (f :: kk :-> ll) (a :: kk i j) :: ll (Map0 f i) (Map0 f j) Source Github #

Mapping of 1-cells.

Instances

Instances details

type Map1 (ThinFunctor p :: THINK k :-> THINK t) ('THIN :: THINK k i j) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi type Map1 (ThinFunctor p :: THINK k :-> THINK t) ('THIN :: THINK k i j) = 'THIN :: THINK t (Map0 (ThinFunctor p) i) (Map0 (ThinFunctor p) j)
type Map1 (MonFunctor p :: MonK j1 :-> MonK k) ('MK a :: MonK j1 i j2) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Map1 (MonFunctor p :: MonK j1 :-> MonK k) ('MK a :: MonK j1 i j2) = 'MK (p % a) :: MonK k (Map0 (MonFunctor p) i) (Map0 (MonFunctor p) j2)

class (Bicategory kk, Bicategory ll) => LaxFunctor (f :: kk :-> ll) where Source Github #

A Lax Functor between two bicategories. f is the functor tag, kk is the source bicategory, and ll is the target.

Methods

map2 :: forall {i :: sk} {j :: sk} (a :: kk i j) (b :: kk i j). (Ob0 kk i, Ob0 kk j, Ob a, Ob b) => (a ~> b) -> Map1 f a ~> Map1 f b Source Github #

Strict mapping of 2-cells. This is a strict functor on the hom-categories.

laxId :: forall (i :: Sort kk). Ob0 kk i => (I :: ll (Map0 f i) (Map0 f i)) ~> Map1 f (I :: kk i i) Source Github #

Lax Identity (Laxator for the unit). Note the types: from the identity of the target bicategory, to the mapped identity of the source bicategory.

laxComp :: forall {i :: sk} {j :: sk} {k :: sk} (a :: kk j k) (b :: kk i j). (Ob0 kk i, Ob0 kk j, Ob0 kk k, Ob a, Ob b) => O (Map1 f a) (Map1 f b) ~> Map1 f (O a b) Source Github #

Lax Composition (Laxator for tensor/composition).

withMap0Ob0 :: forall (i :: Sort kk) r. Ob0 kk i => (Ob0 ll (Map0 f i) => r) -> r Source Github #

Get proof that mapping a 0-cell yields a valid 0-cell in the target.

withMap1Ob :: forall {i :: sk} {j :: sk} (a :: kk i j) r. (Ob0 kk i, Ob0 kk j, Ob a) => ((Ob (Map1 f a), Ob0 ll (Map0 f i), Ob0 ll (Map0 f j)) => r) -> r Source Github #

Get proof that mapping a 1-cell yields a valid 1-cell in the target.

Instances

Instances details

(MonoidalProfunctor p, Representable p) => LaxFunctor (MonFunctor p :: MonK j :-> MonK k) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi Methods map2 :: forall {i :: ()} {j0 :: ()} (a :: MonK j i j0) (b :: MonK j i j0). (Ob0 (MonK j) i, Ob0 (MonK j) j0, Ob a, Ob b) => (a ~> b) -> Map1 (MonFunctor p) a ~> Map1 (MonFunctor p) b Source Github # laxId :: forall (i :: Sort (MonK j)). Ob0 (MonK j) i => (I :: MonK k (Map0 (MonFunctor p) i) (Map0 (MonFunctor p) i)) ~> Map1 (MonFunctor p) (I :: MonK j i i) Source Github # laxComp :: forall {i :: ()} {j0 :: ()} {k0 :: ()} (a :: MonK j j0 k0) (b :: MonK j i j0). (Ob0 (MonK j) i, Ob0 (MonK j) j0, Ob0 (MonK j) k0, Ob a, Ob b) => O (Map1 (MonFunctor p) a) (Map1 (MonFunctor p) b) ~> Map1 (MonFunctor p) (O a b) Source Github # withMap0Ob0 :: forall (i :: Sort (MonK j)) r. Ob0 (MonK j) i => (Ob0 (MonK k) (Map0 (MonFunctor p) i) => r) -> r Source Github # withMap1Ob :: forall {i :: ()} {j0 :: ()} (a :: MonK j i j0) r. (Ob0 (MonK j) i, Ob0 (MonK j) j0, Ob a) => ((Ob (Map1 (MonFunctor p) a), Ob0 (MonK k) (Map0 (MonFunctor p) i), Ob0 (MonK k) (Map0 (MonFunctor p) j0)) => r) -> r Source Github #
(Representable p, Thin' j, Thin' k) => LaxFunctor (ThinFunctor p :: THINK j :-> THINK k) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi Methods map2 :: forall {i :: j} {j0 :: j} (a :: THINK j i j0) (b :: THINK j i j0). (Ob0 (THINK j) i, Ob0 (THINK j) j0, Ob a, Ob b) => (a ~> b) -> Map1 (ThinFunctor p) a ~> Map1 (ThinFunctor p) b Source Github # laxId :: forall (i :: Sort (THINK j)). Ob0 (THINK j) i => (I :: THINK k (Map0 (ThinFunctor p) i) (Map0 (ThinFunctor p) i)) ~> Map1 (ThinFunctor p) (I :: THINK j i i) Source Github # laxComp :: forall {i :: j} {j0 :: j} {k0 :: j} (a :: THINK j j0 k0) (b :: THINK j i j0). (Ob0 (THINK j) i, Ob0 (THINK j) j0, Ob0 (THINK j) k0, Ob a, Ob b) => O (Map1 (ThinFunctor p) a) (Map1 (ThinFunctor p) b) ~> Map1 (ThinFunctor p) (O a b) Source Github # withMap0Ob0 :: forall (i :: Sort (THINK j)) r. Ob0 (THINK j) i => (Ob0 (THINK k) (Map0 (ThinFunctor p) i) => r) -> r Source Github # withMap1Ob :: forall {i :: j} {j0 :: j} (a :: THINK j i j0) r. (Ob0 (THINK j) i, Ob0 (THINK j) j0, Ob a) => ((Ob (Map1 (ThinFunctor p) a), Ob0 (THINK k) (Map0 (ThinFunctor p) i), Ob0 (THINK k) (Map0 (ThinFunctor p) j0)) => r) -> r Source Github #

class (I :: ll (Map0 f i) (Map0 f i)) ~ Map1 f (I :: kk i i) => IsNormal (f :: kk :-> ll) (i :: Sort kk) Source Github #

Instances

Instances details

(I :: ll (Map0 f i) (Map0 f i)) ~ Map1 f (I :: kk i i) => IsNormal (f :: kk :-> ll) (i :: Sort kk) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.LaxFunctor

class (LaxFunctor f, forall (i :: sk). Ob0 kk i => IsNormal f i) => NormalLaxFunctor (f :: kk :-> ll) Source Github #

Instances

Instances details

(LaxFunctor f, forall (i :: sk). Ob0 kk i => IsNormal f i) => NormalLaxFunctor (f :: kk :-> ll) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.LaxFunctor