Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.ThinCategoryAsBi

Synopsis

data THINK k (i :: k) (j :: k) = THIN
data ThinCategory (a :: THINK k i j) (b :: THINK k i j) where
- Id :: forall {k} (i :: k) (j :: k). (HasArrow (Hom k) i j, Ob i, Ob j) => ThinCategory ('THIN :: THINK k i j) ('THIN :: THINK k i j)
class HasArrow (Hom k) a a => HasIdArrow k (a :: k)
class (Thin k, forall (a :: k). Ob a => HasIdArrow k a) => Thin' k
data family ThinFunctor (p :: j +-> k) :: THINK j :-> THINK k

Documentation

data THINK k (i :: k) (j :: k) Source Github #

Constructors

THIN

Instances

Instances details

(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 #

Thin' k => Bicategory (THINK k :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

Methods

o :: forall {i :: k} {j :: k} {k0 :: k} (a :: THINK k j k0) (b :: THINK k j k0) (c :: THINK k i j) (d :: THINK k i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Github #

withOb2 :: forall {i :: k} {j :: k} {k0 :: k} (a :: THINK k j k0) (b :: THINK k i j) r. (Ob a, Ob b, Ob0 (THINK k) i, Ob0 (THINK k) j, Ob0 (THINK k) k0) => (Ob (O a b) => r) -> r Source Github #

withOb0s :: forall {j :: k} {k0 :: k} (a :: THINK k j k0) r. Ob a => ((Ob0 (THINK k) j, Ob0 (THINK k) k0) => r) -> r Source Github #

(\\\) :: forall (i :: k) (j :: k) (ps :: THINK k i j) (qs :: THINK k i j) r. ((Ob0 (THINK k) i, Ob0 (THINK k) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Github #

leftUnitor :: forall {i :: k} {j :: k} (a :: THINK k i j). (Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) => O (I :: THINK k j j) a ~> a Source Github #

leftUnitorInv :: forall {i :: k} {j :: k} (a :: THINK k i j). (Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) => a ~> O (I :: THINK k j j) a Source Github #

rightUnitor :: forall {i :: k} {j :: k} (a :: THINK k i j). (Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) => O a (I :: THINK k i i) ~> a Source Github #

rightUnitorInv :: forall {i :: k} {j :: k} (a :: THINK k i j). (Ob0 (THINK k) i, Ob0 (THINK k) j, Ob a) => a ~> O a (I :: THINK k i i) Source Github #

associator :: forall {h :: k} {i :: k} {j :: k} {k0 :: k} (a :: THINK k j k0) (b :: THINK k i j) (c :: THINK k h i). (Ob0 (THINK k) h, Ob0 (THINK k) i, Ob0 (THINK k) j, Ob0 (THINK k) k0, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c) Source Github #

associatorInv :: forall {h :: k} {i :: k} {j :: k} {k0 :: k} (a :: THINK k j k0) (b :: THINK k i j) (c :: THINK k h i). (Ob0 (THINK k) h, Ob0 (THINK k) i, Ob0 (THINK k) j, Ob0 (THINK k) k0, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Github #

Thin k => CategoryOf (THINK k i j) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi type (~>) = ThinCategory :: THINK k i j -> THINK k i j -> Type

Thin k => Promonad (ThinCategory :: THINK k i j -> THINK k i j -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

Methods

id :: forall (a :: THINK k i j). Ob a => ThinCategory a a Source Github #

(.) :: forall (b :: THINK k i j) (c :: THINK k i j) (a :: THINK k i j). ThinCategory b c -> ThinCategory a b -> ThinCategory a c Source Github #

Thin k => Profunctor (ThinCategory :: THINK k i j -> THINK k i j -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

Methods

dimap :: forall (c :: THINK k i j) (a :: THINK k i j) (b :: THINK k i j) (d :: THINK k i j). (c ~> a) -> (b ~> d) -> ThinCategory a b -> ThinCategory c d Source Github #

lmap :: forall (c :: THINK k i j) (a :: THINK k i j) (b :: THINK k i j). (c ~> a) -> ThinCategory a b -> ThinCategory c b Source Github #

rmap :: forall (b :: THINK k i j) (d :: THINK k i j) (a :: THINK k i j). (b ~> d) -> ThinCategory a b -> ThinCategory a d Source Github #

(\\) :: forall (a :: THINK k i j) (b :: THINK k i j) r. ((Ob a, Ob b) => r) -> ThinCategory a b -> r Source Github #

type Ob0 (THINK k2 :: k2 -> k2 -> Type) (a :: k1) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

type Ob0 (THINK k2 :: k2 -> k2 -> Type) (a :: k1) = Ob a

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 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 I Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

type I = 'THIN :: THINK k i i

type O ('THIN :: THINK k1 j k2) ('THIN :: THINK k1 i j) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

type O ('THIN :: THINK k1 j k2) ('THIN :: THINK k1 i j) = 'THIN :: THINK k1 i k2

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

type (~>) = ThinCategory :: THINK k i j -> THINK k i j -> Type

type Ob (a :: THINK k i j) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

type Ob (a :: THINK k i j) = (a ~ ('THIN :: THINK k i j), Ob i, Ob j, HasArrow (Hom k) i j)

data ThinCategory (a :: THINK k i j) (b :: THINK k i j) where Source Github #

Constructors

Id :: forall {k} (i :: k) (j :: k). (HasArrow (Hom k) i j, Ob i, Ob j) => ThinCategory ('THIN :: THINK k i j) ('THIN :: THINK k i j)

Instances

Instances details

Thin k => Promonad (ThinCategory :: THINK k i j -> THINK k i j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi Methods id :: forall (a :: THINK k i j). Ob a => ThinCategory a a Source Github # (.) :: forall (b :: THINK k i j) (c :: THINK k i j) (a :: THINK k i j). ThinCategory b c -> ThinCategory a b -> ThinCategory a c Source Github #
Thin k => Profunctor (ThinCategory :: THINK k i j -> THINK k i j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi Methods dimap :: forall (c :: THINK k i j) (a :: THINK k i j) (b :: THINK k i j) (d :: THINK k i j). (c ~> a) -> (b ~> d) -> ThinCategory a b -> ThinCategory c d Source Github # lmap :: forall (c :: THINK k i j) (a :: THINK k i j) (b :: THINK k i j). (c ~> a) -> ThinCategory a b -> ThinCategory c b Source Github # rmap :: forall (b :: THINK k i j) (d :: THINK k i j) (a :: THINK k i j). (b ~> d) -> ThinCategory a b -> ThinCategory a d Source Github # (\\) :: forall (a :: THINK k i j) (b :: THINK k i j) r. ((Ob a, Ob b) => r) -> ThinCategory a b -> r Source Github #

class HasArrow (Hom k) a a => HasIdArrow k (a :: k) Source Github #

Instances

Instances details

HasArrow (Hom k) a a => HasIdArrow k (a :: k) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

class (Thin k, forall (a :: k). Ob a => HasIdArrow k a) => Thin' k Source Github #

Instances

Instances details

(Thin k, forall (a :: k). Ob a => HasIdArrow k a) => Thin' k Source Github #
Instance details Defined in Proarrow.Category.Bicategory.ThinCategoryAsBi

data family ThinFunctor (p :: j +-> k) :: THINK j :-> THINK k Source Github #

A functor between thin categories, i.e. a monotone function.

Instances

Instances details

(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 #
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 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