Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.Sub

Documentation

class IsOb tag (a :: k) Source Comments #

data SUBCAT tag (kk :: CAT k) (i :: k) (j :: k) Source Comments #

Constructors

SUB (kk i j)

Instances

Instances details

(Bicategory kk, forall (i :: k). Ob0 kk i => IsObI tag kk i, forall (i :: k) (j :: k) (k1 :: k) (a :: kk i j) (b :: kk j k1). (IsOb tag a, IsOb tag b) => IsObO tag kk i j k1 a b) => Bicategory (SUBCAT tag kk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

o :: forall {k1 :: k} (i :: k) (j :: k) (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk j k1) (d :: SUBCAT tag kk j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall (i :: k) (j :: k) (ps :: SUBCAT tag kk i j) (qs :: SUBCAT tag kk i j) r. ((Ob0 (SUBCAT tag kk) i, Ob0 (SUBCAT tag kk) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> O (I :: SUBCAT tag kk i i) a ~> a Source Comments #

leftUnitorInv :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> a ~> O (I :: SUBCAT tag kk i i) a Source Comments #

rightUnitor :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> O a (I :: SUBCAT tag kk j j) ~> a Source Comments #

rightUnitorInv :: forall (i :: k) (j :: k) (a :: SUBCAT tag kk i j). Obj a -> a ~> O a (I :: SUBCAT tag kk j j) Source Comments #

associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: SUBCAT tag kk i j2) (b :: SUBCAT tag kk j2 j1) (c :: SUBCAT tag kk j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: SUBCAT tag kk i j2) (b :: SUBCAT tag kk j2 j1) (c :: SUBCAT tag kk j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments #

CategoryOf (kk i j) => CategoryOf (SUBCAT tag kk i j) Source Comments #

The subcategory with objects with instances of the given constraint `IsOb tag`.

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.Sub type (~>) = Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type

Promonad ((~>) :: CAT (kk i j)) => Promonad (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

id :: forall (a :: SUBCAT tag kk i j). Ob a => Sub a a Source Comments #

(.) :: forall (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j). Sub b c -> Sub a b -> Sub a c Source Comments #

Profunctor ((~>) :: CAT (kk i j)) => Profunctor (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

Methods

dimap :: forall (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) (d :: SUBCAT tag kk i j). (c ~> a) -> (b ~> d) -> Sub a b -> Sub c d Source Comments #

(\\) :: forall (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) r. ((Ob a, Ob b) => r) -> Sub a b -> r Source Comments #

type Ob0 (SUBCAT tag kk :: k2 -> k2 -> Type) (k3 :: k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type Ob0 (SUBCAT tag kk :: k2 -> k2 -> Type) (k3 :: k1) = Ob0 kk k3

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type I = 'SUB (I :: kk i i) :: SUBCAT tag kk i i

type O (p :: SUBCAT tag kk i1 i2) (q :: SUBCAT tag kk i2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type O (p :: SUBCAT tag kk i1 i2) (q :: SUBCAT tag kk i2 j) = 'SUB (O (UN ('SUB :: kk i1 i2 -> SUBCAT tag kk i1 i2) p) (UN ('SUB :: kk i2 j -> SUBCAT tag kk i2 j) q)) :: SUBCAT tag kk i1 j

type UN ('SUB :: kk i j -> SUBCAT tag kk i j) ('SUB p :: SUBCAT tag kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type UN ('SUB :: kk i j -> SUBCAT tag kk i j) ('SUB p :: SUBCAT tag kk i j) = p

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type (~>) = Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type

type Ob (a :: SUBCAT tag kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Sub

type Ob (a :: SUBCAT tag kk i j) = (Is ('SUB :: kk i j -> SUBCAT tag kk i j) a, Ob (UN ('SUB :: kk i j -> SUBCAT tag kk i j) a), IsOb tag (UN ('SUB :: kk i j -> SUBCAT tag kk i j) a))

data Sub (a :: SUBCAT ob kk i j) (b :: SUBCAT ob kk i j) where Source Comments #

Constructors

Sub :: forall {k} ob (kk :: CAT k) (i :: k) (j :: k) (a1 :: kk i j) (b1 :: kk i j). (IsOb ob a1, IsOb ob b1) => (a1 ~> b1) -> Sub ('SUB a1 :: SUBCAT ob kk i j) ('SUB b1 :: SUBCAT ob kk i j)

Instances

Instances details

Promonad ((~>) :: CAT (kk i j)) => Promonad (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub Methods id :: forall (a :: SUBCAT tag kk i j). Ob a => Sub a a Source Comments # (.) :: forall (b :: SUBCAT tag kk i j) (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j). Sub b c -> Sub a b -> Sub a c Source Comments #
Profunctor ((~>) :: CAT (kk i j)) => Profunctor (Sub :: SUBCAT tag kk i j -> SUBCAT tag kk i j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub Methods dimap :: forall (c :: SUBCAT tag kk i j) (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) (d :: SUBCAT tag kk i j). (c ~> a) -> (b ~> d) -> Sub a b -> Sub c d Source Comments # (\\) :: forall (a :: SUBCAT tag kk i j) (b :: SUBCAT tag kk i j) r. ((Ob a, Ob b) => r) -> Sub a b -> r Source Comments #

class IsOb tag (O a b) => IsObO tag (kk :: k -> k -> Type) (i :: k) (j :: k) (k1 :: k) (a :: kk i j) (b :: kk j k1) Source Comments #

Instances

Instances details

IsOb tag (O a b) => IsObO tag (kk :: k1 -> k1 -> Type) (i :: k1) (j :: k1) (k2 :: k1) (a :: kk i j) (b :: kk j k2) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub

class IsOb tag (I :: kk i i) => IsObI tag (kk :: k -> k -> Type) (i :: k) Source Comments #

Instances

Instances details

IsOb tag (I :: kk i i) => IsObI tag (kk :: k -> k -> Type) (i :: k) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Sub